diff options
| author | Clifford Wolf <clifford@clifford.at> | 2013-06-23 13:28:30 +0200 |
|---|---|---|
| committer | Clifford Wolf <clifford@clifford.at> | 2013-06-23 13:28:30 +0200 |
| commit | 101491132fbd617b0a0819045cc7b5d35395706d (patch) | |
| tree | 2373089242627eda25550aaf98cda08385bee5d9 | |
| parent | 46b177eb8a7a9e52eee4fd2e4a86c56f9a1fb44a (diff) | |
| download | yosys-101491132fbd617b0a0819045cc7b5d35395706d.tar.gz yosys-101491132fbd617b0a0819045cc7b5d35395706d.tar.bz2 yosys-101491132fbd617b0a0819045cc7b5d35395706d.zip | |
Added SAT support for -all/-max with -verify
| -rw-r--r-- | passes/sat/sat.cc | 17 |
1 files changed, 11 insertions, 6 deletions
diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc index 769d94a07..c75204230 100644 --- a/passes/sat/sat.cc +++ b/passes/sat/sat.cc @@ -659,7 +659,7 @@ struct SatPass : public Pass { } else { - if (loopcount > 0) + if (maxsteps > 0) log_cmd_error("The options -maxsteps is only supported for temporal induction proofs!\n"); SatHelper sathelper(design, module); @@ -702,16 +702,16 @@ struct SatPass : public Pass { sathelper.print_model(); - if (verify) { - log("\n"); - log_error("Called with -verify and proof did fail!\n"); - } - if (loopcount != 0) { loopcount--, did_rerun = true; sathelper.invalidate_model(); goto rerun_solver; } + + if (verify) { + log("\n"); + log_error("Called with -verify and proof did fail!\n"); + } } else { @@ -726,6 +726,11 @@ struct SatPass : public Pass { print_qed(); } } + + if (verify && did_rerun) { + log("\n"); + log_error("Called with -verify and proof did fail!\n"); + } } if (0) { |