From fbf5d89587decd2886d501d8c6e1cde076a5476f Mon Sep 17 00:00:00 2001 From: George Rennie Date: Thu, 23 Dec 2021 01:10:32 +0000 Subject: [PATCH] equiv_make: Add -make_assert option This adds a -make_assert flag to equiv_make. When used, the pass generates $eqx and $assert cells to encode equivalence instead of $equiv. --- passes/equiv/equiv_make.cc | 92 +++++++++++++++++-------- tests/various/equiv_make_make_assert.ys | 32 +++++++++ 2 files changed, 97 insertions(+), 27 deletions(-) create mode 100644 tests/various/equiv_make_make_assert.ys diff --git a/passes/equiv/equiv_make.cc b/passes/equiv/equiv_make.cc index 7ef2827bf..56bc50ced 100644 --- a/passes/equiv/equiv_make.cc +++ b/passes/equiv/equiv_make.cc @@ -33,6 +33,7 @@ struct EquivMakeWorker bool inames; vector blacklists; vector encfiles; + bool make_assert; pool blacklist_names; dict> encdata; @@ -143,6 +144,12 @@ struct EquivMakeWorker delete gate_clone; } + void add_eq_assertion(const SigSpec &gold_sig, const SigSpec &gate_sig) + { + auto eq_wire = equiv_mod->Eqx(NEW_ID, gold_sig, gate_sig); + equiv_mod->addAssert(NEW_ID_SUFFIX("assert"), eq_wire, State::S1); + } + void find_same_wires() { SigMap assign_map(equiv_mod); @@ -240,15 +247,24 @@ struct EquivMakeWorker if (gold_wire->port_output || gate_wire->port_output) { - Wire *wire = equiv_mod->addWire(id, gold_wire->width); - wire->port_output = true; gold_wire->port_input = false; gate_wire->port_input = false; gold_wire->port_output = false; gate_wire->port_output = false; - for (int i = 0; i < wire->width; i++) - equiv_mod->addEquiv(NEW_ID, SigSpec(gold_wire, i), SigSpec(gate_wire, i), SigSpec(wire, i)); + Wire *wire = equiv_mod->addWire(id, gold_wire->width); + wire->port_output = true; + + if (make_assert) + { + add_eq_assertion(gold_wire, gate_wire); + equiv_mod->connect(wire, gold_wire); + } + else + { + for (int i = 0; i < wire->width; i++) + equiv_mod->addEquiv(NEW_ID, SigSpec(gold_wire, i), SigSpec(gate_wire, i), SigSpec(wire, i)); + } rd_signal_map.add(assign_map(gold_wire), wire); rd_signal_map.add(assign_map(gate_wire), wire); @@ -265,26 +281,31 @@ struct EquivMakeWorker } else { - Wire *wire = equiv_mod->addWire(id, gold_wire->width); - SigSpec rdmap_gold, rdmap_gate, rdmap_equiv; + if (make_assert) + add_eq_assertion(gold_wire, gate_wire); - for (int i = 0; i < wire->width; i++) { - if (undriven_bits.count(assign_map(SigBit(gold_wire, i)))) { - log(" Skipping signal bit %s [%d]: undriven on gold side.\n", id2cstr(gold_wire->name), i); - continue; + else { + Wire *wire = equiv_mod->addWire(id, gold_wire->width); + SigSpec rdmap_gold, rdmap_gate, rdmap_equiv; + + for (int i = 0; i < wire->width; i++) { + if (undriven_bits.count(assign_map(SigBit(gold_wire, i)))) { + log(" Skipping signal bit %s [%d]: undriven on gold side.\n", id2cstr(gold_wire->name), i); + continue; + } + if (undriven_bits.count(assign_map(SigBit(gate_wire, i)))) { + log(" Skipping signal bit %s [%d]: undriven on gate side.\n", id2cstr(gate_wire->name), i); + continue; + } + equiv_mod->addEquiv(NEW_ID, SigSpec(gold_wire, i), SigSpec(gate_wire, i), SigSpec(wire, i)); + rdmap_gold.append(SigBit(gold_wire, i)); + rdmap_gate.append(SigBit(gate_wire, i)); + rdmap_equiv.append(SigBit(wire, i)); } - if (undriven_bits.count(assign_map(SigBit(gate_wire, i)))) { - log(" Skipping signal bit %s [%d]: undriven on gate side.\n", id2cstr(gate_wire->name), i); - continue; - } - equiv_mod->addEquiv(NEW_ID, SigSpec(gold_wire, i), SigSpec(gate_wire, i), SigSpec(wire, i)); - rdmap_gold.append(SigBit(gold_wire, i)); - rdmap_gate.append(SigBit(gate_wire, i)); - rdmap_equiv.append(SigBit(wire, i)); + + rd_signal_map.add(rdmap_gold, rdmap_equiv); + rd_signal_map.add(rdmap_gate, rdmap_equiv); } - - rd_signal_map.add(rdmap_gold, rdmap_equiv); - rd_signal_map.add(rdmap_gate, rdmap_equiv); } } @@ -353,12 +374,20 @@ struct EquivMakeWorker continue; } - for (int i = 0; i < GetSize(gold_sig); i++) - if (gold_sig[i] != gate_sig[i]) { - Wire *w = equiv_mod->addWire(NEW_ID); - equiv_mod->addEquiv(NEW_ID, gold_sig[i], gate_sig[i], w); - gold_sig[i] = w; - } + if (make_assert) + { + if (gold_sig != gate_sig) + add_eq_assertion(gold_sig, gate_sig); + } + else + { + for (int i = 0; i < GetSize(gold_sig); i++) + if (gold_sig[i] != gate_sig[i]) { + Wire *w = equiv_mod->addWire(NEW_ID); + equiv_mod->addEquiv(NEW_ID, gold_sig[i], gate_sig[i], w); + gold_sig[i] = w; + } + } gold_cell->setPort(gold_conn.first, gold_sig); } @@ -486,6 +515,10 @@ struct EquivMakePass : public Pass { log(" Match FSM encodings using the description from the file.\n"); log(" See 'help fsm_recode' for details.\n"); log("\n"); + log(" -make_assert\n"); + log(" Check equivalence with $assert cells instead of $equiv.\n"); + log(" $eqx (===) is used to compare signals."); + log("\n"); log("Note: The circuit created by this command is not a miter (with something like\n"); log("a trigger output), but instead uses $equiv cells to encode the equivalence\n"); log("checking problem. Use 'miter -equiv' if you want to create a miter circuit.\n"); @@ -496,6 +529,7 @@ struct EquivMakePass : public Pass { EquivMakeWorker worker; worker.ct.setup(design); worker.inames = false; + worker.make_assert = false; size_t argidx; for (argidx = 1; argidx < args.size(); argidx++) @@ -512,6 +546,10 @@ struct EquivMakePass : public Pass { worker.encfiles.push_back(args[++argidx]); continue; } + if (args[argidx] == "-make_assert") { + worker.make_assert = true; + continue; + } break; } diff --git a/tests/various/equiv_make_make_assert.ys b/tests/various/equiv_make_make_assert.ys new file mode 100644 index 000000000..1c2efa723 --- /dev/null +++ b/tests/various/equiv_make_make_assert.ys @@ -0,0 +1,32 @@ +read_verilog <