diff --git a/libs/ezsat/ezsat.cc b/libs/ezsat/ezsat.cc
index dccc00555..577625259 100644
--- a/libs/ezsat/ezsat.cc
+++ b/libs/ezsat/ezsat.cc
@@ -1131,10 +1131,15 @@ void ezSAT::printDIMACS(FILE *f, bool verbose) const
int maxClauseLen = 0;
for (auto &clause : cnfClauses)
maxClauseLen = std::max(int(clause.size()), maxClauseLen);
+ if (!verbose)
+ maxClauseLen = std::min(maxClauseLen, 3);
for (auto &clause : cnfClauses) {
for (auto idx : clause)
fprintf(f, " %*d", digits, idx);
- fprintf(f, " %*d\n", (digits + 1)*int(maxClauseLen - clause.size()) + digits, 0);
+ if (maxClauseLen >= int(clause.size()))
+ fprintf(f, " %*d\n", (digits + 1)*int(maxClauseLen - clause.size()) + digits, 0);
+ else
+ fprintf(f, " %*d\n", digits, 0);
}
}
diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc
index 2cd15d01c..d18a220d3 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<std::string, std::string> 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<int>(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);
}
@@ -878,6 +878,10 @@ struct SatPass : public Pass {
log(" -dump_vcd <vcd-file-name>\n");
log(" dump SAT model (counter example in proof) to VCD file\n");
log("\n");
+ log(" -dump_cnf <cnf-file-name>\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");
@@ -903,6 +907,9 @@ struct SatPass : public Pass {
log(" -maxsteps <N>\n");
log(" Set a maximum length for the induction.\n");
log("\n");
+ log(" -initsteps <N>\n");
+ log(" Set initial length for the induction.\n");
+ log("\n");
log(" -timeout <N>\n");
log(" Maximum number of seconds a single SAT instance may take.\n");
log("\n");
@@ -925,12 +932,12 @@ struct SatPass : public Pass {
std::map<int, std::vector<std::pair<std::string, std::string>>> sets_at;
std::map<int, std::vector<std::string>> unsets_at, sets_def_at, sets_any_undef_at, sets_all_undef_at;
std::vector<std::string> 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;
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");
@@ -970,6 +977,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;
@@ -1108,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);
@@ -1240,21 +1255,42 @@ 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
+ {
+ 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("Induction step failed. Incrementing induction length.\n");
- inductstep.ez.assume(property);
+ log("Dumping CNF to file `%s'.\n", cnf_file_name.c_str());
+ cnf_file_name.clear();
- inductstep.print_model();
+ 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());
+
+ 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("\nReached maximum number of time steps -> proof failed.\n");
@@ -1318,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;