Improvements in equiv_make, equiv_induct

2 files changed, 46 insertions, 0 deletions

diff --git a/passes/equiv/equiv_induct.cc b/passes/equiv/equiv_induct.cc
index ccf4f957..38a52d75 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 07374cfc..be1480e9 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();
 	}
 };