mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-11-04 13:29:12 +00:00
Code Activity

Renamed "sat -dump_fail_to_vcd" to "sat -dump_vcd" and some minor cleanups

Browse source
This commit is contained in:
Clifford Wolf 2014-02-17 13:57:14 +01:00
parent 4a948d780a
commit 0851c2b6ea
1 changed files with 9 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

14
passes/sat/sat.cc
View file

@ -875,6 +875,9 @@ struct SatPass : public Pass {
log(" -set-init-zero\n"); log(" -set-init-zero\n");
log(" set all initial states (not set using -set-init) to zero\n"); log(" set all initial states (not set using -set-init) to zero\n");
log("\n"); log("\n");
log(" -dump_vcd <vcd-file-name>\n");
log(" dump SAT model (counter example in proof) to VCD file\n");
log("\n");
log("The following additional options can be used to set up a proof. If also -seq\n"); log("The following additional options can be used to set up a proof. If also -seq\n");
log("is passed, a temporal induction proof is performed.\n"); log("is passed, a temporal induction proof is performed.\n");
log("\n"); log("\n");
@ -927,8 +930,7 @@ struct SatPass : public Pass {
bool ignore_div_by_zero = false, set_init_undef = false, set_init_zero = false, max_undef = false; bool ignore_div_by_zero = false, set_init_undef = false, set_init_zero = 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, falsify = false, tempinduct_def = false, set_init_def = false; bool ignore_unknown_cells = false, falsify = false, tempinduct_def = false, set_init_def = false;
bool dump_fail_to_vcd = false; std::string vcd_file_name;
std::string vcd_file_name = "";
log_header("Executing SAT pass (solving SAT problems in the circuit).\n"); log_header("Executing SAT pass (solving SAT problems in the circuit).\n");
@ -1102,8 +1104,7 @@ struct SatPass : public Pass {
ignore_unknown_cells = true; ignore_unknown_cells = true;
continue; continue;
} }
if (args[argidx] == "-dump_fail_to_vcd" && argidx+1 < args.size()) { if (args[argidx] == "-dump_vcd" && argidx+1 < args.size()) {
dump_fail_to_vcd = true;
vcd_file_name = args[++argidx]; vcd_file_name = args[++argidx];
continue; continue;
} }
@ -1219,7 +1220,7 @@ struct SatPass : public Pass {
log("SAT temporal induction proof finished - model found for base case: FAIL!\n"); log("SAT temporal induction proof finished - model found for base case: FAIL!\n");
print_proof_failed(); print_proof_failed();
basecase.print_model(); basecase.print_model();
if(dump_fail_to_vcd) if(!vcd_file_name.empty())
basecase.dump_model_to_vcd(vcd_file_name); basecase.dump_model_to_vcd(vcd_file_name);
goto tip_failed; goto tip_failed;
} }
@ -1344,6 +1345,9 @@ struct SatPass : public Pass {
sathelper.print_model(); sathelper.print_model();
if(!vcd_file_name.empty())
sathelper.dump_model_to_vcd(vcd_file_name);
if (loopcount != 0) { if (loopcount != 0) {
loopcount--, rerun_counter++; loopcount--, rerun_counter++;
sathelper.invalidate_model(max_undef); sathelper.invalidate_model(max_undef);