diff options
author | Clifford Wolf <clifford@clifford.at> | 2015-02-19 10:53:40 +0100 |
---|---|---|
committer | Clifford Wolf <clifford@clifford.at> | 2015-02-19 10:53:40 +0100 |
commit | 1ecee6c49cf18f4acec7ae942d36db7370c92071 (patch) | |
tree | e048ab6d8b9da29d7fd00172fd88f0d6e733039a /passes/sat | |
parent | 20eb5cad4b41cbf2278f3213fb8f24a944fb2f7d (diff) | |
download | yosys-1ecee6c49cf18f4acec7ae942d36db7370c92071.tar.gz yosys-1ecee6c49cf18f4acec7ae942d36db7370c92071.tar.bz2 yosys-1ecee6c49cf18f4acec7ae942d36db7370c92071.zip |
Added "sat -dump_json" (WaveJSON format)
Diffstat (limited to 'passes/sat')
-rw-r--r-- | passes/sat/sat.cc | 96 |
1 files changed, 92 insertions, 4 deletions
diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc index 1aae421f0..a7a510d7d 100644 --- a/passes/sat/sat.cc +++ b/passes/sat/sat.cc @@ -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 |