Improvements in equiv_make, equiv_induct

diff --git a/passes/equiv/equiv_induct.cc b/passes/equiv/equiv_induct.cc
index ccf4f957feba2a693baaa04581745e28cf179df0..38a52d7542692db0bfa5e986fa820f65d8f6092d 100644 (file)
--- 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 07374cfc343c6fe25f0f89ca294971b61dfce756..be1480e9425825f72763fb6207eef21cada48817 100644 (file)
--- 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();
        }
 };