From 0851c2b6ea7044d9bce2014a2be2365a2bf7e1b0 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Mon, 17 Feb 2014 13:57:14 +0100 Subject: Renamed "sat -dump_fail_to_vcd" to "sat -dump_vcd" and some minor cleanups --- passes/sat/sat.cc | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) (limited to 'passes') 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 \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); -- cgit v1.2.3