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

Added SAT support for -all/-max with -verify

This commit is contained in:
Clifford Wolf 2013-06-23 13:28:30 +02:00
parent 46b177eb8a
commit 101491132f
1 changed files with 11 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

17
passes/sat/sat.cc
View File

@ -659,7 +659,7 @@ struct SatPass : public Pass {
} }
else else
{ {
if (loopcount > 0) if (maxsteps > 0)
log_cmd_error("The options -maxsteps is only supported for temporal induction proofs!\n"); log_cmd_error("The options -maxsteps is only supported for temporal induction proofs!\n");
SatHelper sathelper(design, module); SatHelper sathelper(design, module);
@ -702,16 +702,16 @@ struct SatPass : public Pass {
sathelper.print_model(); sathelper.print_model();
if (verify) {
log("\n");
log_error("Called with -verify and proof did fail!\n");
}
if (loopcount != 0) { if (loopcount != 0) {
loopcount--, did_rerun = true; loopcount--, did_rerun = true;
sathelper.invalidate_model(); sathelper.invalidate_model();
goto rerun_solver; goto rerun_solver;
} }
if (verify) {
log("\n");
log_error("Called with -verify and proof did fail!\n");
}
} }
else else
{ {
@ -726,6 +726,11 @@ struct SatPass : public Pass {
print_qed(); print_qed();
} }
} }
if (verify && did_rerun) {
log("\n");
log_error("Called with -verify and proof did fail!\n");
}
} }
if (0) { if (0) {