Merge pull request #3565 from jix/sat-def-formal

sat: Add -set-def-formal option to force defined $any* outputs

3 files changed, 46 insertions, 10 deletions

diff --git a/kernel/satgen.cc b/kernel/satgen.cc
index 05eeca76e..2a1fd1711 100644
--- a/kernel/satgen.cc
+++ b/kernel/satgen.cc
@@ -1187,6 +1187,10 @@ bool SatGen::importCell(RTLIL::Cell *cell, int timestep)
 		if (timestep == 1)
 		{
 			initial_state.add((*sigmap)(cell->getPort(ID::Q)));
+			if (model_undef && def_formal) {
+				std::vector<int> undef_q = importUndefSigSpec(cell->getPort(ID::Q), timestep);
+				ez->assume(ez->NOT(ez->vec_reduce_or(undef_q)));
+			}
 		}
 		else
 		{
@@ -1254,13 +1258,18 @@ bool SatGen::importCell(RTLIL::Cell *cell, int timestep)
 
 	if (cell->type == ID($anyconst))
 	{
-		if (timestep < 2)
+		if (timestep < 2) {
+			if (model_undef && def_formal) {
+				std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
+				ez->assume(ez->NOT(ez->vec_reduce_or(undef_y)));
+			}
 			return true;
+		}
 
 		std::vector<int> d = importDefSigSpec(cell->getPort(ID::Y), timestep-1);
 		std::vector<int> q = importDefSigSpec(cell->getPort(ID::Y), timestep);
 
-		std::vector<int> qq = model_undef ? ez->vec_var(q.size()) : q;
+		std::vector<int> qq = (model_undef && !def_formal) ? ez->vec_var(q.size()) : q;
 		ez->assume(ez->vec_eq(d, qq));
 
 		if (model_undef)
@@ -1268,14 +1277,24 @@ bool SatGen::importCell(RTLIL::Cell *cell, int timestep)
 			std::vector<int> undef_d = importUndefSigSpec(cell->getPort(ID::Y), timestep-1);
 			std::vector<int> undef_q = importUndefSigSpec(cell->getPort(ID::Y), timestep);
 
-			ez->assume(ez->vec_eq(undef_d, undef_q));
-			undefGating(q, qq, undef_q);
+			if (def_formal) {
+				for (auto &undef_q_bit : undef_q)
+					ez->SET(ez->CONST_FALSE, undef_q_bit);
+			} else {
+				ez->assume(ez->vec_eq(undef_d, undef_q));
+				undefGating(q, qq, undef_q);
+			}
 		}
 		return true;
 	}
 
 	if (cell->type == ID($anyseq))
 	{
+		if (model_undef && def_formal) {
+			std::vector<int> undef_q = importUndefSigSpec(cell->getPort(ID::Y), timestep);
+			for (auto &undef_q_bit : undef_q)
+				ez->SET(ez->CONST_FALSE, undef_q_bit);
+		}
 		return true;
 	}
 
diff --git a/kernel/satgen.h b/kernel/satgen.h
index da2cec222..8a89ff9db 100644
--- a/kernel/satgen.h
+++ b/kernel/satgen.h
@@ -73,6 +73,7 @@ struct SatGen
 	std::map<std::pair<std::string, int>, bool> initstates;
 	bool ignore_div_by_zero;
 	bool model_undef;
+	bool def_formal = false;
 
 	SatGen(ezSAT *ez, SigMap *sigmap, std::string prefix = std::string()) :
 			ez(ez), sigmap(sigmap), prefix(prefix), ignore_div_by_zero(false), model_undef(false)
diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc
index e10517d72..69f81e3df 100644
--- a/passes/sat/sat.cc
+++ b/passes/sat/sat.cc
@@ -65,11 +65,12 @@ struct SatHelper
 	int max_timestep, timeout;
 	bool gotTimeout;
 
