Added "sat -dump_json" (WaveJSON format)

diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc
index 1aae421f0bb04949765c6121cf85d5819e51b642..a7a510d7d63c09bcc6f20cbcc242a2ae077c70e0 100644 (file)
--- 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