From 13051e6acf6c1fd506a49d258c3d99c1334c78cc Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Tue, 18 Feb 2014 09:03:16 +0100 Subject: Added "sat -initsteps" --- passes/sat/sat.cc | 43 +++++++++++++++++++++++++++++-------------- 1 file changed, 29 insertions(+), 14 deletions(-) (limited to 'passes') diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc index 2cd15d01..2dc7a16b 100644 --- a/passes/sat/sat.cc +++ b/passes/sat/sat.cc @@ -903,6 +903,9 @@ struct SatPass : public Pass { log(" -maxsteps \n"); log(" Set a maximum length for the induction.\n"); log("\n"); + log(" -initsteps \n"); + log(" Set initial length for the induction.\n"); + log("\n"); log(" -timeout \n"); log(" Maximum number of seconds a single SAT instance may take.\n"); log("\n"); @@ -925,7 +928,7 @@ struct SatPass : public Pass { std::map>> sets_at; std::map> unsets_at, sets_def_at, sets_any_undef_at, sets_all_undef_at; std::vector shows, sets_def, sets_any_undef, sets_all_undef; - int loopcount = 0, seq_len = 0, maxsteps = 0, timeout = 0; + int loopcount = 0, seq_len = 0, maxsteps = 0, initsteps = 0, timeout = 0; bool verify = false, fail_on_timeout = false, enable_undef = false, set_def_inputs = 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; @@ -970,6 +973,10 @@ struct SatPass : public Pass { maxsteps = atoi(args[++argidx].c_str()); continue; } + if (args[argidx] == "-initsteps" && argidx+1 < args.size()) { + initsteps = atoi(args[++argidx].c_str()); + continue; + } if (args[argidx] == "-ignore_div_by_zero") { ignore_div_by_zero = true; continue; @@ -1240,21 +1247,29 @@ struct SatPass : public Pass { if (inductlen > 1) inductstep.force_unique_state(1, inductlen + 1); - log("\n[induction step] Solving problem with %d variables and %d clauses..\n", - inductstep.ez.numCnfVariables(), inductstep.ez.numCnfClauses()); - - if (!inductstep.solve(inductstep.ez.NOT(property))) { - if (inductstep.gotTimeout) - goto timeout; - log("Induction step proven: SUCCESS!\n"); - print_qed(); - goto tip_success; + if (inductlen < initsteps) + { + log("\n[induction step] Skipping problem with %d variables and %d clauses (below initsteps).\n", + inductstep.ez.numCnfVariables(), inductstep.ez.numCnfClauses()); + inductstep.ez.assume(property); } + else + { + log("\n[induction step] Solving problem with %d variables and %d clauses..\n", + inductstep.ez.numCnfVariables(), inductstep.ez.numCnfClauses()); + + if (!inductstep.solve(inductstep.ez.NOT(property))) { + if (inductstep.gotTimeout) + goto timeout; + log("Induction step proven: SUCCESS!\n"); + print_qed(); + goto tip_success; + } - log("Induction step failed. Incrementing induction length.\n"); - inductstep.ez.assume(property); - - inductstep.print_model(); + log("Induction step failed. Incrementing induction length.\n"); + inductstep.ez.assume(property); + inductstep.print_model(); + } } log("\nReached maximum number of time steps -> proof failed.\n"); -- cgit v1.2.3 From 32af10fa9b0fb8c86451a15f780288da13d4ab99 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Tue, 18 Feb 2014 09:28:05 +0100 Subject: Coding style corrections in SatHelper::dump_model_to_vcd() --- passes/sat/sat.cc | 62 +++++++++++++++++++++++++++---------------------------- 1 file changed, 31 insertions(+), 31 deletions(-) (limited to 'passes') diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc index 2dc7a16b..3b4a394e 100644 --- a/passes/sat/sat.cc +++ b/passes/sat/sat.cc @@ -632,27 +632,27 @@ struct SatHelper if (last_timestep == -2) log(" no model variables selected for display.\n"); } - + void dump_model_to_vcd(std::string vcd_file_name) { - FILE* f = fopen(vcd_file_name.c_str(), "w"); - if(!f) + FILE *f = fopen(vcd_file_name.c_str(), "w"); + if (!f) log_cmd_error("Can't open output file `%s' for writing: %s\n", vcd_file_name.c_str(), strerror(errno)); - + log("Dumping SAT model to VCD file %s\n", vcd_file_name.c_str()); - + time_t timestamp; struct tm* now; - char stime[128] = {0}; + char stime[128] = {}; time(×tamp); now = localtime(×tamp); strftime(stime, sizeof(stime), "%c", now); - + std::string module_fname = "unknown"; auto apos = module->attributes.find("\\src"); if(apos != module->attributes.end()) module_fname = module->attributes["\\src"].decode_string(); - + fprintf(f, "$date\n"); fprintf(f, " %s\n", stime); fprintf(f, "$end\n"); @@ -663,21 +663,22 @@ struct SatHelper fprintf(f, " Generated from SAT problem in module %s (declared at %s)\n", module->name.c_str(), module_fname.c_str()); fprintf(f, "$end\n"); - - //VCD has some limits on internal (non-display) identifier names, so make legal ones + + // VCD has some limits on internal (non-display) identifier names, so make legal ones std::map vcdnames; - - fprintf(f, "$timescale 1ns\n"); //arbitrary time scale since actual clock period is unknown/unimportant + + fprintf(f, "$timescale 1ns\n"); // arbitrary time scale since actual clock period is unknown/unimportant fprintf(f, "$scope module %s $end\n", module->name.c_str()); - for (auto &info : modelInfo) { - if(vcdnames.find(info.description) != vcdnames.end()) + for (auto &info : modelInfo) + { + if (vcdnames.find(info.description) != vcdnames.end()) continue; - + char namebuf[16]; snprintf(namebuf, sizeof(namebuf), "v%d", static_cast(vcdnames.size())); vcdnames[info.description] = namebuf; - - //Even display identifiers can't use some special characters + + // Even display identifiers can't use some special characters std::string legal_desc = info.description.c_str(); for (auto &c : legal_desc) { if(c == '$') @@ -685,21 +686,21 @@ struct SatHelper if(c == ':') c = '_'; } - + fprintf(f, "$var wire %d %s %s $end\n", info.width, namebuf, legal_desc.c_str()); - - //Need to look at first *two* cycles! - //We need to put a name on all variables but those without an initialization clause - //have no value at timestep 0 + + // Need to look at first *two* cycles! + // We need to put a name on all variables but those without an initialization clause + // have no value at timestep 0 if(info.timestep > 1) break; } fprintf(f, "$upscope $end\n"); fprintf(f, "$enddefinitions $end\n"); fprintf(f, "$dumpvars\n"); - + static const char bitvals[] = "01xzxx"; - + int last_timestep = -2; for (auto &info : modelInfo) { @@ -710,19 +711,18 @@ struct SatHelper if (enable_undef && modelValues.at(modelExpressions.size()/2 + info.offset + i)) value.bits.back() = RTLIL::State::Sx; } - - if (info.timestep != last_timestep) { + + if (info.timestep != last_timestep) { if(last_timestep == 0) fprintf(f, "$end\n"); else fprintf(f, "#%d\n", info.timestep); - last_timestep = info.timestep; } - - if(info.width == 1) + + if(info.width == 1) { fprintf(f, "%c%s\n", bitvals[value.bits[0]], vcdnames[info.description].c_str()); - else { + } else { fprintf(f, "b"); for(int k=info.width-1; k >= 0; k --) //need to flip bit ordering for VCD fprintf(f, "%c", bitvals[value.bits[k]]); @@ -732,7 +732,7 @@ struct SatHelper if (last_timestep == -2) log(" no model variables selected for display.\n"); - + fclose(f); } -- cgit v1.2.3 From a78bba1f5cf5b8c312c453e5c2c1a57b6946bebd Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Tue, 18 Feb 2014 09:29:08 +0100 Subject: Added "sat -dump_cnf" --- passes/sat/sat.cc | 39 ++++++++++++++++++++++++++++++++++----- 1 file changed, 34 insertions(+), 5 deletions(-) (limited to 'passes') diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc index 3b4a394e..d18a220d 100644 --- a/passes/sat/sat.cc +++ b/passes/sat/sat.cc @@ -878,6 +878,10 @@ struct SatPass : public Pass { log(" -dump_vcd \n"); log(" dump SAT model (counter example in proof) to VCD file\n"); log("\n"); + log(" -dump_cnf \n"); + log(" dump CNF of SAT problem (in DIMACS format). in temporal induction\n"); + log(" proofs this is the CNF of the first induction step.\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"); @@ -933,7 +937,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; - std::string vcd_file_name; + std::string vcd_file_name, cnf_file_name; log_header("Executing SAT pass (solving SAT problems in the circuit).\n"); @@ -1115,6 +1119,10 @@ struct SatPass : public Pass { vcd_file_name = args[++argidx]; continue; } + if (args[argidx] == "-dump_cnf" && argidx+1 < args.size()) { + cnf_file_name = args[++argidx]; + continue; + } break; } extra_args(args, argidx, design); @@ -1255,6 +1263,19 @@ struct SatPass : public Pass { } else { + if (!cnf_file_name.empty()) + { + FILE *f = fopen(cnf_file_name.c_str(), "w"); + if (!f) + log_cmd_error("Can't open output file `%s' for writing: %s\n", cnf_file_name.c_str(), strerror(errno)); + + log("Dumping CNF to file `%s'.\n", cnf_file_name.c_str()); + cnf_file_name.clear(); + + inductstep.ez.printDIMACS(f, false); + fclose(f); + } + log("\n[induction step] Solving problem with %d variables and %d clauses..\n", inductstep.ez.numCnfVariables(), inductstep.ez.numCnfClauses()); @@ -1333,10 +1354,18 @@ struct SatPass : public Pass { } sathelper.generate_model(); -#if 0 - // print CNF for debugging - sathelper.ez.printDIMACS(stdout, true); -#endif + if (!cnf_file_name.empty()) + { + FILE *f = fopen(cnf_file_name.c_str(), "w"); + if (!f) + log_cmd_error("Can't open output file `%s' for writing: %s\n", cnf_file_name.c_str(), strerror(errno)); + + log("Dumping CNF to file `%s'.\n", cnf_file_name.c_str()); + cnf_file_name.clear(); + + sathelper.ez.printDIMACS(f, false); + fclose(f); + } int rerun_counter = 0; -- cgit v1.2.3