-	SatHelper(RTLIL::Design *design, RTLIL::Module *module, bool enable_undef) :
+	SatHelper(RTLIL::Design *design, RTLIL::Module *module, bool enable_undef, bool set_def_formal) :
 		design(design), module(module), sigmap(module), ct(design), satgen(ez.get(), &sigmap)
 	{
 		this->enable_undef = enable_undef;
 		satgen.model_undef = enable_undef;
+		satgen.def_formal = set_def_formal;
 		set_init_def = false;
 		set_init_undef = false;
 		set_init_zero = false;
@@ -254,7 +255,13 @@ struct SatHelper
 
 		if (initstate)
 		{
-			RTLIL::SigSpec big_lhs, big_rhs;
+			RTLIL::SigSpec big_lhs, big_rhs, forced_def;
+
+			// Check for $anyinit cells that are forced to be defined
+			if (set_init_undef && satgen.def_formal)
+				for (auto cell : module->cells())
+					if (cell->type == ID($anyinit))
+						forced_def.append(sigmap(cell->getPort(ID::Q)));
 
 			for (auto wire : module->wires())
 			{
@@ -323,6 +330,7 @@ struct SatHelper
 			if (set_init_undef) {
 				RTLIL::SigSpec rem = satgen.initial_state.export_all();
 				rem.remove(big_lhs);
+				rem.remove(forced_def);
 				big_lhs.append(rem);
 				big_rhs.append(RTLIL::SigSpec(RTLIL::State::Sx, rem.size()));
 			}
@@ -933,6 +941,9 @@ struct SatPass : public Pass {
 		log("    -set-def-inputs\n");
 		log("        add -set-def constraints for all module inputs\n");
 		log("\n");
+		log("    -set-def-formal\n");
+		log("        add -set-def constraints for formal $anyinit, $anyconst, $anyseq cells\n");
+		log("\n");
 		log("    -show <signal>\n");
 		log("        show the model for the specified signal. if no -show option is\n");
 		log("        passed then a set of signals to be shown is automatically selected.\n");
@@ -1068,7 +1079,7 @@ struct SatPass : public Pass {
 		std::map<int, std::vector<std::string>> unsets_at, sets_def_at, sets_any_undef_at, sets_all_undef_at;
 		std::vector<std::string> shows, sets_def, sets_any_undef, sets_all_undef;
 		int loopcount = 0, seq_len = 0, maxsteps = 0, initsteps = 0, timeout = 0, prove_skip = 0;
-		bool verify = false, fail_on_timeout = false, enable_undef = false, set_def_inputs = false;
+		bool verify = false, fail_on_timeout = false, enable_undef = false, set_def_inputs = false, set_def_formal = false;
 		bool ignore_div_by_zero = false, set_init_undef = false, set_init_zero = false, max_undef = false;
 		bool tempinduct = false, prove_asserts = false, show_inputs = false, show_outputs = false;
 		bool show_regs = false, show_public = false, show_all = false;
@@ -1141,6 +1152,11 @@ struct SatPass : public Pass {
 				set_def_inputs = true;
 				continue;
 			}
+			if (args[argidx] == "-set-def-formal") {
+				enable_undef = true;
+				set_def_formal = true;
+				continue;
+			}
 			if (args[argidx] == "-set" && argidx+2 < args.size()) {
 				std::string lhs = args[++argidx];
 				std::string rhs = args[++argidx];
@@ -1380,8 +1396,8 @@ struct SatPass : public Pass {
 			if (loopcount > 0 || max_undef)
 				log_cmd_error("The options -max, -all, and -max_undef are not supported for temporal induction proofs!\n");
 
-			SatHelper basecase(design, module, enable_undef);
-			SatHelper inductstep(design, module, enable_undef);
+			SatHelper basecase(design, module, enable_undef, set_def_formal);
+			SatHelper inductstep(design, module, enable_undef, set_def_formal);
 
 			basecase.sets = sets;
 			basecase.set_assumes = set_assumes;
@@ -1570,7 +1586,7 @@ struct SatPass : public Pass {
 			if (maxsteps > 0)
 				log_cmd_error("The options -maxsteps is only supported for temporal induction proofs!\n");
 
-			SatHelper sathelper(design, module, enable_undef);
+			SatHelper sathelper(design, module, enable_undef, set_def_formal);
 
 			sathelper.sets = sets;
 			sathelper.set_assumes = set_assumes;