diff options
Diffstat (limited to 'passes/equiv/equiv_make.cc')
| -rw-r--r-- | passes/equiv/equiv_make.cc | 185 |
1 files changed, 77 insertions, 108 deletions
diff --git a/passes/equiv/equiv_make.cc b/passes/equiv/equiv_make.cc index 7ef2827bf..e15e510be 100644 --- a/passes/equiv/equiv_make.cc +++ b/passes/equiv/equiv_make.cc @@ -33,6 +33,7 @@ struct EquivMakeWorker bool inames; vector<string> blacklists; vector<string> encfiles; + bool make_assert; pool<IdString> blacklist_names; dict<IdString, dict<Const, Const>> encdata; @@ -40,16 +41,6 @@ struct EquivMakeWorker pool<SigBit> undriven_bits; SigMap assign_map; - dict<SigBit, pool<Cell*>> bit2driven; // map: bit <--> and its driven cells - - CellTypes comb_ct; - - EquivMakeWorker() - { - comb_ct.setup_internals(); - comb_ct.setup_stdcells(); - } - void read_blacklists() { for (auto fn : blacklists) @@ -143,10 +134,17 @@ 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); SigMap rd_signal_map; + SigPool primary_inputs; // list of cells without added $equiv cells auto cells_list = equiv_mod->cells().to_vector(); @@ -240,15 +238,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); @@ -262,57 +269,53 @@ struct EquivMakeWorker gate_wire->port_input = false; equiv_mod->connect(gold_wire, wire); equiv_mod->connect(gate_wire, wire); + primary_inputs.add(assign_map(gold_wire)); + primary_inputs.add(assign_map(gate_wire)); + primary_inputs.add(wire); } 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; - } - 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; + 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)); } - 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); + } } } - init_bit2driven(); - - pool<Cell*> visited_cells; for (auto c : cells_list) for (auto &conn : c->connections()) if (!ct.cell_output(c->type, conn.first)) { SigSpec old_sig = assign_map(conn.second); SigSpec new_sig = rd_signal_map(old_sig); - - if(old_sig != new_sig) { - SigSpec tmp_sig = old_sig; - for (int i = 0; i < GetSize(old_sig); i++) { - SigBit old_bit = old_sig[i], new_bit = new_sig[i]; - - visited_cells.clear(); - if (check_signal_in_fanout(visited_cells, old_bit, new_bit)) - continue; - - log("Changing input %s of cell %s (%s): %s -> %s\n", - log_id(conn.first), log_id(c), log_id(c->type), - log_signal(old_bit), log_signal(new_bit)); - - tmp_sig[i] = new_bit; - } - c->setPort(conn.first, tmp_sig); + for (int i = 0; i < GetSize(old_sig); i++) + if (primary_inputs.check(old_sig[i])) + new_sig[i] = old_sig[i]; + if (old_sig != new_sig) { + log("Changing input %s of cell %s (%s): %s -> %s\n", + log_id(conn.first), log_id(c), log_id(c->type), + log_signal(old_sig), log_signal(new_sig)); + c->setPort(conn.first, new_sig); } } @@ -353,12 +356,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); } @@ -403,57 +414,6 @@ struct EquivMakeWorker } } - void init_bit2driven() - { - for (auto cell : equiv_mod->cells()) { - if (!ct.cell_known(cell->type) && !cell->type.in(ID($dff), ID($_DFF_P_), ID($_DFF_N_), ID($ff), ID($_FF_))) - continue; - for (auto &conn : cell->connections()) - { - if (yosys_celltypes.cell_input(cell->type, conn.first)) - for (auto bit : assign_map(conn.second)) - { - bit2driven[bit].insert(cell); - } - } - } - } - - bool check_signal_in_fanout(pool<Cell*> & visited_cells, SigBit source_bit, SigBit target_bit) - { - if (source_bit == target_bit) - return true; - - if (bit2driven.count(source_bit) == 0) - return false; - - auto driven_cells = bit2driven.at(source_bit); - for (auto driven_cell: driven_cells) - { - bool is_comb = comb_ct.cell_known(driven_cell->type); - if (!is_comb) - continue; - - if (visited_cells.count(driven_cell) > 0) - continue; - visited_cells.insert(driven_cell); - - for (auto &conn: driven_cell->connections()) - { - if (yosys_celltypes.cell_input(driven_cell->type, conn.first)) - continue; - - for (auto bit: conn.second) { - bool is_in_fanout = check_signal_in_fanout(visited_cells, bit, target_bit); - if (is_in_fanout == true) - return true; - } - } - } - - return false; - } - void run() { copy_to_equiv(); @@ -486,6 +446,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 +460,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 +477,10 @@ struct EquivMakePass : public Pass { worker.encfiles.push_back(args[++argidx]); continue; } + if (args[argidx] == "-make_assert") { + worker.make_assert = true; + continue; + } break; } |