diff options
| -rw-r--r-- | passes/equiv/equiv_induct.cc | 12 | ||||
| -rw-r--r-- | passes/equiv/equiv_make.cc | 34 |
2 files changed, 46 insertions, 0 deletions
diff --git a/passes/equiv/equiv_induct.cc b/passes/equiv/equiv_induct.cc index ccf4f957f..38a52d754 100644 --- a/passes/equiv/equiv_induct.cc +++ b/passes/equiv/equiv_induct.cc @@ -136,6 +136,18 @@ struct EquivInductPass : public Pass { log(" -seq <N>\n"); log(" the max. number of time steps to be considered (default = 4)\n"); log("\n"); + log("This command is very effective in proving complex sequential circuits, when\n"); + log("the internal state of the circuit quickly propagates to $equiv cells.\n"); + log("\n"); + log("However, this command uses a weak definition of 'equivalence': This command\n"); + log("proves that the two circuits will not diverge after they produce equal\n"); + log("outputs (observable points via $equiv) for at least <N> cycles (the <N>\n"); + log("specified via -seq).\n"); + log("\n"); + log("Combined with simulation this is very powerful because simulation can give\n"); + log("you confidence that the circuits start out synced for at least <N> cycles\n"); + log("after reset.\n"); + log("\n"); } virtual void execute(std::vector<std::string> args, Design *design) { diff --git a/passes/equiv/equiv_make.cc b/passes/equiv/equiv_make.cc index 07374cfc3..be1480e94 100644 --- a/passes/equiv/equiv_make.cc +++ b/passes/equiv/equiv_make.cc @@ -176,11 +176,45 @@ struct EquivMakeWorker } } + void find_undriven_nets() + { + pool<SigBit> undriven_bits; + SigMap assign_map(equiv_mod); + + for (auto wire : equiv_mod->wires()) { + for (auto bit : assign_map(wire)) + if (bit.wire) + undriven_bits.insert(bit); + } + + for (auto wire : equiv_mod->wires()) { + if (wire->port_input) + for (auto bit : assign_map(wire)) + undriven_bits.erase(bit); + } + + for (auto cell : equiv_mod->cells()) { + for (auto &conn : cell->connections()) + if (!ct.cell_known(cell->type) || ct.cell_output(cell->type, conn.first)) + for (auto bit : assign_map(conn.second)) + undriven_bits.erase(bit); + } + + SigSpec undriven_sig(undriven_bits); + undriven_sig.sort_and_unify(); + + for (auto chunk : undriven_sig.chunks()) { + log("Setting undriven nets to undef: %s\n", log_signal(chunk)); + equiv_mod->connect(chunk, SigSpec(State::Sx, chunk.width)); + } + } + void run() { copy_to_equiv(); find_same_wires(); find_same_cells(); + find_undriven_nets(); } }; |