From: Clifford Wolf <clifford@clifford.at>
Date: Tue, 18 Feb 2014 08:03:16 +0000 (+0100)
Subject: Added "sat -initsteps"
X-Git-Tag: yosys-0.3.0~134^2~3
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=13051e6acf6c1fd506a49d258c3d99c1334c78cc;p=yosys.git

Added "sat -initsteps"
---

diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc
index 2cd15d01c..2dc7a16ba 100644
--- a/passes/sat/sat.cc
+++ b/passes/sat/sat.cc
@@ -903,6 +903,9 @@ struct SatPass : public Pass {
 		log("    -maxsteps <N>\n");
 		log("        Set a maximum length for the induction.\n");
 		log("\n");
+		log("    -initsteps <N>\n");
+		log("        Set initial length for the induction.\n");
+		log("\n");
 		log("    -timeout <N>\n");
 		log("        Maximum number of seconds a single SAT instance may take.\n");
 		log("\n");
@@ -925,7 +928,7 @@ struct SatPass : public Pass {
 		std::map<int, std::vector<std::pair<std::string, std::string>>> sets_at;
 		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, timeout = 0;
+		int loopcount = 0, seq_len = 0, maxsteps = 0, initsteps = 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, set_init_zero = false, max_undef = false;
 		bool tempinduct = false, prove_asserts = false, show_inputs = false, show_outputs = false;
@@ -970,6 +973,10 @@ struct SatPass : public Pass {
 				maxsteps = atoi(args[++argidx].c_str());
 				continue;
 			}
+			if (args[argidx] == "-initsteps" && argidx+1 < args.size()) {
+				initsteps = atoi(args[++argidx].c_str());
+				continue;
+			}
 			if (args[argidx] == "-ignore_div_by_zero") {
 				ignore_div_by_zero = true;
 				continue;
@@ -1240,21 +1247,29 @@ struct SatPass : public Pass {
 				if (inductlen > 1)
 					inductstep.force_unique_state(1, inductlen + 1);
 
-				log("\n[induction step] Solving problem with %d variables and %d clauses..\n",
-						inductstep.ez.numCnfVariables(), inductstep.ez.numCnfClauses());
-
-				if (!inductstep.solve(inductstep.ez.NOT(property))) {
-					if (inductstep.gotTimeout)
-						goto timeout;
-					log("Induction step proven: SUCCESS!\n");
-					print_qed();
-					goto tip_success;
+				if (inductlen < initsteps)
+				{
+					log("\n[induction step] Skipping problem with %d variables and %d clauses (below initsteps).\n",
+							inductstep.ez.numCnfVariables(), inductstep.ez.numCnfClauses());
+					inductstep.ez.assume(property);
 				}
+				else
+				{
+					log("\n[induction step] Solving problem with %d variables and %d clauses..\n",
+							inductstep.ez.numCnfVariables(), inductstep.ez.numCnfClauses());
+
+					if (!inductstep.solve(inductstep.ez.NOT(property))) {
+						if (inductstep.gotTimeout)
+							goto timeout;
+						log("Induction step proven: SUCCESS!\n");
+						print_qed();
+						goto tip_success;
+					}
 
-				log("Induction step failed. Incrementing induction length.\n");
-				inductstep.ez.assume(property);
-
-				inductstep.print_model();
+					log("Induction step failed. Incrementing induction length.\n");
+					inductstep.ez.assume(property);
+					inductstep.print_model();
+				}
 			}
 
 			log("\nReached maximum number of time steps -> proof failed.\n");