riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

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

This commit is contained in:
Clifford Wolf 2015-02-21 22:52:49 +01:00
parent b19c926af8
commit fae0e75ace
1 changed files with 64 additions and 21 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

85
passes/sat/sat.cc
View File

@ -993,6 +993,14 @@ struct SatPass : public Pass {
log(" -tempinduct-inductonly\n"); log(" -tempinduct-inductonly\n");
log(" Run only the induction half of temporal induction\n"); log(" Run only the induction half of temporal induction\n");
log("\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(" -prove <signal> <value>\n");
log(" Attempt to proof that <signal> is always <value>.\n"); log(" Attempt to proof that <signal> is always <value>.\n");
log("\n"); log("\n");
@ -1011,6 +1019,13 @@ struct SatPass : public Pass {
log("\n"); log("\n");
log(" -initsteps <N>\n"); log(" -initsteps <N>\n");
log(" Set initial length for the induction.\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("\n");
log(" -timeout <N>\n"); log(" -timeout <N>\n");
log(" Maximum number of seconds a single SAT instance may take.\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 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 ignore_unknown_cells = false, falsify = false, tempinduct_def = false, set_init_def = false;
bool tempinduct_baseonly = false, tempinduct_inductonly = 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; std::string vcd_file_name, json_file_name, cnf_file_name;
log_header("Executing SAT pass (solving SAT problems in the circuit).\n"); 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()); initsteps = atoi(args[++argidx].c_str());
continue; 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") { if (args[argidx] == "-ignore_div_by_zero") {
ignore_div_by_zero = true; ignore_div_by_zero = true;
continue; continue;
@ -1142,6 +1162,10 @@ struct SatPass : public Pass {
tempinduct_inductonly = true; tempinduct_inductonly = true;
continue; 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()) { if (args[argidx] == "-prove" && argidx+2 < args.size()) {
std::string lhs = args[++argidx]; std::string lhs = args[++argidx];
std::string rhs = args[++argidx]; std::string rhs = args[++argidx];
@ -1370,24 +1394,34 @@ struct SatPass : public Pass {
if (inductlen > 1) if (inductlen > 1)
basecase.force_unique_state(seq_len + 1, seq_len + inductlen); basecase.force_unique_state(seq_len + 1, seq_len + inductlen);
log("\n[base case] Solving problem with %d variables and %d clauses..\n", if (tempinduct_skip < inductlen)
basecase.ez->numCnfVariables(), basecase.ez->numCnfClauses()); {
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))) { if (basecase.solve(basecase.ez->NOT(property))) {
log("SAT temporal induction proof finished - model found for base case: FAIL!\n"); log("SAT temporal induction proof finished - model found for base case: FAIL!\n");
print_proof_failed(); print_proof_failed();
basecase.print_model(); basecase.print_model();
if(!vcd_file_name.empty()) if(!vcd_file_name.empty())
basecase.dump_model_to_vcd(vcd_file_name); basecase.dump_model_to_vcd(vcd_file_name);
if(!json_file_name.empty()) if(!json_file_name.empty())
basecase.dump_model_to_json(json_file_name); basecase.dump_model_to_json(json_file_name);
goto tip_failed; goto tip_failed;
}
if (basecase.gotTimeout)
goto timeout;
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());
} }
if (basecase.gotTimeout)
goto timeout;
log("Base case for induction length %d proven.\n", inductlen);
basecase.ez->assume(property); basecase.ez->assume(property);
} }
@ -1402,10 +1436,19 @@ struct SatPass : public Pass {
if (inductlen > 1) if (inductlen > 1)
inductstep.force_unique_state(1, 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", if (inductlen < tempinduct_skip)
inductstep.ez->numCnfVariables(), inductstep.ez->numCnfClauses()); 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); inductstep.ez->assume(property);
} }
else else
@ -1423,8 +1466,8 @@ struct SatPass : public Pass {
fclose(f); fclose(f);
} }
log("\n[induction step] Solving problem with %d variables and %d clauses..\n", log("\n[induction step %d] Solving problem with %d variables and %d clauses..\n",
inductstep.ez->numCnfVariables(), inductstep.ez->numCnfClauses()); inductlen, inductstep.ez->numCnfVariables(), inductstep.ez->numCnfClauses());
if (!inductstep.solve(inductstep.ez->NOT(property))) { if (!inductstep.solve(inductstep.ez->NOT(property))) {
if (inductstep.gotTimeout) if (inductstep.gotTimeout)