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

Added sat -verify and -falsify support for non-prove cases

This commit is contained in:
Clifford Wolf 2014-02-06 00:59:41 +01:00
parent cd06055e77
commit e915043144
1 changed files with 26 additions and 14 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

28
passes/sat/sat.cc
View File

@ -972,15 +972,9 @@ struct SatPass : public Pass {
if (module == NULL) if (module == NULL)
log_cmd_error("Can't perform SAT on an empty selection!\n"); 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) if (!prove.size() && !prove_x.size() && !prove_asserts && tempinduct)
log_cmd_error("Got -tempinduct but nothing to prove!\n"); 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) { if (set_def_inputs) {
for (auto &it : module->wires) for (auto &it : module->wires)
if (it.second->port_input) if (it.second->port_input)
@ -1192,20 +1186,31 @@ struct SatPass : public Pass {
goto rerun_solver; goto rerun_solver;
} }
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) { if (verify) {
log("\n"); log("\n");
log_error("Called with -verify and proof did fail!\n"); log_error("Called with -verify and proof did fail!\n");
} }
} }
}
else else
{ {
if (sathelper.gotTimeout) if (sathelper.gotTimeout)
goto timeout; goto timeout;
if (rerun_counter) if (rerun_counter)
log("SAT solving finished - no more models found (after %d distinct solutions).\n", 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"); 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"); log("SAT proof finished - no model found: SUCCESS!\n");
print_qed(); print_qed();
if (falsify) { if (falsify) {
@ -1215,11 +1220,18 @@ struct SatPass : public Pass {
} }
} }
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) { if (verify && rerun_counter) {
log("\n"); log("\n");
log_error("Called with -verify and proof did fail!\n"); log_error("Called with -verify and proof did fail!\n");
} }
} }
}
if (0) { if (0) {
timeout: timeout: