summaryrefslogtreecommitdiff
path: root/passes
diff options
context:
space:
mode:
authorClifford Wolf <clifford@clifford.at>2014-02-17 13:57:14 +0100
committerClifford Wolf <clifford@clifford.at>2014-02-17 13:59:39 +0100
commit0851c2b6ea7044d9bce2014a2be2365a2bf7e1b0 (patch)
tree446e79b49c26e2a4d5ffdb7b314f0ee2c1fdb497 /passes
parent4a948d780a6dd7de73b4dd05aecabe3a12863f3f (diff)
Renamed "sat -dump_fail_to_vcd" to "sat -dump_vcd" and some minor cleanups
Diffstat (limited to 'passes')
-rw-r--r--passes/sat/sat.cc14
1 files changed, 9 insertions, 5 deletions
diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc
index 1cf4f084..2cd15d01 100644
--- a/passes/sat/sat.cc
+++ b/passes/sat/sat.cc
@@ -875,6 +875,9 @@ struct SatPass : public Pass {
log(" -set-init-zero\n");
log(" set all initial states (not set using -set-init) to zero\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("is passed, a temporal induction proof is performed.\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 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 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");
@@ -1102,8 +1104,7 @@ struct SatPass : public Pass {
ignore_unknown_cells = true;
continue;
}
- if (args[argidx] == "-dump_fail_to_vcd" && argidx+1 < args.size()) {
- dump_fail_to_vcd = true;
+ if (args[argidx] == "-dump_vcd" && argidx+1 < args.size()) {
vcd_file_name = args[++argidx];
continue;
}
@@ -1219,7 +1220,7 @@ struct SatPass : public Pass {
log("SAT temporal induction proof finished - model found for base case: FAIL!\n");
print_proof_failed();
basecase.print_model();
- if(dump_fail_to_vcd)
+ if(!vcd_file_name.empty())
basecase.dump_model_to_vcd(vcd_file_name);
goto tip_failed;
}
@@ -1344,6 +1345,9 @@ struct SatPass : public Pass {
sathelper.print_model();
+ if(!vcd_file_name.empty())
+ sathelper.dump_model_to_vcd(vcd_file_name);
+
if (loopcount != 0) {
loopcount--, rerun_counter++;
sathelper.invalidate_model(max_undef);