Added "-dump_fail_to_vcd" argument to SAT solver

diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc
index c082715909493be7c918b2d9367335cfdc916f72..1cf4f084186d29f3b770876bc8a784354f38bf7b 100644 (file)
--- a/passes/sat/sat.cc
+++ b/passes/sat/sat.cc
@@ -30,6 +30,8 @@
 #include <stdlib.h>
 #include <stdio.h>
 #include <algorithm>
+#include <errno.h>
+#include <string.h>
 
 namespace {
 
@@ -630,6 +632,109 @@ 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)
+                       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};
+               time(&timestamp);
+               now = localtime(&timestamp);
+               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");
+               fprintf(f, "$version\n");
+               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",
+                       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
+               std::map<std::string, std::string> vcdnames;
+               
+               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())
+                               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
+                       std::string legal_desc = info.description.c_str();
+                       for (auto &c : legal_desc) {
+                               if(c == '$')
+                                       c = '_';
+                               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
+                       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)
+               {
+                       RTLIL::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;
+                       }
+                       
+                       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)
+                               fprintf(f, "%c%s\n", bitvals[value.bits[0]], vcdnames[info.description].c_str());
+                       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]]);
+                               fprintf(f, " %s\n", vcdnames[info.description].c_str());
+                       }
+               }
+
+               if (last_timestep == -2)
+                       log("  no model variables selected for display.\n");
+               
+               fclose(f);
+       }
 
        void invalidate_model(bool max_undef)
        {
@@ -822,6 +927,8 @@ 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;
+               bool dump_fail_to_vcd = false;
+               std::string vcd_file_name = "";
 
                log_header("Executing SAT pass (solving SAT problems in the circuit).\n");
 
@@ -995,6 +1102,11 @@ struct SatPass : public Pass {
                                ignore_unknown_cells = true;
                                continue;
                        }
+                       if (args[argidx] == "-dump_fail_to_vcd" && argidx+1 < args.size()) {
+                               dump_fail_to_vcd = true;
+                               vcd_file_name = args[++argidx];
+                               continue;
+                       }
                        break;
                }
                extra_args(args, argidx, design);
@@ -1107,6 +1219,8 @@ struct SatPass : public Pass {
                                        log("SAT temporal induction proof finished - model found for base case: FAIL!\n");
                                        print_proof_failed();
                                        basecase.print_model();
+                                       if(dump_fail_to_vcd)
+                                               basecase.dump_model_to_vcd(vcd_file_name);
                                        goto tip_failed;
                                }