Added sat -set-def/-set-*-undef support

1 files changed, 66 insertions, 5 deletions

diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc
index e3b941f5b..0a8006ebb 100644
--- a/passes/sat/sat.cc
+++ b/passes/sat/sat.cc
@@ -202,6 +202,71 @@ struct SatHelper
 		check_undef_enabled(big_lhs), check_undef_enabled(big_rhs);
 		ez.assume(satgen.signals_eq(big_lhs, big_rhs, timestep));
 
+		// 0 = sets_def
+		// 1 = sets_any_undef
+		// 2 = sets_all_undef
+		std::set<RTLIL::SigSpec> sets_def_undef[3];
+
+		for (auto &s : sets_def) {
+			RTLIL::SigSpec sig;
+			if (!RTLIL::SigSpec::parse(sig, module, s))
+				log_cmd_error("Failed to parse set-def expression `%s'.\n", s.c_str());
+			sets_def_undef[0].insert(sig);
+		}
+
+		for (auto &s : sets_any_undef) {
+			RTLIL::SigSpec sig;
+			if (!RTLIL::SigSpec::parse(sig, module, s))
+				log_cmd_error("Failed to parse set-def expression `%s'.\n", s.c_str());
+			sets_def_undef[1].insert(sig);
+		}
+
+		for (auto &s : sets_all_undef) {
+			RTLIL::SigSpec sig;
+			if (!RTLIL::SigSpec::parse(sig, module, s))
+				log_cmd_error("Failed to parse set-def expression `%s'.\n", s.c_str());
+			sets_def_undef[2].insert(sig);
+		}
+
+		for (auto &s : sets_def_at[timestep]) {
+			RTLIL::SigSpec sig;
+			if (!RTLIL::SigSpec::parse(sig, module, s))
+				log_cmd_error("Failed to parse set-def expression `%s'.\n", s.c_str());
+			sets_def_undef[0].insert(sig);
+			sets_def_undef[1].erase(sig);
+			sets_def_undef[2].erase(sig);
+		}
+
+		for (auto &s : sets_any_undef_at[timestep]) {
+			RTLIL::SigSpec sig;
+			if (!RTLIL::SigSpec::parse(sig, module, s))
+				log_cmd_error("Failed to parse set-def expression `%s'.\n", s.c_str());
+			sets_def_undef[0].erase(sig);
+			sets_def_undef[1].insert(sig);
+			sets_def_undef[2].erase(sig);
+		}
+
+		for (auto &s : sets_all_undef_at[timestep]) {
+			RTLIL::SigSpec sig;
+			if (!RTLIL::SigSpec::parse(sig, module, s))
+				log_cmd_error("Failed to parse set-def expression `%s'.\n", s.c_str());
+			sets_def_undef[0].erase(sig);
+			sets_def_undef[1].erase(sig);
+			sets_def_undef[2].insert(sig);
+		}
+
+		for (int t = 0; t < 3; t++)
+		for (auto &sig : sets_def_undef[t]) {
+			log("Import %s constraint for timestep: %s\n", t == 0 ? "def" : t == 1 ? "any_undef" : "all_undef", log_signal(sig));
+			std::vector<int> undef_sig = satgen.importUndefSigSpec(sig, timestep);
+			if (t == 0)
+				ez.assume(ez.NOT(ez.expression(ezSAT::OpOr, undef_sig)));
+			if (t == 1)
+				ez.assume(ez.expression(ezSAT::OpOr, undef_sig));
+			if (t == 2)
+				ez.assume(ez.expression(ezSAT::OpAnd, undef_sig));
+		}
+
 		int import_cell_counter = 0;
 		for (auto &c : module->cells)
 			if (design->selected(module, c.second)) {
@@ -567,7 +632,6 @@ struct SatPass : public Pass {
 		log("    -set <signal> <value>\n");
 		log("        set the specified signal to the specified value.\n");
 		log("\n");
-	#if 0
 		log("    -set-def <signal>\n");
 		log("        add a constraint that all bits of the given signal must be defined\n");
 		log("\n");
@@ -577,7 +641,6 @@ struct SatPass : public Pass {
 		log("    -set-all-undef <signal>\n");
 		log("        add a constraint that all bits of the given signal are undefined\n");
 		log("\n");
-	#endif
 		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");
@@ -596,13 +659,11 @@ struct SatPass : public Pass {
 		log("        set or unset the specified signal to the specified value in the\n");
 		log("        given timestep. this has priority over a -set for the same signal.\n");
 		log("\n");
-	#if 0
 		log("    -set-def-at <N> <signal>\n");
 		log("    -set-any-undef-at <N> <signal>\n");
 		log("    -set-all-undef-at <N> <signal>\n");
 		log("        add undef contraints in the given timestep.\n");
 		log("\n");
-	#endif
 		log("    -set-init <signal> <value>\n");
 		log("        set the initial value for the register driving the signal to the value\n");
 		log("\n");
@@ -638,7 +699,7 @@ struct SatPass : public Pass {
 		std::vector<std::string> shows, sets_def, sets_any_undef, sets_all_undef;
 		int loopcount = 0, seq_len = 0, maxsteps = 0, timeout = 0;
 		bool verify = false, fail_on_timeout = false, enable_undef = false;
-		bool ignore_div_by_zero = false, set_init_undef = false, max_undef = true;
+		bool ignore_div_by_zero = false, set_init_undef = false, max_undef = false;
 
 		log_header("Executing SAT pass (solving SAT problems in the circuit).\n");