diff options
author | Clifford Wolf <clifford@clifford.at> | 2014-02-06 00:59:41 +0100 |
---|---|---|
committer | Clifford Wolf <clifford@clifford.at> | 2014-02-06 00:59:41 +0100 |
commit | e915043144d52e2ff97e2b4638ed1af84426e359 (patch) | |
tree | 511246408855fa1a93f2d3a65345ad998c2573bc /passes/sat | |
parent | cd06055e779d5909692da39bededc0141080c9d0 (diff) | |
download | yosys-e915043144d52e2ff97e2b4638ed1af84426e359.tar.gz yosys-e915043144d52e2ff97e2b4638ed1af84426e359.tar.bz2 yosys-e915043144d52e2ff97e2b4638ed1af84426e359.zip |
Added sat -verify and -falsify support for non-prove cases
Diffstat (limited to 'passes/sat')
-rw-r--r-- | passes/sat/sat.cc | 40 |
1 files changed, 26 insertions, 14 deletions
diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc index 062feeb97..f77897b06 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"); + } } } |