From bc86b4a7e9c847180e6fd7ed81e0a15d5aee00a0 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Sat, 31 Jan 2015 13:58:04 +0100
Subject: [PATCH] Added "equiv_induct -undef"

---
 kernel/sigtools.h            |  2 +-
 passes/equiv/equiv_induct.cc | 55 ++++++++++++++++++++++++++++++++----
 2 files changed, 51 insertions(+), 6 deletions(-)

diff --git a/kernel/sigtools.h b/kernel/sigtools.h
index c38736e70..f92a87dbb 100644
--- a/kernel/sigtools.h
+++ b/kernel/sigtools.h
@@ -129,7 +129,7 @@ struct SigPool
 		return sig;
 	}
 
-	size_t size()
+	size_t size() const
 	{
 		return bits.size();
 	}
diff --git a/passes/equiv/equiv_induct.cc b/passes/equiv/equiv_induct.cc
index ff91d11af..c5b4eda72 100644
--- a/passes/equiv/equiv_induct.cc
+++ b/passes/equiv/equiv_induct.cc
@@ -40,15 +40,18 @@ struct EquivInductWorker
 
 	dict<int, int> ez_step_is_consistent;
 	pool<Cell*> cell_warn_cache;
+	SigPool undriven_signals;
 
-	EquivInductWorker(Module *module, const pool<Cell*> &unproven_equiv_cells, int max_seq) : module(module), sigmap(module),
+	EquivInductWorker(Module *module, const pool<Cell*> &unproven_equiv_cells, bool model_undef, int max_seq) : module(module), sigmap(module),
 			cells(module->selected_cells()), workset(unproven_equiv_cells), satgen(&ez, &sigmap), max_seq(max_seq), success_counter(0)
 	{
+		satgen.model_undef = model_undef;
 	}
 
 	void create_timestep(int step)
 	{
 		vector<int> ez_equal_terms;
+
 		for (auto cell : cells) {
 			if (!satgen.importCell(cell, step) && !cell_warn_cache.count(cell)) {
 				log_warning("No SAT model available for cell %s (%s).\n", log_id(cell), log_id(cell->type));
@@ -60,11 +63,19 @@ struct EquivInductWorker
 				if (bit_a != bit_b) {
 					int ez_a = satgen.importSigBit(bit_a, step);
 					int ez_b = satgen.importSigBit(bit_b, step);
-					ez_equal_terms.push_back(ez.IFF(ez_a, ez_b));
+					int cond = ez.IFF(ez_a, ez_b);
+					if (satgen.model_undef)
+						cond = ez.OR(cond, satgen.importUndefSigBit(bit_a, step));
+					ez_equal_terms.push_back(cond);
 				}
 			}
 		}
 
+		if (satgen.model_undef) {
+			for (auto bit : undriven_signals.export_all())
+				ez.assume(ez.NOT(satgen.importUndefSigBit(bit, step)));
+		}
+
 		log_assert(!ez_step_is_consistent.count(step));
 		ez_step_is_consistent[step] = ez.expression(ez.OpAnd, ez_equal_terms);
 	}
@@ -73,7 +84,28 @@ struct EquivInductWorker
 	{
 		log("Found %d unproven $equiv cells in module %s:\n", GetSize(workset), log_id(module));
 
+		if (satgen.model_undef) {
+			for (auto cell : cells)
+				if (yosys_celltypes.cell_known(cell->type))
+					for (auto &conn : cell->connections())
+						if (yosys_celltypes.cell_input(cell->type, conn.first))
+							undriven_signals.add(sigmap(conn.second));
+			for (auto cell : cells)
+				if (yosys_celltypes.cell_known(cell->type))
+					for (auto &conn : cell->connections())
+						if (yosys_celltypes.cell_output(cell->type, conn.first))
+							undriven_signals.del(sigmap(conn.second));
+		}
+
 		create_timestep(1);
+
+		if (satgen.model_undef) {
+			for (auto bit : satgen.initial_state.export_all())
+				ez.assume(ez.NOT(satgen.importUndefSigBit(bit, 1)));
+			log("  Undef modelling: force def on %d initial reg values and %d inputs.\n",
+				GetSize(satgen.initial_state), GetSize(undriven_signals));
+		}
+
 		for (int step = 1; step <= max_seq; step++)
 		{
 			ez.assume(ez_step_is_consistent[step]);
@@ -107,11 +139,16 @@ struct EquivInductWorker
 			SigBit bit_a = sigmap(cell->getPort("\\A")).to_single_sigbit();
 			SigBit bit_b = sigmap(cell->getPort("\\B")).to_single_sigbit();
 
+			log("  Trying to prove $equiv for %s:", log_signal(sigmap(cell->getPort("\\Y"))));
+
 			int ez_a = satgen.importSigBit(bit_a, max_seq+1);
 			int ez_b = satgen.importSigBit(bit_b, max_seq+1);
+			int cond = ez.XOR(ez_a, ez_b);
 
-			log("  Trying to prove $equiv for %s:", log_signal(sigmap(cell->getPort("\\Y"))));
-			if (!ez.solve(ez.XOR(ez_a, ez_b))) {
+			if (satgen.model_undef)
+				cond = ez.AND(cond, ez.NOT(satgen.importUndefSigBit(bit_a, max_seq+1)));
+
+			if (!ez.solve(cond)) {
 				log(" success!\n");
 				cell->setPort("\\B", cell->getPort("\\A"));
 				success_counter++;
@@ -135,6 +172,9 @@ struct EquivInductPass : public Pass {
 		log("Only selected $equiv cells are proven and only selected cells are used to\n");
 		log("perform the proof.\n");
 		log("\n");
+		log("    -undef\n");
+		log("        enable modelling of undef states\n");
+		log("\n");
 		log("    -seq <N>\n");
 		log("        the max. number of time steps to be considered (default = 4)\n");
 		log("\n");
@@ -154,12 +194,17 @@ struct EquivInductPass : public Pass {
 	virtual void execute(std::vector<std::string> args, Design *design)
 	{
 		int success_counter = 0;
+		bool model_undef = false;
 		int max_seq = 4;
 
 		log_header("Executing EQUIV_INDUCT pass.\n");
 
 		size_t argidx;
 		for (argidx = 1; argidx < args.size(); argidx++) {
+			if (args[argidx] == "-undef") {
+				model_undef = true;
+				continue;
+			}
 			if (args[argidx] == "-seq" && argidx+1 < args.size()) {
 				max_seq = atoi(args[++argidx].c_str());
 				continue;
@@ -183,7 +228,7 @@ struct EquivInductPass : public Pass {
 				continue;
 			}
 
-			EquivInductWorker worker(module, unproven_equiv_cells, max_seq);
+			EquivInductWorker worker(module, unproven_equiv_cells, model_undef, max_seq);
 			worker.run();
 			success_counter += worker.success_counter;
 		}
-- 
2.30.2