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

added sat -falsify

This commit is contained in:
Clifford Wolf 2014-02-04 13:34:37 +01:00
parent d267bcde4e
commit 6891fd79a3
1 changed files with 28 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

32
passes/sat/sat.cc
View File

@ -779,6 +779,12 @@ struct SatPass : public Pass {
log(" -verify-no-timeout\n"); log(" -verify-no-timeout\n");
log(" Like -verify but do not return an error for timeouts.\n"); log(" Like -verify but do not return an error for timeouts.\n");
log("\n"); log("\n");
log(" -falsify\n");
log(" Return an error and stop the synthesis script if the proof succeeds.\n");
log("\n");
log(" -falsify-no-timeout\n");
log(" Like -falsify but do not return an error for timeouts.\n");
log("\n");
} }
virtual void execute(std::vector<std::string> args, RTLIL::Design *design) virtual void execute(std::vector<std::string> args, RTLIL::Design *design)
{ {
@ -790,7 +796,7 @@ struct SatPass : public Pass {
bool verify = false, fail_on_timeout = false, enable_undef = false, set_def_inputs = false; bool verify = false, fail_on_timeout = false, enable_undef = false, set_def_inputs = false;
bool ignore_div_by_zero = false, set_init_undef = false, max_undef = false; bool ignore_div_by_zero = false, set_init_undef = false, max_undef = false;
bool tempinduct = false, prove_asserts = false, show_inputs = false, show_outputs = false; bool tempinduct = false, prove_asserts = false, show_inputs = false, show_outputs = false;
bool ignore_unknown_cells = false; bool ignore_unknown_cells = false, falsify = false;
log_header("Executing SAT pass (solving SAT problems in the circuit).\n"); log_header("Executing SAT pass (solving SAT problems in the circuit).\n");
@ -809,6 +815,15 @@ struct SatPass : public Pass {
verify = true; verify = true;
continue; continue;
} }
if (args[argidx] == "-falsify") {
fail_on_timeout = true;
falsify = true;
continue;
}
if (args[argidx] == "-falsify-no-timeout") {
falsify = true;
continue;
}
if (args[argidx] == "-timeout" && argidx+1 < args.size()) { if (args[argidx] == "-timeout" && argidx+1 < args.size()) {
timeout = atoi(args[++argidx].c_str()); timeout = atoi(args[++argidx].c_str());
continue; continue;
@ -957,8 +972,8 @@ 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) if (!prove.size() && !prove_x.size() && !prove_asserts && (verify || falsify))
log_cmd_error("Got -verify but nothing to prove!\n"); 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");
@ -1094,7 +1109,12 @@ struct SatPass : public Pass {
log_error("Called with -verify and proof did fail!\n"); log_error("Called with -verify and proof did fail!\n");
} }
tip_success:; if (0)
tip_success:
if (falsify) {
log("\n");
log_error("Called with -falsify and proof did succeed!\n");
}
} }
else else
{ {
@ -1188,6 +1208,10 @@ struct SatPass : public Pass {
else { 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) {
log("\n");
log_error("Called with -falsify and proof did succeed!\n");
}
} }
} }