Added sat -tempinduc and sat -prove-asserts

1 files changed, 41 insertions, 10 deletions

diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc
index fef99dfc..cf3cd59f 100644
--- a/passes/sat/sat.cc
+++ b/passes/sat/sat.cc
@@ -47,6 +47,7 @@ struct SatHelper
 	std::vector<std::pair<std::string, std::string>> sets, prove, prove_x, sets_init;
 	std::map<int, std::vector<std::pair<std::string, std::string>>> sets_at;
 	std::map<int, std::vector<std::string>> unsets_at;
+	bool prove_asserts;
 
 	// undef constraints
 	bool enable_undef, set_init_undef;
@@ -284,7 +285,7 @@ struct SatHelper
 
 	int setup_proof(int timestep = -1)
 	{
-		assert(prove.size() + prove_x.size() > 0);
+		assert(prove.size() || prove_x.size() || prove_asserts);
 
 		RTLIL::SigSpec big_lhs, big_rhs;
 		std::vector<int> prove_bits;
@@ -352,6 +353,9 @@ struct SatHelper
 				prove_bits.push_back(ez.OR(undef_lhs.at(i), ez.AND(ez.NOT(undef_rhs.at(i)), ez.NOT(ez.XOR(value_lhs.at(i), value_rhs.at(i))))));
 		}
 
+		if (prove_asserts)
+			prove_bits.push_back(satgen.importAsserts(timestep));
+
 		return ez.expression(ezSAT::OpAnd, prove_bits);
 	}
 
@@ -717,15 +721,21 @@ struct SatPass : public Pass {
 		log("The following additional options can be used to set up a proof. If also -seq\n");
 		log("is passed, a temporal induction proof is performed.\n");
 		log("\n");
+		log("    -tempinduct\n");
+		log("        Perform a temporal induction proof. In a temporalinduction proof it is\n");
+		log("        proven that the condition holds forever after the number of time steps\n");
+		log("        specified using -seq.\n");
+		log("\n");
 		log("    -prove <signal> <value>\n");
-		log("        Attempt to proof that <signal> is always <value>. In a temporal\n");
-		log("        induction proof it is proven that the condition holds forever after\n");
-		log("        the number of time steps passed using -seq.\n");
+		log("        Attempt to proof that <signal> is always <value>.\n");
 		log("\n");
 		log("    -prove-x <signal> <value>\n");
 		log("        Like -prove, but an undef (x) bit in the lhs matches any value on\n");
 		log("        the right hand side. Useful for equivialence checking.\n");
 		log("\n");
+		log("    -prove-asserts\n");
+		log("        Prove that all asserts in the design hold.\n");
+		log("\n");
 		log("    -maxsteps <N>\n");
 		log("        Set a maximum length for the induction.\n");
 		log("\n");
@@ -748,6 +758,7 @@ struct SatPass : public Pass {
 		int loopcount = 0, seq_len = 0, maxsteps = 0, timeout = 0;
 		bool verify = false, fail_on_timeout = false, enable_undef = false, set_def_inputs = false;
 		bool ignore_div_by_zero = false, set_init_undef = false, max_undef = false;
+		bool tempinduct = false, prove_asserts = false;
 
 		log_header("Executing SAT pass (solving SAT problems in the circuit).\n");
 
@@ -817,6 +828,10 @@ struct SatPass : public Pass {
 				enable_undef = true;
 				continue;
 			}
+			if (args[argidx] == "-tempinduct") {
+				tempinduct = true;
+				continue;
+			}
 			if (args[argidx] == "-prove" && argidx+2 < args.size()) {
 				std::string lhs = args[++argidx];
 				std::string rhs = args[++argidx];
@@ -830,6 +845,10 @@ struct SatPass : public Pass {
 				enable_undef = true;
 				continue;
 			}
+			if (args[argidx] == "-prove-asserts") {
+				prove_asserts = true;
+				continue;
+			}
 			if (args[argidx] == "-seq" && argidx+1 < args.size()) {
 				seq_len = atoi(args[++argidx].c_str());
 				continue;
@@ -894,16 +913,22 @@ struct SatPass : public Pass {
 		if (module == NULL) 
 			log_cmd_error("Can't perform SAT on an empty selection!\n");
 
-		if (prove.size() + prove_x.size() == 0 && verify)
+		if (!prove.size() && !prove_x.size() && !prove_asserts && verify)
 			log_cmd_error("Got -verify but nothing to prove!\n");
 
+		if (!prove.size() && !prove_x.size() && !prove_asserts && tempinduct)
+			log_cmd_error("Got -tempinduct but nothing to prove!\n");
+
+		if (seq_len == 0 && tempinduct)
+			log_cmd_error("Got -tempinduct but no -seq argument!\n");
+
 		if (set_def_inputs) {
 			for (auto &it : module->wires)
 				if (it.second->port_input)
 					sets_def.push_back(it.second->name);
 		}
 
-		if (prove.size() + prove_x.size() > 0 && seq_len > 0)
+		if (tempinduct)
 		{
 			if (loopcount > 0 || max_undef)
 				log_cmd_error("The options -max, -all, and -max_undef are not supported for temporal induction proofs!\n");
@@ -914,6 +939,7 @@ struct SatPass : public Pass {
 			basecase.sets = sets;
 			basecase.prove = prove;
 			basecase.prove_x = prove_x;
+			basecase.prove_asserts = prove_asserts;
 			basecase.sets_at = sets_at;
 			basecase.unsets_at = unsets_at;
 			basecase.shows = shows;
@@ -935,6 +961,7 @@ struct SatPass : public Pass {
 			inductstep.sets = sets;
 			inductstep.prove = prove;
 			inductstep.prove_x = prove_x;
+			inductstep.prove_asserts = prove_asserts;
 			inductstep.shows = shows;
 			inductstep.timeout = timeout;
 			inductstep.sets_def = sets_def;
@@ -1021,6 +1048,7 @@ struct SatPass : public Pass {
 			sathelper.sets = sets;
 			sathelper.prove = prove;
 			sathelper.prove_x = prove_x;
+			sathelper.prove_asserts = prove_asserts;
 			sathelper.sets_at = sets_at;
 			sathelper.unsets_at = unsets_at;
 			sathelper.shows = shows;
@@ -1037,11 +1065,14 @@ struct SatPass : public Pass {
 
 			if (seq_len == 0) {
 				sathelper.setup();
-				if (sathelper.prove.size() + sathelper.prove_x.size() > 0)
+				if (sathelper.prove.size() || sathelper.prove_x.size() || sathelper.prove_asserts)
 					sathelper.ez.assume(sathelper.ez.NOT(sathelper.setup_proof()));
 			} else {
-				for (int timestep = 1; timestep <= seq_len; timestep++)
+				for (int timestep = 1; timestep <= seq_len; timestep++) {
 					sathelper.setup(timestep);
+					if (sathelper.prove.size() || sathelper.prove_x.size() || sathelper.prove_asserts)
+						sathelper.ez.assume(sathelper.ez.NOT(sathelper.setup_proof(timestep)));
+				}
 				sathelper.setup_init();
 			}
 			sathelper.generate_model();
@@ -1064,7 +1095,7 @@ struct SatPass : public Pass {
 					sathelper.maximize_undefs();
 				}
 
-				if (prove.size() + prove_x.size() == 0) {
+				if (!prove.size() && !prove_x.size() && !prove_asserts) {
 					log("SAT solving finished - model found:\n");
 				} else {
 					log("SAT proof finished - model found: FAIL!\n");
@@ -1090,7 +1121,7 @@ struct SatPass : public Pass {
 					goto timeout;
 				if (rerun_counter)
 					log("SAT solving finished - no more models found (after %d distinct solutions).\n", rerun_counter);
-				else if (prove.size() + prove_x.size() == 0)
+				else if (!prove.size() && !prove_x.size() && !prove_asserts)
 					log("SAT solving finished - no model found.\n");
 				else {
 					log("SAT proof finished - no model found: SUCCESS!\n");