summaryrefslogtreecommitdiff
path: root/passes/sat
diff options
context:
space:
mode:
authorClifford Wolf <clifford@clifford.at>2014-02-06 00:59:41 +0100
committerClifford Wolf <clifford@clifford.at>2014-02-06 00:59:41 +0100
commite915043144d52e2ff97e2b4638ed1af84426e359 (patch)
tree511246408855fa1a93f2d3a65345ad998c2573bc /passes/sat
parentcd06055e779d5909692da39bededc0141080c9d0 (diff)
Added sat -verify and -falsify support for non-prove cases
Diffstat (limited to 'passes/sat')
-rw-r--r--passes/sat/sat.cc40
1 files changed, 26 insertions, 14 deletions
diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc
index 062feeb9..f77897b0 100644
--- a/passes/sat/sat.cc
+++ b/passes/sat/sat.cc
@@ -972,15 +972,9 @@ struct SatPass : public Pass {
if (module == NULL)
log_cmd_error("Can't perform SAT on an empty selection!\n");
- if (!prove.size() && !prove_x.size() && !prove_asserts && (verify || falsify))
- log_cmd_error("Got -verify or -falsify but nothing to prove!\n");
-
if (!prove.size() && !prove_x.size() && !prove_asserts && tempinduct)
log_cmd_error("Got -tempinduct but nothing to prove!\n");
- if (seq_len == 0 && tempinduct)
- log_cmd_error("Got -tempinduct but no -seq argument!\n");
-
if (set_def_inputs) {
for (auto &it : module->wires)
if (it.second->port_input)
@@ -1192,9 +1186,16 @@ struct SatPass : public Pass {
goto rerun_solver;
}
- if (verify) {
- log("\n");
- log_error("Called with -verify and proof did fail!\n");
+ if (!prove.size() && !prove_x.size() && !prove_asserts) {
+ if (falsify) {
+ log("\n");
+ log_error("Called with -falsify and found a model!\n");
+ }
+ } else {
+ if (verify) {
+ log("\n");
+ log_error("Called with -verify and proof did fail!\n");
+ }
}
}
else
@@ -1203,9 +1204,13 @@ struct SatPass : public Pass {
goto timeout;
if (rerun_counter)
log("SAT solving finished - no more models found (after %d distinct solutions).\n", rerun_counter);
- else if (!prove.size() && !prove_x.size() && !prove_asserts)
+ else if (!prove.size() && !prove_x.size() && !prove_asserts) {
log("SAT solving finished - no model found.\n");
- else {
+ if (verify) {
+ log("\n");
+ log_error("Called with -verify and found no model!\n");
+ }
+ } else {
log("SAT proof finished - no model found: SUCCESS!\n");
print_qed();
if (falsify) {
@@ -1215,9 +1220,16 @@ struct SatPass : public Pass {
}
}
- if (verify && rerun_counter) {
- log("\n");
- log_error("Called with -verify and proof did fail!\n");
+ if (!prove.size() && !prove_x.size() && !prove_asserts) {
+ if (falsify && rerun_counter) {
+ log("\n");
+ log_error("Called with -falsify and found a model!\n");
+ }
+ } else {
+ if (verify && rerun_counter) {
+ log("\n");
+ log_error("Called with -verify and proof did fail!\n");
+ }
}
}