mirror of https://github.com/YosysHQ/yosys.git
Added "sat -dump_json" (WaveJSON format)
This commit is contained in:
Clifford Wolf
parent
20eb5cad4b
commit
1ecee6c49c
|
|
@ -671,7 +671,7 @@ struct SatHelper
|
|||
fprintf(f, " %s\n", stime);
|
||||
fprintf(f, "$end\n");
|
||||
fprintf(f, "$version\n");
|
||||
fprintf(f, " Generated by %s\n", yosys_version_str);
|
||||
fprintf(f, " Generated by %s\n", yosys_version_str);
|
||||
fprintf(f, "$end\n");
|
||||
fprintf(f, "$comment\n");
|
||||
fprintf(f, " Generated from SAT problem in module %s (declared at %s)\n",
|
||||
|
|
@ -750,6 +750,81 @@ struct SatHelper
|
|||
fclose(f);
|
||||
}
|
||||
|
||||
void dump_model_to_json(std::string json_file_name)
|
||||
{
|
||||
FILE *f = fopen(json_file_name.c_str(), "w");
|
||||
if (!f)
|
||||
log_cmd_error("Can't open output file `%s' for writing: %s\n", json_file_name.c_str(), strerror(errno));
|
||||
|
||||
log("Dumping SAT model to WaveJSON file '%s'.\n", json_file_name.c_str());
|
||||
|
||||
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, "// Generated by %s\n", yosys_version_str);
|
||||
|
||||
int mintime = 1, maxtime = 0, maxwidth = 0;;
|
||||
dict<string, pair<int, dict<int, Const>>> wavedata;
|
||||
|
||||
for (auto &info : modelInfo)
|
||||
{
|
||||
Const value;
|
||||
for (int i = 0; i < info.width; i++) {
|
||||
value.bits.push_back(modelValues.at(info.offset+i) ? RTLIL::State::S1 : RTLIL::State::S0);
|
||||
if (enable_undef && modelValues.at(modelExpressions.size()/2 + info.offset + i))
|
||||
value.bits.back() = RTLIL::State::Sx;
|
||||
}
|
||||
|
||||
wavedata[info.description].first = info.width;
|
||||
wavedata[info.description].second[info.timestep] = value;
|
||||
mintime = std::min(mintime, info.timestep);
|
||||
maxtime = std::max(maxtime, info.timestep);
|
||||
maxwidth = std::max(maxwidth, info.width);
|
||||
}
|
||||
|
||||
fprintf(f, "{ signal: [\n");
|
||||
for (auto &wd : wavedata) {
|
||||
vector<string> data;
|
||||
string name = wd.first.c_str();
|
||||
while (name.substr(0, 1) == "\\")
|
||||
name = name.substr(1);
|
||||
fprintf(f, " { name: '%s', wave: '", name.c_str());
|
||||
for (int i = mintime; i <= maxtime; i++) {
|
||||
if (wd.second.second.count(i)) {
|
||||
string this_data = wd.second.second[i].as_string();
|
||||
char ch = '=';
|
||||
if (wd.second.first == 1)
|
||||
ch = this_data[0];
|
||||
if (!data.empty() && data.back() == this_data) {
|
||||
fprintf(f, ".");
|
||||
} else {
|
||||
data.push_back(this_data);
|
||||
fprintf(f, "%c", ch);
|
||||
}
|
||||
} else {
|
||||
data.push_back("");
|
||||
fprintf(f, "4");
|
||||
}
|
||||
}
|
||||
if (wd.second.first != 1) {
|
||||
fprintf(f, "', data: [");
|
||||
for (int i = 0; i < GetSize(data); i++)
|
||||
fprintf(f, "%s'%s'", i ? ", " : "", data[i].c_str());
|
||||
fprintf(f, "] },\n");
|
||||
} else {
|
||||
fprintf(f, "' },\n");
|
||||
}
|
||||
}
|
||||
fprintf(f, " ],\n");
|
||||
fprintf(f, " config: {\n");
|
||||
fprintf(f, " hscale: %.2f,\n", maxwidth / 4.0);
|
||||
fprintf(f, " },\n");
|
||||
fprintf(f, "}\n");
|
||||
fclose(f);
|
||||
}
|
||||
|
||||
void invalidate_model(bool max_undef)
|
||||
{
|
||||
std::vector<int> clause;
|
||||
|
|
@ -890,6 +965,9 @@ 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_json <json-file-name>\n");
|
||||
log(" dump SAT model (counter example in proof) to a WaveJSON 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");
|
||||
|
|
@ -952,7 +1030,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, cnf_file_name;
|
||||
std::string vcd_file_name, json_file_name, cnf_file_name;
|
||||
|
||||
log_header("Executing SAT pass (solving SAT problems in the circuit).\n");
|
||||
|
||||
|
|
@ -1143,6 +1221,10 @@ struct SatPass : public Pass {
|
|||
vcd_file_name = args[++argidx];
|
||||
continue;
|
||||
}
|
||||
if (args[argidx] == "-dump_json" && argidx+1 < args.size()) {
|
||||
json_file_name = args[++argidx];
|
||||
continue;
|
||||
}
|
||||
if (args[argidx] == "-dump_cnf" && argidx+1 < args.size()) {
|
||||
cnf_file_name = args[++argidx];
|
||||
continue;
|
||||
|
|
@ -1159,7 +1241,7 @@ struct SatPass : public Pass {
|
|||
RTLIL::id2cstr(module->name), RTLIL::id2cstr(mod_it.first));
|
||||
module = mod_it.second;
|
||||
}
|
||||
if (module == NULL)
|
||||
if (module == NULL)
|
||||
log_cmd_error("Can't perform SAT on an empty selection!\n");
|
||||
|
||||
if (!prove.size() && !prove_x.size() && !prove_asserts && tempinduct)
|
||||
|
|
@ -1267,6 +1349,8 @@ struct SatPass : public Pass {
|
|||
basecase.print_model();
|
||||
if(!vcd_file_name.empty())
|
||||
basecase.dump_model_to_vcd(vcd_file_name);
|
||||
if(!json_file_name.empty())
|
||||
basecase.dump_model_to_json(json_file_name);
|
||||
goto tip_failed;
|
||||
}
|
||||
|
||||
|
|
@ -1326,6 +1410,8 @@ struct SatPass : public Pass {
|
|||
log("\nReached maximum number of time steps -> proof failed.\n");
|
||||
if(!vcd_file_name.empty())
|
||||
inductstep.dump_model_to_vcd(vcd_file_name);
|
||||
if(!json_file_name.empty())
|
||||
inductstep.dump_model_to_json(json_file_name);
|
||||
print_proof_failed();
|
||||
|
||||
tip_failed:
|
||||
|
|
@ -1424,6 +1510,8 @@ struct SatPass : public Pass {
|
|||
|
||||
if(!vcd_file_name.empty())
|
||||
sathelper.dump_model_to_vcd(vcd_file_name);
|
||||
if(!json_file_name.empty())
|
||||
sathelper.dump_model_to_json(json_file_name);
|
||||
|
||||
if (loopcount != 0) {
|
||||
loopcount--, rerun_counter++;
|
||||
|
|
@ -1487,5 +1575,5 @@ struct SatPass : public Pass {
|
|||
}
|
||||
}
|
||||
} SatPass;
|
||||
|
||||
|
||||
PRIVATE_NAMESPACE_END
|
||||
|
|
|
|||
Loading…
Reference in New Issue