1 /*
2 * yosys -- Yosys Open SYnthesis Suite
3 *
4 * Copyright (C) 2012 Claire Xenia Wolf <claire@yosyshq.com>
5 *
6 * Permission to use, copy, modify, and/or distribute this software for any
7 * purpose with or without fee is hereby granted, provided that the above
8 * copyright notice and this permission notice appear in all copies.
9 *
10 * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
11 * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
12 * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
13 * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
14 * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
15 * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
16 * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
17 *
18 */
19
20 #include "kernel/register.h"
21 #include "kernel/rtlil.h"
22 #include "kernel/log.h"
23
24 USING_YOSYS_NAMESPACE
25 PRIVATE_NAMESPACE_BEGIN
26
create_miter_equiv(struct Pass * that,std::vector<std::string> args,RTLIL::Design * design)27 void create_miter_equiv(struct Pass *that, std::vector<std::string> args, RTLIL::Design *design)
28 {
29 bool flag_ignore_gold_x = false;
30 bool flag_make_outputs = false;
31 bool flag_make_outcmp = false;
32 bool flag_make_assert = false;
33 bool flag_flatten = false;
34
35 log_header(design, "Executing MITER pass (creating miter circuit).\n");
36
37 size_t argidx;
38 for (argidx = 2; argidx < args.size(); argidx++)
39 {
40 if (args[argidx] == "-ignore_gold_x") {
41 flag_ignore_gold_x = true;
42 continue;
43 }
44 if (args[argidx] == "-make_outputs") {
45 flag_make_outputs = true;
46 continue;
47 }
48 if (args[argidx] == "-make_outcmp") {
49 flag_make_outcmp = true;
50 continue;
51 }
52 if (args[argidx] == "-make_assert") {
53 flag_make_assert = true;
54 continue;
55 }
56 if (args[argidx] == "-flatten") {
57 flag_flatten = true;
58 continue;
59 }
60 break;
61 }
62 if (argidx+3 != args.size() || args[argidx].compare(0, 1, "-") == 0)
63 that->cmd_error(args, argidx, "command argument error");
64
65 RTLIL::IdString gold_name = RTLIL::escape_id(args[argidx++]);
66 RTLIL::IdString gate_name = RTLIL::escape_id(args[argidx++]);
67 RTLIL::IdString miter_name = RTLIL::escape_id(args[argidx++]);
68
69 if (design->module(gold_name) == nullptr)
70 log_cmd_error("Can't find gold module %s!\n", gold_name.c_str());
71 if (design->module(gate_name) == nullptr)
72 log_cmd_error("Can't find gate module %s!\n", gate_name.c_str());
73 if (design->module(miter_name) != nullptr)
74 log_cmd_error("There is already a module %s!\n", miter_name.c_str());
75
76 RTLIL::Module *gold_module = design->module(gold_name);
77 RTLIL::Module *gate_module = design->module(gate_name);
78
79 for (auto gold_wire : gold_module->wires()) {
80 if (gold_wire->port_id == 0)
81 continue;
82 RTLIL::Wire *gate_wire = gate_module->wire(gold_wire->name);
83 if (gate_wire == nullptr)
84 goto match_gold_port_error;
85 if (gold_wire->port_input != gate_wire->port_input)
86 goto match_gold_port_error;
87 if (gold_wire->port_output != gate_wire->port_output)
88 goto match_gold_port_error;
89 if (gold_wire->width != gate_wire->width)
90 goto match_gold_port_error;
91 continue;
92 match_gold_port_error:
93 log_cmd_error("No matching port in gate module was found for %s!\n", gold_wire->name.c_str());
94 }
95
96 for (auto gate_wire : gate_module->wires()) {
97 if (gate_wire->port_id == 0)
98 continue;
99 RTLIL::Wire *gold_wire = gold_module->wire(gate_wire->name);
100 if (gold_wire == nullptr)
101 goto match_gate_port_error;
102 if (gate_wire->port_input != gold_wire->port_input)
103 goto match_gate_port_error;
104 if (gate_wire->port_output != gold_wire->port_output)
105 goto match_gate_port_error;
106 if (gate_wire->width != gold_wire->width)
107 goto match_gate_port_error;
108 continue;
109 match_gate_port_error:
110 log_cmd_error("No matching port in gold module was found for %s!\n", gate_wire->name.c_str());
111 }
112
113 log("Creating miter cell \"%s\" with gold cell \"%s\" and gate cell \"%s\".\n", RTLIL::id2cstr(miter_name), RTLIL::id2cstr(gold_name), RTLIL::id2cstr(gate_name));
114
115 RTLIL::Module *miter_module = new RTLIL::Module;
116 miter_module->name = miter_name;
117 design->add(miter_module);
118
119 RTLIL::Cell *gold_cell = miter_module->addCell(ID(gold), gold_name);
120 RTLIL::Cell *gate_cell = miter_module->addCell(ID(gate), gate_name);
121
122 RTLIL::SigSpec all_conditions;
123
124 for (auto gold_wire : gold_module->wires())
125 {
126 if (gold_wire->port_input)
127 {
128 RTLIL::Wire *w = miter_module->addWire("\\in_" + RTLIL::unescape_id(gold_wire->name), gold_wire->width);
129 w->port_input = true;
130
131 gold_cell->setPort(gold_wire->name, w);
132 gate_cell->setPort(gold_wire->name, w);
133 }
134
135 if (gold_wire->port_output)
136 {
137 RTLIL::Wire *w_gold = miter_module->addWire("\\gold_" + RTLIL::unescape_id(gold_wire->name), gold_wire->width);
138 w_gold->port_output = flag_make_outputs;
139
140 RTLIL::Wire *w_gate = miter_module->addWire("\\gate_" + RTLIL::unescape_id(gold_wire->name), gold_wire->width);
141 w_gate->port_output = flag_make_outputs;
142
143 gold_cell->setPort(gold_wire->name, w_gold);
144 gate_cell->setPort(gold_wire->name, w_gate);
145
146 RTLIL::SigSpec this_condition;
147
148 if (flag_ignore_gold_x)
149 {
150 RTLIL::SigSpec gold_x = miter_module->addWire(NEW_ID, w_gold->width);
151 for (int i = 0; i < w_gold->width; i++) {
152 RTLIL::Cell *eqx_cell = miter_module->addCell(NEW_ID, ID($eqx));
153 eqx_cell->parameters[ID::A_WIDTH] = 1;
154 eqx_cell->parameters[ID::B_WIDTH] = 1;
155 eqx_cell->parameters[ID::Y_WIDTH] = 1;
156 eqx_cell->parameters[ID::A_SIGNED] = 0;
157 eqx_cell->parameters[ID::B_SIGNED] = 0;
158 eqx_cell->setPort(ID::A, RTLIL::SigSpec(w_gold, i));
159 eqx_cell->setPort(ID::B, RTLIL::State::Sx);
160 eqx_cell->setPort(ID::Y, gold_x.extract(i, 1));
161 }
162
163 RTLIL::SigSpec gold_masked = miter_module->addWire(NEW_ID, w_gold->width);
164 RTLIL::SigSpec gate_masked = miter_module->addWire(NEW_ID, w_gate->width);
165
166 RTLIL::Cell *or_gold_cell = miter_module->addCell(NEW_ID, ID($or));
167 or_gold_cell->parameters[ID::A_WIDTH] = w_gold->width;
168 or_gold_cell->parameters[ID::B_WIDTH] = w_gold->width;
169 or_gold_cell->parameters[ID::Y_WIDTH] = w_gold->width;
170 or_gold_cell->parameters[ID::A_SIGNED] = 0;
171 or_gold_cell->parameters[ID::B_SIGNED] = 0;
172 or_gold_cell->setPort(ID::A, w_gold);
173 or_gold_cell->setPort(ID::B, gold_x);
174 or_gold_cell->setPort(ID::Y, gold_masked);
175
176 RTLIL::Cell *or_gate_cell = miter_module->addCell(NEW_ID, ID($or));
177 or_gate_cell->parameters[ID::A_WIDTH] = w_gate->width;
178 or_gate_cell->parameters[ID::B_WIDTH] = w_gate->width;
179 or_gate_cell->parameters[ID::Y_WIDTH] = w_gate->width;
180 or_gate_cell->parameters[ID::A_SIGNED] = 0;
181 or_gate_cell->parameters[ID::B_SIGNED] = 0;
182 or_gate_cell->setPort(ID::A, w_gate);
183 or_gate_cell->setPort(ID::B, gold_x);
184 or_gate_cell->setPort(ID::Y, gate_masked);
185
186 RTLIL::Cell *eq_cell = miter_module->addCell(NEW_ID, ID($eqx));
187 eq_cell->parameters[ID::A_WIDTH] = w_gold->width;
188 eq_cell->parameters[ID::B_WIDTH] = w_gate->width;
189 eq_cell->parameters[ID::Y_WIDTH] = 1;
190 eq_cell->parameters[ID::A_SIGNED] = 0;
191 eq_cell->parameters[ID::B_SIGNED] = 0;
192 eq_cell->setPort(ID::A, gold_masked);
193 eq_cell->setPort(ID::B, gate_masked);
194 eq_cell->setPort(ID::Y, miter_module->addWire(NEW_ID));
195 this_condition = eq_cell->getPort(ID::Y);
196 }
197 else
198 {
199 RTLIL::Cell *eq_cell = miter_module->addCell(NEW_ID, ID($eqx));
200 eq_cell->parameters[ID::A_WIDTH] = w_gold->width;
201 eq_cell->parameters[ID::B_WIDTH] = w_gate->width;
202 eq_cell->parameters[ID::Y_WIDTH] = 1;
203 eq_cell->parameters[ID::A_SIGNED] = 0;
204 eq_cell->parameters[ID::B_SIGNED] = 0;
205 eq_cell->setPort(ID::A, w_gold);
206 eq_cell->setPort(ID::B, w_gate);
207 eq_cell->setPort(ID::Y, miter_module->addWire(NEW_ID));
208 this_condition = eq_cell->getPort(ID::Y);
209 }
210
211 if (flag_make_outcmp)
212 {
213 RTLIL::Wire *w_cmp = miter_module->addWire("\\cmp_" + RTLIL::unescape_id(gold_wire->name));
214 w_cmp->port_output = true;
215 miter_module->connect(RTLIL::SigSig(w_cmp, this_condition));
216 }
217
218 all_conditions.append(this_condition);
219 }
220 }
221
222 if (all_conditions.size() != 1) {
223 RTLIL::Cell *reduce_cell = miter_module->addCell(NEW_ID, ID($reduce_and));
224 reduce_cell->parameters[ID::A_WIDTH] = all_conditions.size();
225 reduce_cell->parameters[ID::Y_WIDTH] = 1;
226 reduce_cell->parameters[ID::A_SIGNED] = 0;
227 reduce_cell->setPort(ID::A, all_conditions);
228 reduce_cell->setPort(ID::Y, miter_module->addWire(NEW_ID));
229 all_conditions = reduce_cell->getPort(ID::Y);
230 }
231
232 if (flag_make_assert) {
233 RTLIL::Cell *assert_cell = miter_module->addCell(NEW_ID, ID($assert));
234 assert_cell->setPort(ID::A, all_conditions);
235 assert_cell->setPort(ID::EN, State::S1);
236 }
237
238 RTLIL::Wire *w_trigger = miter_module->addWire(ID(trigger));
239 w_trigger->port_output = true;
240
241 RTLIL::Cell *not_cell = miter_module->addCell(NEW_ID, ID($not));
242 not_cell->parameters[ID::A_WIDTH] = all_conditions.size();
243 not_cell->parameters[ID::A_WIDTH] = all_conditions.size();
244 not_cell->parameters[ID::Y_WIDTH] = w_trigger->width;
245 not_cell->parameters[ID::A_SIGNED] = 0;
246 not_cell->setPort(ID::A, all_conditions);
247 not_cell->setPort(ID::Y, w_trigger);
248
249 miter_module->fixup_ports();
250
251 if (flag_flatten) {
252 log_push();
253 Pass::call_on_module(design, miter_module, "flatten -wb; opt_expr -keepdc -undriven;;");
254 log_pop();
255 }
256 }
257
create_miter_assert(struct Pass * that,std::vector<std::string> args,RTLIL::Design * design)258 void create_miter_assert(struct Pass *that, std::vector<std::string> args, RTLIL::Design *design)
259 {
260 bool flag_make_outputs = false;
261 bool flag_flatten = false;
262
263 log_header(design, "Executing MITER pass (creating miter circuit).\n");
264
265 size_t argidx;
266 for (argidx = 2; argidx < args.size(); argidx++)
267 {
268 if (args[argidx] == "-make_outputs") {
269 flag_make_outputs = true;
270 continue;
271 }
272 if (args[argidx] == "-flatten") {
273 flag_flatten = true;
274 continue;
275 }
276 break;
277 }
278 if ((argidx+1 != args.size() && argidx+2 != args.size()) || args[argidx].compare(0, 1, "-") == 0)
279 that->cmd_error(args, argidx, "command argument error");
280
281 IdString module_name = RTLIL::escape_id(args[argidx++]);
282 IdString miter_name = argidx < args.size() ? RTLIL::escape_id(args[argidx++]) : "";
283
284 if (design->module(module_name) == nullptr)
285 log_cmd_error("Can't find module %s!\n", module_name.c_str());
286 if (!miter_name.empty() && design->module(miter_name) != nullptr)
287 log_cmd_error("There is already a module %s!\n", miter_name.c_str());
288
289 Module *module = design->module(module_name);
290
291 if (!miter_name.empty()) {
292 module = module->clone();
293 module->name = miter_name;
294 design->add(module);
295 }
296
297 if (!flag_make_outputs)
298 for (auto wire : module->wires())
299 wire->port_output = false;
300
301 Wire *trigger = module->addWire(ID(trigger));
302 trigger->port_output = true;
303 module->fixup_ports();
304
305 if (flag_flatten) {
306 log_push();
307 Pass::call_on_module(design, module, "flatten -wb;;");
308 log_pop();
309 }
310
311 SigSpec assert_signals, assume_signals;
312 vector<Cell*> cell_list = module->cells();
313 for (auto cell : cell_list)
314 {
315 if (!cell->type.in(ID($assert), ID($assume)))
316 continue;
317
318 SigBit is_active = module->Nex(NEW_ID, cell->getPort(ID::A), State::S1);
319 SigBit is_enabled = module->Eqx(NEW_ID, cell->getPort(ID::EN), State::S1);
320
321 if (cell->type == ID($assert)) {
322 assert_signals.append(module->And(NEW_ID, is_active, is_enabled));
323 } else {
324 assume_signals.append(module->And(NEW_ID, is_active, is_enabled));
325 }
326
327 module->remove(cell);
328 }
329
330 if (assume_signals.empty())
331 {
332 module->addReduceOr(NEW_ID, assert_signals, trigger);
333 }
334 else
335 {
336 Wire *assume_q = module->addWire(NEW_ID);
337 assume_q->attributes[ID::init] = State::S0;
338 assume_signals.append(assume_q);
339
340 SigSpec assume_nok = module->ReduceOr(NEW_ID, assume_signals);
341 SigSpec assume_ok = module->Not(NEW_ID, assume_nok);
342 module->addFf(NEW_ID, assume_nok, assume_q);
343
344 SigSpec assert_fail = module->ReduceOr(NEW_ID, assert_signals);
345 module->addAnd(NEW_ID, assert_fail, assume_ok, trigger);
346 }
347
348 if (flag_flatten) {
349 log_push();
350 Pass::call_on_module(design, module, "opt_expr -keepdc -undriven;;");
351 log_pop();
352 }
353 }
354
355 struct MiterPass : public Pass {
MiterPassMiterPass356 MiterPass() : Pass("miter", "automatically create a miter circuit") { }
helpMiterPass357 void help() override
358 {
359 // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
360 log("\n");
361 log(" miter -equiv [options] gold_name gate_name miter_name\n");
362 log("\n");
363 log("Creates a miter circuit for equivalence checking. The gold- and gate- modules\n");
364 log("must have the same interfaces. The miter circuit will have all inputs of the\n");
365 log("two source modules, prefixed with 'in_'. The miter circuit has a 'trigger'\n");
366 log("output that goes high if an output mismatch between the two source modules is\n");
367 log("detected.\n");
368 log("\n");
369 log(" -ignore_gold_x\n");
370 log(" a undef (x) bit in the gold module output will match any value in\n");
371 log(" the gate module output.\n");
372 log("\n");
373 log(" -make_outputs\n");
374 log(" also route the gold- and gate-outputs to 'gold_*' and 'gate_*' outputs\n");
375 log(" on the miter circuit.\n");
376 log("\n");
377 log(" -make_outcmp\n");
378 log(" also create a cmp_* output for each gold/gate output pair.\n");
379 log("\n");
380 log(" -make_assert\n");
381 log(" also create an 'assert' cell that checks if trigger is always low.\n");
382 log("\n");
383 log(" -flatten\n");
384 log(" call 'flatten -wb; opt_expr -keepdc -undriven;;' on the miter circuit.\n");
385 log("\n");
386 log("\n");
387 log(" miter -assert [options] module [miter_name]\n");
388 log("\n");
389 log("Creates a miter circuit for property checking. All input ports are kept,\n");
390 log("output ports are discarded. An additional output 'trigger' is created that\n");
391 log("goes high when an assert is violated. Without a miter_name, the existing\n");
392 log("module is modified.\n");
393 log("\n");
394 log(" -make_outputs\n");
395 log(" keep module output ports.\n");
396 log("\n");
397 log(" -flatten\n");
398 log(" call 'flatten -wb; opt_expr -keepdc -undriven;;' on the miter circuit.\n");
399 log("\n");
400 }
executeMiterPass401 void execute(std::vector<std::string> args, RTLIL::Design *design) override
402 {
403 if (args.size() > 1 && args[1] == "-equiv") {
404 create_miter_equiv(this, args, design);
405 return;
406 }
407
408 if (args.size() > 1 && args[1] == "-assert") {
409 create_miter_assert(this, args, design);
410 return;
411 }
412
413 log_cmd_error("Missing mode parameter!\n");
414 }
415 } MiterPass;
416
417 PRIVATE_NAMESPACE_END
418