mirror of https://github.com/YosysHQ/yosys.git
Merge branch 'master' of github.com:cliffordwolf/yosys
This commit is contained in:
Clifford Wolf
commit
23a3b488a0
|
|
@ -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);
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
|
||||
|
|
|
|||
Loading…
Reference in New Issue