summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorAndrew Zonenberg <azonenberg@drawersteak.com>2014-02-17 06:06:04 -0500
committerClifford Wolf <clifford@clifford.at>2014-02-17 13:52:36 +0100
commit4a948d780a6dd7de73b4dd05aecabe3a12863f3f (patch)
tree733f15dcd6bd03f33cb7e8b1e44b9d7288b217a4
parent0fbc1a59dd617aa3e9e9219180b8df0a37447300 (diff)
Added "-dump_fail_to_vcd" argument to SAT solver
-rw-r--r--passes/sat/sat.cc114
1 files changed, 114 insertions, 0 deletions
diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc
index c0827159..1cf4f084 100644
--- 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;
}