Added "sat -stepsize" and "sat -tempinduct-step"

1 files changed, 64 insertions, 21 deletions

diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc
index 3d6aab46..b998359d 100644
--- a/passes/sat/sat.cc
+++ b/passes/sat/sat.cc
@@ -993,6 +993,14 @@ struct SatPass : public Pass {
 		log("    -tempinduct-inductonly\n");
 		log("        Run only the induction half of temporal induction\n");
 		log("\n");
+		log("    -tempinduct-skip <N>\n");
+		log("        Skip the first <N> steps of the induction proof.\n");
+		log("\n");
+		log("        note: this will assume that the base case holds for <N> steps.\n");
+		log("        this must be proven independently with \"-tempinduct-baseonly\n");
+		log("        -maxsteps <N>\". Use -initsteps if you just want to set a\n");
+		log("        minimal induction length.\n");
+		log("\n");
 		log("    -prove <signal> <value>\n");
 		log("        Attempt to proof that <signal> is always <value>.\n");
 		log("\n");
@@ -1011,6 +1019,13 @@ struct SatPass : public Pass {
 		log("\n");
 		log("    -initsteps <N>\n");
 		log("        Set initial length for the induction.\n");
+		log("        This will speed up the search of the right induction length\n");
+		log("        for deep induction proofs.\n");
+		log("\n");
+		log("    -stepsize <N>\n");
+		log("        Increase the size of the induction proof in steps of <N>.\n");
+		log("        This will speed up the search of the right induction length\n");
+		log("        for deep induction proofs.\n");
 		log("\n");
 		log("    -timeout <N>\n");
 		log("        Maximum number of seconds a single SAT instance may take.\n");
@@ -1040,6 +1055,7 @@ struct SatPass : public Pass {
 		bool tempinduct = false, prove_asserts = false, show_inputs = false, show_outputs = false;
 		bool ignore_unknown_cells = false, falsify = false, tempinduct_def = false, set_init_def = false;
 		bool tempinduct_baseonly = false, tempinduct_inductonly = false;
+		int tempinduct_skip = 0, stepsize = 1;
 		std::string vcd_file_name, json_file_name, cnf_file_name;
 
 		log_header("Executing SAT pass (solving SAT problems in the circuit).\n");
@@ -1084,6 +1100,10 @@ struct SatPass : public Pass {
 				initsteps = atoi(args[++argidx].c_str());
 				continue;
 			}
+			if (args[argidx] == "-stepsize" && argidx+1 < args.size()) {
+				stepsize = std::max(1, atoi(args[++argidx].c_str()));
+				continue;
+			}
 			if (args[argidx] == "-ignore_div_by_zero") {
 				ignore_div_by_zero = true;
 				continue;
@@ -1142,6 +1162,10 @@ struct SatPass : public Pass {
 				tempinduct_inductonly = true;
 				continue;
 			}
+			if (args[argidx] == "-tempinduct-skip" && argidx+1 < args.size()) {
+				tempinduct_skip = atoi(args[++argidx].c_str());
+				continue;
+			}
 			if (args[argidx] == "-prove" && argidx+2 < args.size()) {
 				std::string lhs = args[++argidx];
 				std::string rhs = args[++argidx];
@@ -1370,24 +1394,34 @@ struct SatPass : public Pass {
 					if (inductlen > 1)
 						basecase.force_unique_state(seq_len + 1, seq_len + inductlen);
 
-					log("\n[base case] Solving problem with %d variables and %d clauses..\n",
-							basecase.ez->numCnfVariables(), basecase.ez->numCnfClauses());
-
-					if (basecase.solve(basecase.ez->NOT(property))) {
-						log("SAT temporal induction proof finished - model found for base case: FAIL!\n");
-						print_proof_failed();
-						basecase.print_model();
-						if(!vcd_file_name.empty())
-							basecase.dump_model_to_vcd(vcd_file_name);
-						if(!json_file_name.empty())
-							basecase.dump_model_to_json(json_file_name);
-						goto tip_failed;
-					}
+					if (tempinduct_skip < inductlen)
+					{
+						log("\n[base case %d] Solving problem with %d variables and %d clauses..\n",
+								inductlen, basecase.ez->numCnfVariables(), basecase.ez->numCnfClauses());
+
+						if (basecase.solve(basecase.ez->NOT(property))) {
+							log("SAT temporal induction proof finished - model found for base case: FAIL!\n");
+							print_proof_failed();
+							basecase.print_model();
+							if(!vcd_file_name.empty())
+								basecase.dump_model_to_vcd(vcd_file_name);
+							if(!json_file_name.empty())
+								basecase.dump_model_to_json(json_file_name);
+							goto tip_failed;
+						}
 
-					if (basecase.gotTimeout)
-						goto timeout;
+						if (basecase.gotTimeout)
+							goto timeout;
 
-					log("Base case for induction length %d proven.\n", inductlen);
+						log("Base case for induction length %d proven.\n", inductlen);
+					}
+					else
+					{
+						log("\n[base case %d] Skipping prove for this step (-tempinduct-skip %d).",
+								inductlen, tempinduct_skip);
+						log("\n[base case %d] Problem size so far: %d variables and %d clauses.\n",
+								inductlen, basecase.ez->numCnfVariables(), basecase.ez->numCnfClauses());
+					}
 					basecase.ez->assume(property);
 				}
 
@@ -1402,10 +1436,19 @@ struct SatPass : public Pass {
 					if (inductlen > 1)
 						inductstep.force_unique_state(1, inductlen + 1);
 
-					if (inductlen < initsteps)
+					if (inductlen < tempinduct_skip || inductlen < initsteps || inductlen % stepsize != 0)
 					{
-						log("\n[induction step] Skipping problem with %d variables and %d clauses (below initsteps).\n",
-								inductstep.ez->numCnfVariables(), inductstep.ez->numCnfClauses());
+						if (inductlen < tempinduct_skip)
+							log("\n[induction step %d] Skipping prove for this step (-tempinduct-skip %d).",
+									inductlen, tempinduct_skip);
+						if (inductlen < initsteps)
+							log("\n[induction step %d] Skipping prove for this step (-initsteps %d).",
+									inductlen, tempinduct_skip);
+						if (inductlen % stepsize != 0)
+							log("\n[induction step %d] Skipping prove for this step (-stepsize %d).",
+									inductlen, stepsize);
+						log("\n[induction step %d] Problem size so far: %d variables and %d clauses.\n",
+								inductlen, inductstep.ez->numCnfVariables(), inductstep.ez->numCnfClauses());
 						inductstep.ez->assume(property);
 					}
 					else
@@ -1423,8 +1466,8 @@ struct SatPass : public Pass {
 							fclose(f);
 						}
 
-						log("\n[induction step] Solving problem with %d variables and %d clauses..\n",
-								inductstep.ez->numCnfVariables(), inductstep.ez->numCnfClauses());
+						log("\n[induction step %d] Solving problem with %d variables and %d clauses..\n",
+								inductlen, inductstep.ez->numCnfVariables(), inductstep.ez->numCnfClauses());
 
 						if (!inductstep.solve(inductstep.ez->NOT(property))) {
 							if (inductstep.gotTimeout)