diff options
author | Clifford Wolf <clifford@clifford.at> | 2015-02-21 22:52:49 +0100 |
---|---|---|
committer | Clifford Wolf <clifford@clifford.at> | 2015-02-21 22:52:49 +0100 |
commit | fae0e75ace66d77eaf434305bdb06ca29931ec7b (patch) | |
tree | ac0946e76d0f1b8e665f3874665c92a732c798c3 /passes/sat | |
parent | b19c926af8badd5d5ff84b4cd54e7f40de68c504 (diff) | |
download | yosys-fae0e75ace66d77eaf434305bdb06ca29931ec7b.tar.gz yosys-fae0e75ace66d77eaf434305bdb06ca29931ec7b.tar.bz2 yosys-fae0e75ace66d77eaf434305bdb06ca29931ec7b.zip |
Added "sat -stepsize" and "sat -tempinduct-step"
Diffstat (limited to 'passes/sat')
-rw-r--r-- | passes/sat/sat.cc | 85 |
1 files changed, 64 insertions, 21 deletions
diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc index 3d6aab467..b998359dd 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) |