summaryrefslogtreecommitdiff
path: root/backends
diff options
context:
space:
mode:
Diffstat (limited to 'backends')
-rw-r--r--backends/blif/blif.cc105
-rw-r--r--backends/btor/btor.cc2
-rwxr-xr-xbackends/btor/verilog2btor.sh2
-rw-r--r--backends/edif/edif.cc55
-rw-r--r--backends/ilang/ilang_backend.cc2
-rw-r--r--backends/intersynth/intersynth.cc4
-rw-r--r--backends/json/json.cc16
-rw-r--r--backends/smt2/smt2.cc483
-rw-r--r--backends/smt2/smtbmc.py622
-rw-r--r--backends/smt2/smtio.py545
-rw-r--r--backends/smv/smv.cc2
-rw-r--r--backends/spice/spice.cc67
-rw-r--r--backends/verilog/verilog_backend.cc170
13 files changed, 1648 insertions, 427 deletions
diff --git a/backends/blif/blif.cc b/backends/blif/blif.cc
index f3b57765..6a379e67 100644
--- a/backends/blif/blif.cc
+++ b/backends/blif/blif.cc
@@ -41,13 +41,14 @@ struct BlifDumperConfig
bool param_mode;
bool attr_mode;
bool blackbox_mode;
+ bool noalias_mode;
std::string buf_type, buf_in, buf_out;
std::map<RTLIL::IdString, std::pair<RTLIL::IdString, RTLIL::IdString>> unbuf_types;
std::string true_type, true_out, false_type, false_out, undef_type, undef_out;
BlifDumperConfig() : icells_mode(false), conn_mode(false), impltf_mode(false), gates_mode(false),
- cname_mode(false), param_mode(false), attr_mode(false), blackbox_mode(false) { }
+ cname_mode(false), param_mode(false), attr_mode(false), blackbox_mode(false), noalias_mode(false) { }
};
struct BlifDumper
@@ -86,12 +87,13 @@ struct BlifDumper
}
vector<shared_str> cstr_buf;
+ pool<SigBit> cstr_bits_seen;
const char *cstr(RTLIL::IdString id)
{
std::string str = RTLIL::unescape_id(id);
for (size_t i = 0; i < str.size(); i++)
- if (str[i] == '#' || str[i] == '=')
+ if (str[i] == '#' || str[i] == '=' || str[i] == '<' || str[i] == '>')
str[i] = '?';
cstr_buf.push_back(str);
return cstr_buf.back().c_str();
@@ -99,15 +101,17 @@ struct BlifDumper
const char *cstr(RTLIL::SigBit sig)
{
+ cstr_bits_seen.insert(sig);
+
if (sig.wire == NULL) {
- if (sig == RTLIL::State::S0) return config->false_type == "-" ? config->false_out.c_str() : "$false";
- if (sig == RTLIL::State::S1) return config->true_type == "-" ? config->true_out.c_str() : "$true";
- return config->undef_type == "-" ? config->undef_out.c_str() : "$undef";
+ if (sig == RTLIL::State::S0) return config->false_type == "-" || config->false_type == "+" ? config->false_out.c_str() : "$false";
+ if (sig == RTLIL::State::S1) return config->true_type == "-" || config->true_type == "+" ? config->true_out.c_str() : "$true";
+ return config->undef_type == "-" || config->undef_type == "+" ? config->undef_out.c_str() : "$undef";
}
std::string str = RTLIL::unescape_id(sig.wire->name);
for (size_t i = 0; i < str.size(); i++)
- if (str[i] == '#' || str[i] == '=')
+ if (str[i] == '#' || str[i] == '=' || str[i] == '<' || str[i] == '>')
str[i] = '?';
if (sig.wire->width != 1)
@@ -200,19 +204,25 @@ struct BlifDumper
if (!config->impltf_mode) {
if (!config->false_type.empty()) {
- if (config->false_type != "-")
+ if (config->false_type == "+")
+ f << stringf(".names %s\n", config->false_out.c_str());
+ else if (config->false_type != "-")
f << stringf(".%s %s %s=$false\n", subckt_or_gate(config->false_type),
config->false_type.c_str(), config->false_out.c_str());
} else
f << stringf(".names $false\n");
if (!config->true_type.empty()) {
- if (config->true_type != "-")
+ if (config->true_type == "+")
+ f << stringf(".names %s\n1\n", config->true_out.c_str());
+ else if (config->true_type != "-")
f << stringf(".%s %s %s=$true\n", subckt_or_gate(config->true_type),
config->true_type.c_str(), config->true_out.c_str());
} else
f << stringf(".names $true\n1\n");
if (!config->undef_type.empty()) {
- if (config->undef_type != "-")
+ if (config->undef_type == "+")
+ f << stringf(".names %s\n", config->undef_out.c_str());
+ else if (config->undef_type != "-")
f << stringf(".%s %s %s=$undef\n", subckt_or_gate(config->undef_type),
config->undef_type.c_str(), config->undef_out.c_str());
} else
@@ -317,14 +327,25 @@ struct BlifDumper
continue;
}
+ if (!config->icells_mode && cell->type == "$_DLATCH_N_") {
+ f << stringf(".latch %s %s al %s%s\n", cstr(cell->getPort("\\D")), cstr(cell->getPort("\\Q")),
+ cstr(cell->getPort("\\E")), cstr_init(cell->getPort("\\Q")));
+ continue;
+ }
+
+ if (!config->icells_mode && cell->type == "$_DLATCH_P_") {
+ f << stringf(".latch %s %s ah %s%s\n", cstr(cell->getPort("\\D")), cstr(cell->getPort("\\Q")),
+ cstr(cell->getPort("\\E")), cstr_init(cell->getPort("\\Q")));
+ continue;
+ }
+
if (!config->icells_mode && cell->type == "$lut") {
f << stringf(".names");
auto &inputs = cell->getPort("\\A");
auto width = cell->parameters.at("\\WIDTH").as_int();
log_assert(inputs.size() == width);
- for (int i = width-1; i >= 0; i--) {
+ for (int i = width-1; i >= 0; i--)
f << stringf(" %s", cstr(inputs.extract(i, 1)));
- }
auto &output = cell->getPort("\\Y");
log_assert(output.size() == 1);
f << stringf(" %s", cstr(output));
@@ -340,6 +361,34 @@ struct BlifDumper
continue;
}
+ if (!config->icells_mode && cell->type == "$sop") {
+ f << stringf(".names");
+ auto &inputs = cell->getPort("\\A");
+ auto width = cell->parameters.at("\\WIDTH").as_int();
+ auto depth = cell->parameters.at("\\DEPTH").as_int();
+ vector<State> table = cell->parameters.at("\\TABLE").bits;
+ while (GetSize(table) < 2*width*depth)
+ table.push_back(State::S0);
+ log_assert(inputs.size() == width);
+ for (int i = 0; i < width; i++)
+ f << stringf(" %s", cstr(inputs.extract(i, 1)));
+ auto &output = cell->getPort("\\Y");
+ log_assert(output.size() == 1);
+ f << stringf(" %s", cstr(output));
+ f << stringf("\n");
+ for (int i = 0; i < depth; i++) {
+ for (int j = 0; j < width; j++) {
+ bool pat0 = table.at(2*width*i + 2*j + 0) == State::S1;
+ bool pat1 = table.at(2*width*i + 2*j + 1) == State::S1;
+ if (pat0 && !pat1) f << "0";
+ else if (!pat0 && pat1) f << "1";
+ else f << "-";
+ }
+ f << " 1\n";
+ }
+ continue;
+ }
+
f << stringf(".%s %s", subckt_or_gate(cell->type.str()), cstr(cell->type));
for (auto &conn : cell->connections())
for (int i = 0; i < conn.second.size(); i++) {
@@ -361,14 +410,21 @@ struct BlifDumper
for (auto &conn : module->connections())
for (int i = 0; i < conn.first.size(); i++)
+ {
+ SigBit lhs_bit = conn.first[i];
+ SigBit rhs_bit = conn.second[i];
+
+ if (config->noalias_mode && cstr_bits_seen.count(lhs_bit) == 0)
+ continue;
+
if (config->conn_mode)
- f << stringf(".conn %s %s\n", cstr(conn.second.extract(i, 1)), cstr(conn.first.extract(i, 1)));
+ f << stringf(".conn %s %s\n", cstr(rhs_bit), cstr(lhs_bit));
else if (!config->buf_type.empty())
- f << stringf(".%s %s %s=%s %s=%s\n", subckt_or_gate(config->buf_type), config->buf_type.c_str(), config->buf_in.c_str(), cstr(conn.second.extract(i, 1)),
- config->buf_out.c_str(), cstr(conn.first.extract(i, 1)));
+ f << stringf(".%s %s %s=%s %s=%s\n", subckt_or_gate(config->buf_type), config->buf_type.c_str(),
+ config->buf_in.c_str(), cstr(rhs_bit), config->buf_out.c_str(), cstr(lhs_bit));
else
- f << stringf(".names %s %s\n1 1\n", cstr(conn.second.extract(i, 1)), cstr(conn.first.extract(i, 1)));
-
+ f << stringf(".names %s %s\n1 1\n", cstr(rhs_bit), cstr(lhs_bit));
+ }
f << stringf(".end\n");
}
@@ -406,7 +462,14 @@ struct BlifBackend : public Backend {
log(" use the specified cell types to drive nets that are constant 1, 0, or\n");
log(" undefined. when '-' is used as <cell-type>, then <out-port> specifies\n");
log(" the wire name to be used for the constant signal and no cell driving\n");
- log(" that wire is generated.\n");
+ log(" that wire is generated. when '+' is used as <cell-type>, then <out-port>\n");
+ log(" specifies the wire name to be used for the constant signal and a .names\n");
+ log(" statement is generated to drive the wire.\n");
+ log("\n");
+ log(" -noalias\n");
+ log(" if a net name is aliasing another net name, then by default a net\n");
+ log(" without fanout is created that is driven by the other net. This option\n");
+ log(" suppresses the generation of this nets without fanout.\n");
log("\n");
log("The following options can be useful when the generated file is not going to be\n");
log("read by a BLIF parser but a custom tool. It is recommended to not name the output\n");
@@ -448,7 +511,7 @@ struct BlifBackend : public Backend {
std::string false_type, false_out;
BlifDumperConfig config;
- log_header("Executing BLIF backend.\n");
+ log_header(design, "Executing BLIF backend.\n");
size_t argidx;
for (argidx = 1; argidx < args.size(); argidx++)
@@ -517,6 +580,10 @@ struct BlifBackend : public Backend {
config.impltf_mode = true;
continue;
}
+ if (args[argidx] == "-noalias") {
+ config.noalias_mode = true;
+ continue;
+ }
break;
}
extra_args(f, filename, args, argidx);
@@ -540,7 +607,7 @@ struct BlifBackend : public Backend {
if (module->processes.size() != 0)
log_error("Found unmapped processes in module %s: unmapped processes are not supported in BLIF backend!\n", RTLIL::id2cstr(module->name));
if (module->memories.size() != 0)
- log_error("Found munmapped emories in module %s: unmapped memories are not supported in BLIF backend!\n", RTLIL::id2cstr(module->name));
+ log_error("Found unmapped memories in module %s: unmapped memories are not supported in BLIF backend!\n", RTLIL::id2cstr(module->name));
if (module->name == RTLIL::escape_id(top_module_name)) {
BlifDumper::dump(*f, module, design, config);
diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc
index 465723f1..bbe90e85 100644
--- a/backends/btor/btor.cc
+++ b/backends/btor/btor.cc
@@ -1065,7 +1065,7 @@ struct BtorBackend : public Backend {
std::string false_type, false_out;
BtorDumperConfig config;
- log_header("Executing BTOR backend.\n");
+ log_header(design, "Executing BTOR backend.\n");
size_t argidx=1;
extra_args(f, filename, args, argidx);
diff --git a/backends/btor/verilog2btor.sh b/backends/btor/verilog2btor.sh
index 1c537d5b..dfd7f1a8 100755
--- a/backends/btor/verilog2btor.sh
+++ b/backends/btor/verilog2btor.sh
@@ -22,7 +22,7 @@ hierarchy -top $3;
hierarchy -libdir $DIR;
hierarchy -check;
proc;
-opt; opt_const -mux_undef; opt;
+opt; opt_expr -mux_undef; opt;
rename -hide;;;
#techmap -map +/pmux2mux.v;;
splice; opt;
diff --git a/backends/edif/edif.cc b/backends/edif/edif.cc
index 475e43da..d16f1831 100644
--- a/backends/edif/edif.cc
+++ b/backends/edif/edif.cc
@@ -100,6 +100,11 @@ struct EdifBackend : public Backend {
log(" -top top_module\n");
log(" set the specified module as design top module\n");
log("\n");
+ log(" -nogndvcc\n");
+ log(" do not create \"GND\" and \"VCC\" cells. (this will produce an error\n");
+ log(" if the design contains constant nets. use \"hilomap\" to map to custom\n");
+ log(" constant drivers first)\n");
+ log("\n");
log("Unfortunately there are different \"flavors\" of the EDIF file format. This\n");
log("command generates EDIF files for the Xilinx place&route tools. It might be\n");
log("necessary to make small modifications to this command when a different tool\n");
@@ -108,10 +113,11 @@ struct EdifBackend : public Backend {
}
virtual void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design)
{
- log_header("Executing EDIF backend.\n");
+ log_header(design, "Executing EDIF backend.\n");
std::string top_module_name;
std::map<RTLIL::IdString, std::map<RTLIL::IdString, int>> lib_cell_ports;
+ bool nogndvcc = false;
CellTypes ct(design);
EdifNames edif_names;
@@ -122,6 +128,10 @@ struct EdifBackend : public Backend {
top_module_name = args[++argidx];
continue;
}
+ if (args[argidx] == "-nogndvcc") {
+ nogndvcc = true;
+ continue;
+ }
break;
}
extra_args(f, filename, args, argidx);
@@ -143,7 +153,7 @@ struct EdifBackend : public Backend {
if (module->processes.size() != 0)
log_error("Found unmapped processes in module %s: unmapped processes are not supported in EDIF backend!\n", RTLIL::id2cstr(module->name));
if (module->memories.size() != 0)
- log_error("Found munmapped emories in module %s: unmapped memories are not supported in EDIF backend!\n", RTLIL::id2cstr(module->name));
+ log_error("Found unmapped memories in module %s: unmapped memories are not supported in EDIF backend!\n", RTLIL::id2cstr(module->name));
for (auto cell_it : module->cells_)
{
@@ -169,21 +179,24 @@ struct EdifBackend : public Backend {
*f << stringf(" (edifLevel 0)\n");
*f << stringf(" (technology (numberDefinition))\n");
- *f << stringf(" (cell GND\n");
- *f << stringf(" (cellType GENERIC)\n");
- *f << stringf(" (view VIEW_NETLIST\n");
- *f << stringf(" (viewType NETLIST)\n");
- *f << stringf(" (interface (port G (direction OUTPUT)))\n");
- *f << stringf(" )\n");
- *f << stringf(" )\n");
-
- *f << stringf(" (cell VCC\n");
- *f << stringf(" (cellType GENERIC)\n");
- *f << stringf(" (view VIEW_NETLIST\n");
- *f << stringf(" (viewType NETLIST)\n");
- *f << stringf(" (interface (port P (direction OUTPUT)))\n");
- *f << stringf(" )\n");
- *f << stringf(" )\n");
+ if (!nogndvcc)
+ {
+ *f << stringf(" (cell GND\n");
+ *f << stringf(" (cellType GENERIC)\n");
+ *f << stringf(" (view VIEW_NETLIST\n");
+ *f << stringf(" (viewType NETLIST)\n");
+ *f << stringf(" (interface (port G (direction OUTPUT)))\n");
+ *f << stringf(" )\n");
+ *f << stringf(" )\n");
+
+ *f << stringf(" (cell VCC\n");
+ *f << stringf(" (cellType GENERIC)\n");
+ *f << stringf(" (view VIEW_NETLIST\n");
+ *f << stringf(" (viewType NETLIST)\n");
+ *f << stringf(" (interface (port P (direction OUTPUT)))\n");
+ *f << stringf(" )\n");
+ *f << stringf(" )\n");
+ }
for (auto &cell_it : lib_cell_ports) {
*f << stringf(" (cell %s\n", EDIF_DEF(cell_it.first));
@@ -279,8 +292,10 @@ struct EdifBackend : public Backend {
}
*f << stringf(" )\n");
*f << stringf(" (contents\n");
- *f << stringf(" (instance GND (viewRef VIEW_NETLIST (cellRef GND (libraryRef LIB))))\n");
- *f << stringf(" (instance VCC (viewRef VIEW_NETLIST (cellRef VCC (libraryRef LIB))))\n");
+ if (!nogndvcc) {
+ *f << stringf(" (instance GND (viewRef VIEW_NETLIST (cellRef GND (libraryRef LIB))))\n");
+ *f << stringf(" (instance VCC (viewRef VIEW_NETLIST (cellRef VCC (libraryRef LIB))))\n");
+ }
for (auto &cell_it : module->cells_) {
RTLIL::Cell *cell = cell_it.second;
*f << stringf(" (instance %s\n", EDIF_DEF(cell->name));
@@ -326,6 +341,8 @@ struct EdifBackend : public Backend {
for (auto &ref : it.second)
*f << stringf(" %s\n", ref.c_str());
if (sig.wire == NULL) {
+ if (nogndvcc)
+ log_error("Design contains constant nodes (map with \"hilomap\" first).\n");
if (sig == RTLIL::State::S0)
*f << stringf(" (portRef G (instanceRef GND))\n");
if (sig == RTLIL::State::S1)
diff --git a/backends/ilang/ilang_backend.cc b/backends/ilang/ilang_backend.cc
index adabf05e..03e29c52 100644
--- a/backends/ilang/ilang_backend.cc
+++ b/backends/ilang/ilang_backend.cc
@@ -391,7 +391,7 @@ struct IlangBackend : public Backend {
{
bool selected = false;
- log_header("Executing ILANG backend.\n");
+ log_header(design, "Executing ILANG backend.\n");
size_t argidx;
for (argidx = 1; argidx < args.size(); argidx++) {
diff --git a/backends/intersynth/intersynth.cc b/backends/intersynth/intersynth.cc
index 72a70e38..34cb52fb 100644
--- a/backends/intersynth/intersynth.cc
+++ b/backends/intersynth/intersynth.cc
@@ -73,7 +73,7 @@ struct IntersynthBackend : public Backend {
}
virtual void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design)
{
- log_header("Executing INTERSYNTH backend.\n");
+ log_header(design, "Executing INTERSYNTH backend.\n");
log_push();
std::vector<std::string> libfiles;
@@ -113,7 +113,7 @@ struct IntersynthBackend : public Backend {
}
if (libs.size() > 0)
- log_header("Continuing INTERSYNTH backend.\n");
+ log_header(design, "Continuing INTERSYNTH backend.\n");
std::set<std::string> conntypes_code, celltypes_code;
std::string netlists_code;
diff --git a/backends/json/json.cc b/backends/json/json.cc
index 9bc936a6..4baffa33 100644
--- a/backends/json/json.cc
+++ b/backends/json/json.cc
@@ -83,12 +83,12 @@ struct JsonWriter
return str + " ]";
}
- void write_parameters(const dict<IdString, Const> &parameters)
+ void write_parameters(const dict<IdString, Const> &parameters, bool for_module=false)
{
bool first = true;
for (auto &param : parameters) {
f << stringf("%s\n", first ? "" : ",");
- f << stringf(" %s: ", get_name(param.first).c_str());
+ f << stringf(" %s%s: ", for_module ? "" : " ", get_name(param.first).c_str());
if ((param.second.flags & RTLIL::ConstFlags::CONST_FLAG_STRING) != 0)
f << get_string(param.second.decode_string());
else if (GetSize(param.second.bits) > 32)
@@ -111,6 +111,10 @@ struct JsonWriter
f << stringf(" %s: {\n", get_name(module->name).c_str());
+ f << stringf(" \"attributes\": {");
+ write_parameters(module->attributes, /*for_module=*/true);
+ f << stringf("\n },\n");
+
f << stringf(" \"ports\": {");
bool first = true;
for (auto n : module->ports) {
@@ -411,10 +415,10 @@ struct JsonBackend : public Backend {
log(" - the inverted value of the specified input port bit\n");
log("\n");
log(" [ \"and\", <node-index>, <node-index>, <out-list> ]\n");
- log(" - the ANDed value of the speciefied nodes\n");
+ log(" - the ANDed value of the specified nodes\n");
log("\n");
log(" [ \"nand\", <node-index>, <node-index>, <out-list> ]\n");
- log(" - the inverted ANDed value of the speciefied nodes\n");
+ log(" - the inverted ANDed value of the specified nodes\n");
log("\n");
log(" [ \"true\", <out-list> ]\n");
log(" - the constant value 1\n");
@@ -445,7 +449,7 @@ struct JsonBackend : public Backend {
log(" ]\n");
log("\n");
log("Future version of Yosys might add support for additional fields in the JSON\n");
- log("format. A program processing this format must ignore all unkown fields.\n");
+ log("format. A program processing this format must ignore all unknown fields.\n");
log("\n");
}
virtual void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design)
@@ -463,7 +467,7 @@ struct JsonBackend : public Backend {
}
extra_args(f, filename, args, argidx);
- log_header("Executing JSON backend.\n");
+ log_header(design, "Executing JSON backend.\n");
JsonWriter json_writer(*f, false, aig_mode);
json_writer.write_design(design);
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index c852921e..9a25f3a2 100644
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -32,23 +32,43 @@ struct Smt2Worker
CellTypes ct;
SigMap sigmap;
RTLIL::Module *module;
- bool bvmode, memmode, regsmode, wiresmode, verbose;
+ bool bvmode, memmode, wiresmode, verbose;
int idcounter;
- std::vector<std::string> decls, trans;
+ std::vector<std::string> decls, trans, hier;
std::map<RTLIL::SigBit, RTLIL::Cell*> bit_driver;
- std::set<RTLIL::Cell*> exported_cells;
+ std::set<RTLIL::Cell*> exported_cells, hiercells, hiercells_queue;
pool<Cell*> recursive_cells, registers;
std::map<RTLIL::SigBit, std::pair<int, int>> fcache;
std::map<Cell*, int> memarrays;
std::map<int, int> bvsizes;
+ dict<IdString, char*> ids;
- Smt2Worker(RTLIL::Module *module, bool bvmode, bool memmode, bool regsmode, bool wiresmode, bool verbose) :
+ const char *get_id(IdString n)
+ {
+ if (ids.count(n) == 0) {
+ std::string str = log_id(n);
+ for (int i = 0; i < GetSize(str); i++) {
+ if (str[i] == '\\')
+ str[i] = '/';
+ }
+ ids[n] = strdup(str.c_str());
+ }
+ return ids[n];
+ }
+
+ template<typename T>
+ const char *get_id(T *obj) {
+ return get_id(obj->name);
+ }
+
+ Smt2Worker(RTLIL::Module *module, bool bvmode, bool memmode, bool wiresmode, bool verbose) :
ct(module->design), sigmap(module), module(module), bvmode(bvmode), memmode(memmode),
- regsmode(regsmode), wiresmode(wiresmode), verbose(verbose), idcounter(0)
+ wiresmode(wiresmode), verbose(verbose), idcounter(0)
{
- decls.push_back(stringf("(declare-sort |%s_s| 0)\n", log_id(module)));
+ decls.push_back(stringf("(declare-sort |%s_s| 0)\n", get_id(module)));
+ decls.push_back(stringf("(declare-fun |%s_is| (|%s_s|) Bool)\n", get_id(module), get_id(module)));
for (auto cell : module->cells())
for (auto &conn : cell->connections()) {
@@ -66,6 +86,28 @@ struct Smt2Worker
}
}
+ ~Smt2Worker()
+ {
+ for (auto &it : ids)
+ free(it.second);
+ ids.clear();
+ }
+
+ const char *get_id(Module *m)
+ {
+ return get_id(m->name);
+ }
+
+ const char *get_id(Cell *c)
+ {
+ return get_id(c->name);
+ }
+
+ const char *get_id(Wire *w)
+ {
+ return get_id(w->name);
+ }
+
void register_bool(RTLIL::SigBit bit, int id)
{
if (verbose) log("%*s-> register_bool: %s %d\n", 2+2*GetSize(recursive_cells), "",
@@ -121,14 +163,14 @@ struct Smt2Worker
if (verbose) log("%*s-> external bool: %s\n", 2+2*GetSize(recursive_cells), "",
log_signal(bit));
decls.push_back(stringf("(declare-fun |%s#%d| (|%s_s|) Bool) ; %s\n",
- log_id(module), idcounter, log_id(module), log_signal(bit)));
+ get_id(module), idcounter, get_id(module), log_signal(bit)));
register_bool(bit, idcounter++);
}
auto f = fcache.at(bit);
if (f.second >= 0)
- return stringf("(= ((_ extract %d %d) (|%s#%d| %s)) #b1)", f.second, f.second, log_id(module), f.first, state_name);
- return stringf("(|%s#%d| %s)", log_id(module), f.first, state_name);
+ return stringf("(= ((_ extract %d %d) (|%s#%d| %s)) #b1)", f.second, f.second, get_id(module), f.first, state_name);
+ return stringf("(|%s#%d| %s)", get_id(module), f.first, state_name);
}
std::string get_bool(RTLIL::SigSpec sig, const char *state_name = "state")
@@ -180,10 +222,10 @@ struct Smt2Worker
j++;
}
if (t1.second == 0 && j == bvsizes.at(t1.first))
- subexpr.push_back(stringf("(|%s#%d| %s)", log_id(module), t1.first, state_name));
+ subexpr.push_back(stringf("(|%s#%d| %s)", get_id(module), t1.first, state_name));
else
subexpr.push_back(stringf("((_ extract %d %d) (|%s#%d| %s))",
- t1.second + j - 1, t1.second, log_id(module), t1.first, state_name));
+ t1.second + j - 1, t1.second, get_id(module), t1.first, state_name));
continue;
}
@@ -196,8 +238,8 @@ struct Smt2Worker
for (auto bit : sig.extract(i, j))
log_assert(bit_driver.count(bit) == 0);
decls.push_back(stringf("(declare-fun |%s#%d| (|%s_s|) (_ BitVec %d)) ; %s\n",
- log_id(module), idcounter, log_id(module), j, log_signal(sig.extract(i, j))));
- subexpr.push_back(stringf("(|%s#%d| %s)", log_id(module), idcounter, state_name));
+ get_id(module), idcounter, get_id(module), j, log_signal(sig.extract(i, j))));
+ subexpr.push_back(stringf("(|%s#%d| %s)", get_id(module), idcounter, state_name));
register_bv(sig.extract(i, j), idcounter++);
}
@@ -228,10 +270,11 @@ struct Smt2Worker
else processed_expr += ch;
}
- if (verbose) log("%*s-> import cell: %s\n", 2+2*GetSize(recursive_cells), "",
- log_id(cell));
+ if (verbose)
+ log("%*s-> import cell: %s\n", 2+2*GetSize(recursive_cells), "", log_id(cell));
+
decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) Bool %s) ; %s\n",
- log_id(module), idcounter, log_id(module), processed_expr.c_str(), log_signal(bit)));
+ get_id(module), idcounter, get_id(module), processed_expr.c_str(), log_signal(bit)));
register_bool(bit, idcounter++);
recursive_cells.erase(cell);
}
@@ -271,16 +314,16 @@ struct Smt2Worker
if (width != GetSize(sig_y) && type != 'b')
processed_expr = stringf("((_ extract %d 0) %s)", GetSize(sig_y)-1, processed_expr.c_str());
- if (verbose) log("%*s-> import cell: %s\n", 2+2*GetSize(recursive_cells), "",
- log_id(cell));
+ if (verbose)
+ log("%*s-> import cell: %s\n", 2+2*GetSize(recursive_cells), "", log_id(cell));
if (type == 'b') {
decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) Bool %s) ; %s\n",
- log_id(module), idcounter, log_id(module), processed_expr.c_str(), log_signal(sig_y)));
+ get_id(module), idcounter, get_id(module), processed_expr.c_str(), log_signal(sig_y)));
register_boolvec(sig_y, idcounter++);
} else {
decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
- log_id(module), idcounter, log_id(module), GetSize(sig_y), processed_expr.c_str(), log_signal(sig_y)));
+ get_id(module), idcounter, get_id(module), GetSize(sig_y), processed_expr.c_str(), log_signal(sig_y)));
register_bv(sig_y, idcounter++);
}
@@ -302,21 +345,23 @@ struct Smt2Worker
} else
processed_expr += ch;
- if (verbose) log("%*s-> import cell: %s\n", 2+2*GetSize(recursive_cells), "",
- log_id(cell));
+ if (verbose)
+ log("%*s-> import cell: %s\n", 2+2*GetSize(recursive_cells), "", log_id(cell));
+
decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) Bool %s) ; %s\n",
- log_id(module), idcounter, log_id(module), processed_expr.c_str(), log_signal(sig_y)));
+ get_id(module), idcounter, get_id(module), processed_expr.c_str(), log_signal(sig_y)));
register_boolvec(sig_y, idcounter++);
recursive_cells.erase(cell);
}
void export_cell(RTLIL::Cell *cell)
{
- if (verbose) log("%*s=> export_cell %s (%s) [%s]\n", 2+2*GetSize(recursive_cells), "",
- log_id(cell), log_id(cell->type), exported_cells.count(cell) ? "old" : "new");
+ if (verbose)
+ log("%*s=> export_cell %s (%s) [%s]\n", 2+2*GetSize(recursive_cells), "",
+ log_id(cell), log_id(cell->type), exported_cells.count(cell) ? "old" : "new");
if (recursive_cells.count(cell))
- log_error("Found logic loop in module %s! See cell %s.\n", log_id(module), log_id(cell));
+ log_error("Found logic loop in module %s! See cell %s.\n", get_id(module), get_id(cell));
if (exported_cells.count(cell))
return;
@@ -324,11 +369,21 @@ struct Smt2Worker
exported_cells.insert(cell);
recursive_cells.insert(cell);
+ if (cell->type == "$initstate")
+ {
+ SigBit bit = sigmap(cell->getPort("\\Y").as_bit());
+ decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) Bool (|%s_is| state)) ; %s\n",
+ get_id(module), idcounter, get_id(module), get_id(module), log_signal(bit)));
+ register_bool(bit, idcounter++);
+ recursive_cells.erase(cell);
+ return;
+ }
+
if (cell->type == "$_DFF_P_" || cell->type == "$_DFF_N_")
{
registers.insert(cell);
decls.push_back(stringf("(declare-fun |%s#%d| (|%s_s|) Bool) ; %s\n",
- log_id(module), idcounter, log_id(module), log_signal(cell->getPort("\\Q"))));
+ get_id(module), idcounter, get_id(module), log_signal(cell->getPort("\\Q"))));
register_bool(cell->getPort("\\Q"), idcounter++);
recursive_cells.erase(cell);
return;
@@ -356,12 +411,24 @@ struct Smt2Worker
{
registers.insert(cell);
decls.push_back(stringf("(declare-fun |%s#%d| (|%s_s|) (_ BitVec %d)) ; %s\n",
- log_id(module), idcounter, log_id(module), GetSize(cell->getPort("\\Q")), log_signal(cell->getPort("\\Q"))));
+ get_id(module), idcounter, get_id(module), GetSize(cell->getPort("\\Q")), log_signal(cell->getPort("\\Q"))));
register_bv(cell->getPort("\\Q"), idcounter++);
recursive_cells.erase(cell);
return;
}
+ if (cell->type == "$anyconst")
+ {
+ registers.insert(cell);
+ decls.push_back(stringf("; yosys-smt2-%s %s#%d %s\n", cell->type.c_str() + 1, get_id(module), idcounter,
+ cell->attributes.count("\\src") ? cell->attributes.at("\\src").decode_string().c_str() : get_id(cell)));
+ decls.push_back(stringf("(declare-fun |%s#%d| (|%s_s|) (_ BitVec %d)) ; %s\n",
+ get_id(module), idcounter, get_id(module), GetSize(cell->getPort("\\Y")), log_signal(cell->getPort("\\Y"))));
+ register_bv(cell->getPort("\\Y"), idcounter++);
+ recursive_cells.erase(cell);
+ return;
+ }
+
if (cell->type == "$and") return export_bvop(cell, "(bvand A B)");
if (cell->type == "$or") return export_bvop(cell, "(bvor A B)");
if (cell->type == "$xor") return export_bvop(cell, "(bvxor A B)");
@@ -372,7 +439,13 @@ struct Smt2Worker
if (cell->type == "$sshl") return export_bvop(cell, "(bvshl A B)", 's');
if (cell->type == "$sshr") return export_bvop(cell, "(bvLshr A B)", 's');
- // FIXME: $shift $shiftx
+ if (cell->type.in("$shift", "$shiftx")) {
+ if (cell->getParam("\\B_SIGNED").as_bool()) {
+ /* FIXME */
+ } else {
+ return export_bvop(cell, "(bvlshr A B)", 's');
+ }
+ }
if (cell->type == "$lt") return export_bvop(cell, "(bvUlt A B)", 'b');
if (cell->type == "$le") return export_bvop(cell, "(bvUle A B)", 'b');
@@ -418,11 +491,12 @@ struct Smt2Worker
processed_expr = stringf("(ite %s %s %s)", get_bool(sig_s[i]).c_str(),
get_bv(sig_b.extract(i*width, width)).c_str(), processed_expr.c_str());
- if (verbose) log("%*s-> import cell: %s\n", 2+2*GetSize(recursive_cells), "",
- log_id(cell));
+ if (verbose)
+ log("%*s-> import cell: %s\n", 2+2*GetSize(recursive_cells), "", log_id(cell));
+
RTLIL::SigSpec sig = sigmap(cell->getPort("\\Y"));
decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
- log_id(module), idcounter, log_id(module), width, processed_expr.c_str(), log_signal(sig)));
+ get_id(module), idcounter, get_id(module), width, processed_expr.c_str(), log_signal(sig)));
register_bv(sig, idcounter++);
recursive_cells.erase(cell);
return;
@@ -441,22 +515,27 @@ struct Smt2Worker
int rd_ports = cell->getParam("\\RD_PORTS").as_int();
decls.push_back(stringf("(declare-fun |%s#%d#0| (|%s_s|) (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n",
- log_id(module), arrayid, log_id(module), abits, width, log_id(cell)));
+ get_id(module), arrayid, get_id(module), abits, width, get_id(cell)));
+ decls.push_back(stringf("; yosys-smt2-memory %s %d %d %d\n", get_id(cell), abits, width, rd_ports));
decls.push_back(stringf("(define-fun |%s_m %s| ((state |%s_s|)) (Array (_ BitVec %d) (_ BitVec %d)) (|%s#%d#0| state))\n",
- log_id(module), log_id(cell), log_id(module), abits, width, log_id(module), arrayid));
+ get_id(module), get_id(cell), get_id(module), abits, width, get_id(module), arrayid));
for (int i = 0; i < rd_ports; i++)
{
- std::string addr = get_bv(cell->getPort("\\RD_ADDR").extract(abits*i, abits));
+ SigSpec addr_sig = cell->getPort("\\RD_ADDR").extract(abits*i, abits);
SigSpec data_sig = cell->getPort("\\RD_DATA").extract(width*i, width);
+ std::string addr = get_bv(addr_sig);
if (cell->getParam("\\RD_CLK_ENABLE").extract(i).as_bool())
log_error("Read port %d (%s) of memory %s.%s is clocked. This is not supported by \"write_smt2\"! "
"Call \"memory\" with -nordff to avoid this error.\n", i, log_signal(data_sig), log_id(cell), log_id(module));
+ decls.push_back(stringf("(define-fun |%s_m:%d %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
+ get_id(module), i, get_id(cell), get_id(module), abits, addr.c_str(), log_signal(addr_sig)));
+
decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) (_ BitVec %d) (select (|%s#%d#0| state) %s)) ; %s\n",
- log_id(module), idcounter, log_id(module), width, log_id(module), arrayid, addr.c_str(), log_signal(data_sig)));
+ get_id(module), idcounter, get_id(module), width, get_id(module), arrayid, addr.c_str(), log_signal(data_sig)));
register_bv(data_sig, idcounter++);
}
@@ -465,6 +544,48 @@ struct Smt2Worker
return;
}
+ Module *m = module->design->module(cell->type);
+
+ if (m != nullptr)
+ {
+ decls.push_back(stringf("; yosys-smt2-cell %s %s\n", get_id(cell->type), get_id(cell->name)));
+ string cell_state = stringf("(|%s_h %s| state)", get_id(module), get_id(cell->name));
+
+ for (auto &conn : cell->connections())
+ {
+ Wire *w = m->wire(conn.first);
+ SigSpec sig = sigmap(conn.second);
+
+ if (w->port_output && !w->port_input) {
+ if (GetSize(w) > 1) {
+ if (bvmode) {
+ decls.push_back(stringf("(declare-fun |%s#%d| (|%s_s|) (_ BitVec %d)) ; %s\n",
+ get_id(module), idcounter, get_id(module), GetSize(w), log_signal(sig)));
+ register_bv(sig, idcounter++);
+ } else {
+ for (int i = 0; i < GetSize(w); i++) {
+ decls.push_back(stringf("(declare-fun |%s#%d| (|%s_s|) Bool) ; %s\n",
+ get_id(module), idcounter, get_id(module), log_signal(sig[i])));
+ register_bool(sig[i], idcounter++);
+ }
+ }
+ } else {
+ decls.push_back(stringf("(declare-fun |%s#%d| (|%s_s|) Bool) ; %s\n",
+ get_id(module), idcounter, get_id(module), log_signal(sig)));
+ register_bool(sig, idcounter++);
+ }
+ }
+ }
+
+ decls.push_back(stringf("(declare-fun |%s_h %s| (|%s_s|) |%s_s|)\n",
+ get_id(module), get_id(cell->name), get_id(module), get_id(cell->type)));
+
+ hiercells.insert(cell);
+ hiercells_queue.insert(cell);
+ recursive_cells.erase(cell);
+ return;
+ }
+
log_error("Unsupported cell type %s for cell %s.%s. (Maybe this cell type would be supported in -bv or -mem mode?)\n",
log_id(cell->type), log_id(module), log_id(cell));
}
@@ -474,42 +595,39 @@ struct Smt2Worker
if (verbose) log("=> export logic driving outputs\n");
pool<SigBit> reg_bits;
- if (regsmode) {
- for (auto cell : module->cells())
- if (cell->type.in("$_DFF_P_", "$_DFF_N_", "$dff")) {
- // not using sigmap -- we want the net directly at the dff output
- for (auto bit : cell->getPort("\\Q"))
- reg_bits.insert(bit);
- }
- }
+ for (auto cell : module->cells())
+ if (cell->type.in("$_DFF_P_", "$_DFF_N_", "$dff")) {
+ // not using sigmap -- we want the net directly at the dff output
+ for (auto bit : cell->getPort("\\Q"))
+ reg_bits.insert(bit);
+ }
for (auto wire : module->wires()) {
bool is_register = false;
- if (regsmode)
- for (auto bit : SigSpec(wire))
- if (reg_bits.count(bit))
- is_register = true;
+ for (auto bit : SigSpec(wire))
+ if (reg_bits.count(bit))
+ is_register = true;
if (wire->port_id || is_register || wire->get_bool_attribute("\\keep") || (wiresmode && wire->name[0] == '\\')) {
RTLIL::SigSpec sig = sigmap(wire);
if (wire->port_input)
- decls.push_back(stringf("; yosys-smt2-input %s %d\n", log_id(wire), wire->width));
+ decls.push_back(stringf("; yosys-smt2-input %s %d\n", get_id(wire), wire->width));
if (wire->port_output)
- decls.push_back(stringf("; yosys-smt2-output %s %d\n", log_id(wire), wire->width));
+ decls.push_back(stringf("; yosys-smt2-output %s %d\n", get_id(wire), wire->width));
if (is_register)
- decls.push_back(stringf("; yosys-smt2-register %s %d\n", log_id(wire), wire->width));
+ decls.push_back(stringf("; yosys-smt2-register %s %d\n", get_id(wire), wire->width));
if (wire->get_bool_attribute("\\keep") || (wiresmode && wire->name[0] == '\\'))
- decls.push_back(stringf("; yosys-smt2-wire %s %d\n", log_id(wire), wire->width));
+ decls.push_back(stringf("; yosys-smt2-wire %s %d\n", get_id(wire), wire->width));
if (bvmode && GetSize(sig) > 1) {
decls.push_back(stringf("(define-fun |%s_n %s| ((state |%s_s|)) (_ BitVec %d) %s)\n",
- log_id(module), log_id(wire), log_id(module), GetSize(sig), get_bv(sig).c_str()));
+ get_id(module), get_id(wire), get_id(module), GetSize(sig), get_bv(sig).c_str()));
} else {
for (int i = 0; i < GetSize(sig); i++)
if (GetSize(sig) > 1)
decls.push_back(stringf("(define-fun |%s_n %s %d| ((state |%s_s|)) Bool %s)\n",
- log_id(module), log_id(wire), i, log_id(module), get_bool(sig[i]).c_str()));
+ get_id(module), get_id(wire), i, get_id(module), get_bool(sig[i]).c_str()));
else
decls.push_back(stringf("(define-fun |%s_n %s| ((state |%s_s|)) Bool %s)\n",
- log_id(module), log_id(wire), log_id(module), get_bool(sig[i]).c_str()));
+ get_id(module), get_id(wire), get_id(module), get_bool(sig[i]).c_str()));
}
}
}
@@ -523,26 +641,28 @@ struct Smt2Worker
Const val = wire->attributes.at("\\init");
val.bits.resize(GetSize(sig));
if (bvmode && GetSize(sig) > 1) {
- init_list.push_back(stringf("(= %s #b%s) ; %s", get_bv(sig).c_str(), val.as_string().c_str(), log_id(wire)));
+ init_list.push_back(stringf("(= %s #b%s) ; %s", get_bv(sig).c_str(), val.as_string().c_str(), get_id(wire)));
} else {
for (int i = 0; i < GetSize(sig); i++)
- init_list.push_back(stringf("(= %s %s) ; %s", get_bool(sig[i]).c_str(), val.bits[i] == State::S1 ? "true" : "false", log_id(wire)));
+ init_list.push_back(stringf("(= %s %s) ; %s", get_bool(sig[i]).c_str(), val.bits[i] == State::S1 ? "true" : "false", get_id(wire)));
}
}
if (verbose) log("=> export logic driving asserts\n");
- vector<int> assert_list, assume_list;
+ vector<string> assert_list, assume_list;
for (auto cell : module->cells())
if (cell->type.in("$assert", "$assume")) {
string name_a = get_bool(cell->getPort("\\A"));
string name_en = get_bool(cell->getPort("\\EN"));
+ decls.push_back(stringf("; yosys-smt2-%s %s#%d %s\n", cell->type.c_str() + 1, get_id(module), idcounter,
+ cell->attributes.count("\\src") ? cell->attributes.at("\\src").decode_string().c_str() : get_id(cell)));
decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) Bool (or %s (not %s))) ; %s\n",
- log_id(module), idcounter, log_id(module), name_a.c_str(), name_en.c_str(), log_id(cell)));
+ get_id(module), idcounter, get_id(module), name_a.c_str(), name_en.c_str(), get_id(cell)));
if (cell->type == "$assert")
- assert_list.push_back(idcounter++);
+ assert_list.push_back(stringf("(|%s#%d| state)", get_id(module), idcounter++));
else
- assume_list.push_back(idcounter++);
+ assume_list.push_back(stringf("(|%s#%d| state)", get_id(module), idcounter++));
}
for (int iter = 1; !registers.empty(); iter++)
@@ -558,14 +678,21 @@ struct Smt2Worker
{
std::string expr_d = get_bool(cell->getPort("\\D"));
std::string expr_q = get_bool(cell->getPort("\\Q"), "next_state");
- trans.push_back(stringf(" (= %s %s) ; %s %s\n", expr_d.c_str(), expr_q.c_str(), log_id(cell), log_signal(cell->getPort("\\Q"))));
+ trans.push_back(stringf(" (= %s %s) ; %s %s\n", expr_d.c_str(), expr_q.c_str(), get_id(cell), log_signal(cell->getPort("\\Q"))));
}
if (cell->type == "$dff")
{
std::string expr_d = get_bv(cell->getPort("\\D"));
std::string expr_q = get_bv(cell->getPort("\\Q"), "next_state");
- trans.push_back(stringf(" (= %s %s) ; %s %s\n", expr_d.c_str(), expr_q.c_str(), log_id(cell), log_signal(cell->getPort("\\Q"))));
+ trans.push_back(stringf(" (= %s %s) ; %s %s\n", expr_d.c_str(), expr_q.c_str(), get_id(cell), log_signal(cell->getPort("\\Q"))));
+ }
+
+ if (cell->type == "$anyconst")
+ {
+ std::string expr_d = get_bv(cell->getPort("\\Y"));
+ std::string expr_q = get_bv(cell->getPort("\\Y"), "next_state");
+ trans.push_back(stringf(" (= %s %s) ; %s %s\n", expr_d.c_str(), expr_q.c_str(), get_id(cell), log_signal(cell->getPort("\\Y"))));
}
if (cell->type == "$mem")
@@ -583,56 +710,144 @@ struct Smt2Worker
std::string mask = get_bv(cell->getPort("\\WR_EN").extract(width*i, width));
data = stringf("(bvor (bvand %s %s) (bvand (select (|%s#%d#%d| state) %s) (bvnot %s)))",
- data.c_str(), mask.c_str(), log_id(module), arrayid, i, addr.c_str(), mask.c_str());
+ data.c_str(), mask.c_str(), get_id(module), arrayid, i, addr.c_str(), mask.c_str());
decls.push_back(stringf("(define-fun |%s#%d#%d| ((state |%s_s|)) (Array (_ BitVec %d) (_ BitVec %d)) "
"(store (|%s#%d#%d| state) %s %s)) ; %s\n",
- log_id(module), arrayid, i+1, log_id(module), abits, width,
- log_id(module), arrayid, i, addr.c_str(), data.c_str(), log_id(cell)));
+ get_id(module), arrayid, i+1, get_id(module), abits, width,
+ get_id(module), arrayid, i, addr.c_str(), data.c_str(), get_id(cell)));
+ }
+
+ std::string expr_d = stringf("(|%s#%d#%d| state)", get_id(module), arrayid, wr_ports);
+ std::string expr_q = stringf("(|%s#%d#0| next_state)", get_id(module), arrayid);
+ trans.push_back(stringf(" (= %s %s) ; %s\n", expr_d.c_str(), expr_q.c_str(), get_id(cell)));
+
+ Const init_data = cell->getParam("\\INIT");
+ int memsize = cell->getParam("\\SIZE").as_int();
+
+ for (int i = 0; i < memsize; i++)
+ {
+ if (i*width >= GetSize(init_data))
+ break;
+
+ Const initword = init_data.extract(i*width, width, State::Sx);
+ bool gen_init_constr = false;
+
+ for (auto bit : initword.bits)
+ if (bit == State::S0 || bit == State::S1)
+ gen_init_constr = true;
+
+ if (gen_init_constr) {
+ init_list.push_back(stringf("(= (select (|%s#%d#0| state) #b%s) #b%s) ; %s[%d]",
+ get_id(module), arrayid, Const(i, abits).as_string().c_str(),
+ initword.as_string().c_str(), get_id(cell), i));
+ }
}
+ }
+ }
+ }
+
+ if (verbose) log("=> export logic driving hierarchical cells\n");
- std::string expr_d = stringf("(|%s#%d#%d| state)", log_id(module), arrayid, wr_ports);
- std::string expr_q = stringf("(|%s#%d#0| next_state)", log_id(module), arrayid);
- trans.push_back(stringf(" (= %s %s) ; %s\n", expr_d.c_str(), expr_q.c_str(), log_id(cell)));
+ while (!hiercells_queue.empty())
+ {
+ std::set<RTLIL::Cell*> queue;
+ queue.swap(hiercells_queue);
+
+ for (auto cell : queue)
+ {
+ string cell_state = stringf("(|%s_h %s| state)", get_id(module), get_id(cell->name));
+ Module *m = module->design->module(cell->type);
+ log_assert(m != nullptr);
+
+ for (auto &conn : cell->connections())
+ {
+ Wire *w = m->wire(conn.first);
+ SigSpec sig = sigmap(conn.second);
+
+ if (bvmode || GetSize(w) == 1) {
+ hier.push_back(stringf(" (= %s (|%s_n %s| %s)) ; %s.%s\n", (GetSize(w) > 1 ? get_bv(sig) : get_bool(sig)).c_str(),
+ get_id(cell->type), get_id(w), cell_state.c_str(), get_id(cell->type), get_id(w)));
+ } else {
+ for (int i = 0; i < GetSize(w); i++)
+ hier.push_back(stringf(" (= %s (|%s_n %s %d| %s)) ; %s.%s[%d]\n", get_bool(sig[i]).c_str(),
+ get_id(cell->type), get_id(w), i, cell_state.c_str(), get_id(cell->type), get_id(w), i));
+ }
}
}
}
+ if (verbose) log("=> finalizing SMT2 representation of %s.\n", log_id(module));
+
+ for (auto c : hiercells) {
+ assert_list.push_back(stringf("(|%s_a| (|%s_h %s| state))", get_id(c->type), get_id(module), get_id(c->name)));
+ assume_list.push_back(stringf("(|%s_u| (|%s_h %s| state))", get_id(c->type), get_id(module), get_id(c->name)));
+ init_list.push_back(stringf("(|%s_i| (|%s_h %s| state))", get_id(c->type), get_id(module), get_id(c->name)));
+ hier.push_back(stringf(" (|%s_h| (|%s_h %s| state))\n", get_id(c->type), get_id(module), get_id(c->name)));
+ trans.push_back(stringf(" (|%s_t| (|%s_h %s| state) (|%s_h %s| next_state))\n",
+ get_id(c->type), get_id(module), get_id(c->name), get_id(module), get_id(c->name)));
+ }
+
string assert_expr = assert_list.empty() ? "true" : "(and";
if (!assert_list.empty()) {
- for (int i : assert_list)
- assert_expr += stringf(" (|%s#%d| state)", log_id(module), i);
- assert_expr += ")";
+ if (GetSize(assert_list) == 1) {
+ assert_expr = "\n " + assert_list.front() + "\n";
+ } else {
+ for (auto &str : assert_list)
+ assert_expr += stringf("\n %s", str.c_str());
+ assert_expr += "\n)";
+ }
}
decls.push_back(stringf("(define-fun |%s_a| ((state |%s_s|)) Bool %s)\n",
- log_id(module), log_id(module), assert_expr.c_str()));
+ get_id(module), get_id(module), assert_expr.c_str()));
string assume_expr = assume_list.empty() ? "true" : "(and";
if (!assume_list.empty()) {
- for (int i : assume_list)
- assume_expr += stringf(" (|%s#%d| state)", log_id(module), i);
- assume_expr += ")";
+ if (GetSize(assume_list) == 1) {
+ assume_expr = "\n " + assume_list.front() + "\n";
+ } else {
+ for (auto &str : assume_list)
+ assume_expr += stringf("\n %s", str.c_str());
+ assume_expr += "\n)";
+ }
}
decls.push_back(stringf("(define-fun |%s_u| ((state |%s_s|)) Bool %s)\n",
- log_id(module), log_id(module), assume_expr.c_str()));
+ get_id(module), get_id(module), assume_expr.c_str()));
string init_expr = init_list.empty() ? "true" : "(and";
if (!init_list.empty()) {
- for (auto &str : init_list)
- init_expr += stringf("\n\t%s", str.c_str());
- init_expr += "\n)";
+ if (GetSize(init_list) == 1) {
+ init_expr = "\n " + init_list.front() + "\n";
+ } else {
+ for (auto &str : init_list)
+ init_expr += stringf("\n %s", str.c_str());
+ init_expr += "\n)";
+ }
}
decls.push_back(stringf("(define-fun |%s_i| ((state |%s_s|)) Bool %s)\n",
- log_id(module), log_id(module), init_expr.c_str()));
+ get_id(module), get_id(module), init_expr.c_str()));
}
void write(std::ostream &f)
{
+ f << stringf("; yosys-smt2-module %s\n", get_id(module));
+
for (auto it : decls)
f << it;
- f << stringf("; yosys-smt2-module %s\n", log_id(module));
- f << stringf("(define-fun |%s_t| ((state |%s_s|) (next_state |%s_s|)) Bool ", log_id(module), log_id(module), log_id(module));
+ f << stringf("(define-fun |%s_h| ((state |%s_s|)) Bool ", get_id(module), get_id(module));
+ if (GetSize(hier) > 1) {
+ f << "(and\n";
+ for (auto it : hier)
+ f << it;
+ f << "))\n";
+ } else
+ if (GetSize(hier) == 1)
+ f << "\n" + hier.front() + ")\n";
+ else
+ f << "true)\n";
+
+ f << stringf("(define-fun |%s_t| ((state |%s_s|) (next_state |%s_s|)) Bool ", get_id(module), get_id(module), get_id(module));
if (GetSize(trans) > 1) {
f << "(and\n";
for (auto it : trans)
@@ -643,7 +858,7 @@ struct Smt2Worker
f << "\n" + trans.front() + ")";
else
f << "true)";
- f << stringf(" ; end of module %s\n", log_id(module));
+ f << stringf(" ; end of module %s\n", get_id(module));
}
};
@@ -661,10 +876,10 @@ struct Smt2Backend : public Backend {
log("\n");
log("The '<mod>_s' sort represents a module state. Additional '<mod>_n' functions\n");
log("are provided that can be used to access the values of the signals in the module.\n");
- log("Only ports, and signals with the 'keep' attribute set are made available via\n");
- log("such functions. Without the -bv option, multi-bit wires are exported as\n");
- log("separate functions of type Bool for the individual bits. With the -bv option\n");
- log("multi-bit wires are exported as single functions of type BitVec.\n");
+ log("By default only ports, registers, and wires with the 'keep' attribute set are\n");
+ log("made available via such functions. With the -nobv option, multi-bit wires are\n");
+ log("exported as separate functions of type Bool for the individual bits. Without\n");
+ log("-nobv multi-bit wires are exported as single functions of type BitVec.\n");
log("\n");
log("The '<mod>_t' function evaluates to 'true' when the given pair of states\n");
log("describes a valid state transition.\n");
@@ -676,29 +891,33 @@ struct Smt2Backend : public Backend {
log("the assumptions in the module.\n");
log("\n");
log("The '<mod>_i' function evaluates to 'true' when the given state conforms\n");
- log("to the initial state.\n");
+ log("to the initial state. Furthermore the '<mod>_is' function should be asserted\n");
+ log("to be true for initial states in addition to '<mod>_i', and should be\n");
+ log("asserted to be false for non-initial states.\n");
+ log("\n");
+ log("For hierarchical designs, the '<mod>_h' function must be asserted for each\n");
+ log("state to establish the design hierarchy. The '<mod>_h <cellname>' function\n");
+ log("evaluates to the state corresponding to the given cell within <mod>.\n");
log("\n");
log(" -verbose\n");
log(" this will print the recursive walk used to export the modules.\n");
log("\n");
- log(" -bv\n");
- log(" enable support for BitVec (FixedSizeBitVectors theory). with this\n");
- log(" option set multi-bit wires are represented using the BitVec sort and\n");
+ log(" -nobv\n");
+ log(" disable support for BitVec (FixedSizeBitVectors theory). without this\n");
+ log(" option multi-bit wires are represented using the BitVec sort and\n");
log(" support for coarse grain cells (incl. arithmetic) is enabled.\n");
log("\n");
- log(" -mem\n");
- log(" enable support for memories (via ArraysEx theory). this option\n");
- log(" also implies -bv. only $mem cells without merged registers in\n");
+ log(" -nomem\n");
+ log(" disable support for memories (via ArraysEx theory). this option is\n");
+ log(" implied by -nobv. only $mem cells without merged registers in\n");
log(" read ports are supported. call \"memory\" with -nordff to make sure\n");
log(" that no registers are merged into $mem read ports. '<mod>_m' functions\n");
log(" will be generated for accessing the arrays that are used to represent\n");
log(" memories.\n");
log("\n");
- log(" -regs\n");
- log(" also create '<mod>_n' functions for all registers.\n");
- log("\n");
log(" -wires\n");
- log(" also create '<mod>_n' functions for all public wires.\n");
+ log(" create '<mod>_n' functions for all public wires. by default only ports,\n");
+ log(" registers, and wires with the 'keep' attribute are exported.\n");
log("\n");
log(" -tpl <template_file>\n");
log(" use the given template file. the line containing only the token '%%%%'\n");
@@ -756,9 +975,9 @@ struct Smt2Backend : public Backend {
virtual void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design)
{
std::ifstream template_f;
- bool bvmode = false, memmode = false, regsmode = false, wiresmode = false, verbose = false;
+ bool bvmode = true, memmode = true, wiresmode = false, verbose = false;
- log_header("Executing SMT2 backend.\n");
+ log_header(design, "Executing SMT2 backend.\n");
size_t argidx;
for (argidx = 1; argidx < args.size(); argidx++)
@@ -769,17 +988,17 @@ struct Smt2Backend : public Backend {
log_error("Can't open template file `%s'.\n", args[argidx].c_str());
continue;
}
- if (args[argidx] == "-bv") {
- bvmode = true;
+ if (args[argidx] == "-bv" || args[argidx] == "-mem") {
+ log_warning("Options -bv and -mem are now the default. Support for -bv and -mem will be removed in the future.\n");
continue;
}
- if (args[argidx] == "-mem") {
- bvmode = true;
- memmode = true;
+ if (args[argidx] == "-nobv") {
+ bvmode = false;
+ memmode = false;
continue;
}
- if (args[argidx] == "-regs") {
- regsmode = true;
+ if (args[argidx] == "-nomem") {
+ memmode = false;
continue;
}
if (args[argidx] == "-wires") {
@@ -808,18 +1027,62 @@ struct Smt2Backend : public Backend {
*f << stringf("; SMT-LIBv2 description generated by %s\n", yosys_version_str);
- for (auto module : design->modules())
+ if (!bvmode)
+ *f << stringf("; yosys-smt2-nobv\n");
+
+ if (!memmode)
+ *f << stringf("; yosys-smt2-nomem\n");
+
+ std::vector<RTLIL::Module*> sorted_modules;
+
+ // extract module dependencies
+ std::map<RTLIL::Module*, std::set<RTLIL::Module*>> module_deps;
+ for (auto &mod_it : design->modules_) {
+ module_deps[mod_it.second] = std::set<RTLIL::Module*>();
+ for (auto &cell_it : mod_it.second->cells_)
+ if (design->modules_.count(cell_it.second->type) > 0)
+ module_deps[mod_it.second].insert(design->modules_.at(cell_it.second->type));
+ }
+
+ // simple good-enough topological sort
+ // (O(n*m) on n elements and depth m)
+ while (module_deps.size() > 0) {
+ size_t sorted_modules_idx = sorted_modules.size();
+ for (auto &it : module_deps) {
+ for (auto &dep : it.second)
+ if (module_deps.count(dep) > 0)
+ goto not_ready_yet;
+ // log("Next in topological sort: %s\n", RTLIL::id2cstr(it.first->name));
+ sorted_modules.push_back(it.first);
+ not_ready_yet:;
+ }
+ if (sorted_modules_idx == sorted_modules.size())
+ log_error("Cyclic dependency between modules found! Cycle includes module %s.\n", RTLIL::id2cstr(module_deps.begin()->first->name));
+ while (sorted_modules_idx < sorted_modules.size())
+ module_deps.erase(sorted_modules.at(sorted_modules_idx++));
+ }
+
+ Module *topmod = design->top_module();
+ std::string topmod_id;
+
+ for (auto module : sorted_modules)
{
if (module->get_bool_attribute("\\blackbox") || module->has_memories_warn() || module->has_processes_warn())
continue;
log("Creating SMT-LIBv2 representation of module %s.\n", log_id(module));
- Smt2Worker worker(module, bvmode, memmode, regsmode, wiresmode, verbose);
+ Smt2Worker worker(module, bvmode, memmode, wiresmode, verbose);
worker.run();
worker.write(*f);
+
+ if (module == topmod)
+ topmod_id = worker.get_id(module);
}
+ if (topmod)
+ *f << stringf("; yosys-smt2-topmod %s\n", topmod_id.c_str());
+
*f << stringf("; end of yosys output\n");
if (template_f.is_open()) {
diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index f2911b3e..bb763647 100644
--- a/backends/smt2/smtbmc.py
+++ b/backends/smt2/smtbmc.py
@@ -19,66 +19,119 @@
import os, sys, getopt, re
##yosys-sys-path##
-from smtio import smtio, smtopts, mkvcd
+from smtio import SmtIo, SmtOpts, MkVcd
+from collections import defaultdict
skip_steps = 0
step_size = 1
num_steps = 20
vcdfile = None
+vlogtbfile = None
+inconstr = list()
+outconstr = None
+gentrace = False
tempind = False
+dumpall = False
assume_skipped = None
+final_only = False
topmod = None
-so = smtopts()
+noinfo = False
+so = SmtOpts()
def usage():
print("""
yosys-smtbmc [options] <yosys_smt2_output>
- -t <num_steps>, -t <skip_steps>:<num_steps>
- default: skip_steps=0, num_steps=20
+ -t <num_steps>
+ -t <skip_steps>:<num_steps>
+ -t <skip_steps>:<step_size>:<num_steps>
+ default: skip_steps=0, step_size=1, num_steps=20
- -u <start_step>
- assume asserts in skipped steps in BMC
-
- -S <step_size>
- proof <step_size> time steps at once
-
- -c <vcd_filename>
- write counter-example to this VCD file
- (hint: use 'write_smt2 -wires' for maximum
- coverage of signals in generated VCD file)
+ -g
+ generate an arbitrary trace that satisfies
+ all assertions and assumptions.
-i
instead of BMC run temporal induction
-m <module_name>
name of the top module
+
+ --smtc <constr_filename>
+ read constraints file
+
+ --noinfo
+ only run the core proof, do not collect and print any
+ additional information (e.g. which assert failed)
+
+ --final-only
+ only check final constraints, assume base case
+
+ --assume-skipped <start_step>
+ assume asserts in skipped steps in BMC.
+ no assumptions are created for skipped steps
+ before <start_step>.
+
+ --dump-vcd <vcd_filename>
+ write trace to this VCD file
+ (hint: use 'write_smt2 -wires' for maximum
+ coverage of signals in generated VCD file)
+
+ --dump-vlogtb <verilog_filename>
+ write trace as Verilog test bench
+
+ --dump-smtc <constr_filename>
+ write trace as constraints file
+
+ --dump-all
+ when using -g or -i, create a dump file for each
+ step. The character '%' is replaces in all dump
+ filenames with the step number.
""" + so.helpmsg())
sys.exit(1)
try:
- opts, args = getopt.getopt(sys.argv[1:], so.optstr + "t:u:S:c:im:")
+ opts, args = getopt.getopt(sys.argv[1:], so.shortopts + "t:igm:", so.longopts +
+ ["final-only", "assume-skipped=", "smtc=", "dump-vcd=", "dump-vlogtb=", "dump-smtc=", "dump-all", "noinfo"])
except:
usage()
for o, a in opts:
if o == "-t":
- match = re.match(r"(\d+):(.*)", a)
- if match:
- skip_steps = int(match.group(1))
- num_steps = int(match.group(2))
+ a = a.split(":")
+ if len(a) == 1:
+ num_steps = int(a[0])
+ elif len(a) == 2:
+ skip_steps = int(a[0])
+ num_steps = int(a[1])
+ elif len(a) == 3:
+ skip_steps = int(a[0])
+ step_size = int(a[1])
+ num_steps = int(a[2])
else:
- num_steps = int(a)
- elif o == "-u":
+ assert 0
+ elif o == "--assume-skipped":
assume_skipped = int(a)
- elif o == "-S":
- step_size = int(a)
- elif o == "-c":
+ elif o == "--final-only":
+ final_only = True
+ elif o == "--smtc":
+ inconstr.append(a)
+ elif o == "--dump-vcd":
vcdfile = a
+ elif o == "--dump-vlogtb":
+ vlogtbfile = a
+ elif o == "--dump-smtc":
+ outconstr = a
+ elif o == "--dump-all":
+ dumpall = True
+ elif o == "--noinfo":
+ noinfo = True
elif o == "-i":
tempind = True
+ elif o == "-g":
+ gentrace = True
elif o == "-m":
topmod = a
elif so.handle(o, a):
@@ -90,73 +143,422 @@ if len(args) != 1:
usage()
-smt = smtio(opts=so)
+constr_final_start = None
+constr_asserts = defaultdict(list)
+constr_assumes = defaultdict(list)
+
+for fn in inconstr:
+ current_states = None
+ current_line = 0
+
+ with open(fn, "r") as f:
+ for line in f:
+ current_line += 1
+
+ if line.startswith("#"):
+ continue
+
+ tokens = line.split()
+
+ if len(tokens) == 0:
+ continue
+
+ if tokens[0] == "initial":
+ current_states = set()
+ if not tempind:
+ current_states.add(0)
+ continue
+
+ if tokens[0] == "final":
+ constr_final = True
+ if len(tokens) == 1:
+ current_states = set(["final-%d" % i for i in range(0, num_steps+1)])
+ constr_final_start = 0
+ elif len(tokens) == 2:
+ i = int(tokens[1])
+ assert i < 0
+ current_states = set(["final-%d" % i for i in range(-i, num_steps+1)])
+ constr_final_start = -i if constr_final_start is None else min(constr_final_start, -i)
+ else:
+ assert 0
+ continue
+
+ if tokens[0] == "state":
+ current_states = set()
+ if not tempind:
+ for token in tokens[1:]:
+ tok = token.split(":")
+ if len(tok) == 1:
+ current_states.add(int(token))
+ elif len(tok) == 2:
+ lower = int(tok[0])
+ if tok[1] == "*":
+ upper = num_steps
+ else:
+ upper = int(tok[1])
+ for i in range(lower, upper+1):
+ current_states.add(i)
+ else:
+ assert 0
+ continue
+
+ if tokens[0] == "always":
+ if len(tokens) == 1:
+ current_states = set(range(0, num_steps+1))
+ elif len(tokens) == 2:
+ i = int(tokens[1])
+ assert i < 0
+ current_states = set(range(-i, num_steps+1))
+ else:
+ assert 0
+ continue
+
+ if tokens[0] == "assert":
+ assert current_states is not None
+
+ for state in current_states:
+ constr_asserts[state].append(("%s:%d" % (fn, current_line), " ".join(tokens[1:])))
+
+ continue
+
+ if tokens[0] == "assume":
+ assert current_states is not None
+
+ for state in current_states:
+ constr_assumes[state].append(("%s:%d" % (fn, current_line), " ".join(tokens[1:])))
+
+ continue
+
+ assert 0
+
+
+def get_constr_expr(db, state, final=False, getvalues=False):
+ if final:
+ if ("final-%d" % state) not in db:
+ return ([], [], []) if getvalues else "true"
+ else:
+ if state not in db:
+ return ([], [], []) if getvalues else "true"
+
+ netref_regex = re.compile(r'(^|[( ])\[(-?[0-9]+:|)([^\]]+)\](?=[ )]|$)')
+
+ def replace_netref(match):
+ state_sel = match.group(2)
+
+ if state_sel == "":
+ st = state
+ elif state_sel[0] == "-":
+ st = state + int(state_sel[:-1])
+ else:
+ st = int(state_sel[:-1])
+
+ expr = smt.net_expr(topmod, "s%d" % st, smt.get_path(topmod, match.group(3)))
+
+ return match.group(1) + expr
+
+ expr_list = list()
+ for loc, expr in db[("final-%d" % state) if final else state]:
+ actual_expr = netref_regex.sub(replace_netref, expr)
+ if getvalues:
+ expr_list.append((loc, expr, actual_expr))
+ else:
+ expr_list.append(actual_expr)
+
+ if getvalues:
+ loc_list, expr_list, acual_expr_list = zip(*expr_list)
+ value_list = smt.get_list(acual_expr_list)
+ return loc_list, expr_list, value_list
+
+ if len(expr_list) == 0:
+ return "true"
+
+ if len(expr_list) == 1:
+ return expr_list[0]
+
+ return "(and %s)" % " ".join(expr_list)
-print("%s Solver: %s" % (smt.timestamp(), so.solver))
-smt.setup("QF_AUFBV")
-debug_nets = set()
-debug_nets_re = re.compile(r"^; yosys-smt2-(input|output|register|wire) (\S+) (\d+)")
+smt = SmtIo(opts=so)
+
+def print_msg(msg):
+ print("%s %s" % (smt.timestamp(), msg))
+ sys.stdout.flush()
+
+print_msg("Solver: %s" % (so.solver))
with open(args[0], "r") as f:
for line in f:
- match = debug_nets_re.match(line)
- if match:
- debug_nets.add(match.group(2))
- if line.startswith("; yosys-smt2-module") and topmod is None:
- topmod = line.split()[2]
smt.write(line)
+if topmod is None:
+ topmod = smt.topmod
+
assert topmod is not None
+assert topmod in smt.modinfo
+
+
+def write_vcd_trace(steps_start, steps_stop, index):
+ filename = vcdfile.replace("%", index)
+ print_msg("Writing trace to VCD file: %s" % (filename))
+
+ with open(filename, "w") as vcd_file:
+ vcd = MkVcd(vcd_file)
+ path_list = list()
+
+ for netpath in sorted(smt.hiernets(topmod)):
+ hidden_net = False
+ for n in netpath:
+ if n.startswith("$"):
+ hidden_net = True
+ if not hidden_net:
+ vcd.add_net([topmod] + netpath, smt.net_width(topmod, netpath))
+ path_list.append(netpath)
+
+ for i in range(steps_start, steps_stop):
+ vcd.set_time(i)
+ value_list = smt.get_net_bin_list(topmod, path_list, "s%d" % i)
+ for path, value in zip(path_list, value_list):
+ vcd.set_net([topmod] + path, value)
+
+ vcd.set_time(steps_stop)
+
+
+def write_vlogtb_trace(steps_start, steps_stop, index):
+ filename = vlogtbfile.replace("%", index)
+ print_msg("Writing trace to Verilog testbench: %s" % (filename))
+
+ with open(filename, "w") as f:
+ print("module testbench;", file=f)
+ print(" reg [4095:0] vcdfile;", file=f)
+ print(" reg clock = 0, genclock = 1;", file=f)
+
+ primary_inputs = list()
+ clock_inputs = set()
+
+ for name in smt.modinfo[topmod].inputs:
+ if name in ["clk", "clock", "CLK", "CLOCK"]:
+ clock_inputs.add(name)
+ width = smt.modinfo[topmod].wsize[name]
+ primary_inputs.append((name, width))
+
+ for name, width in primary_inputs:
+ if name in clock_inputs:
+ print(" wire [%d:0] PI_%s = clock;" % (width-1, name), file=f)
+ else:
+ print(" reg [%d:0] PI_%s;" % (width-1, name), file=f)
+
+ print(" %s UUT (" % topmod, file=f)
+ print(",\n".join(" .{name}(PI_{name})".format(name=name) for name, _ in primary_inputs), file=f)
+ print(" );", file=f)
+
+ print(" initial begin", file=f)
+ print(" if ($value$plusargs(\"vcd=%s\", vcdfile)) begin", file=f)
+ print(" $dumpfile(vcdfile);", file=f)
+ print(" $dumpvars(0, testbench);", file=f)
+ print(" end", file=f)
+ print(" while (genclock) begin", file=f)
+ print(" #5; clock = 0;", file=f)
+ print(" #5; clock = 1;", file=f)
+ print(" end", file=f)
+ print(" end", file=f)
+
+ print(" initial begin", file=f)
+
+ regs = sorted(smt.hiernets(topmod, regs_only=True))
+ regvals = smt.get_net_bin_list(topmod, regs, "s%d" % steps_start)
+
+ print(" #1;", file=f)
+ for reg, val in zip(regs, regvals):
+ hidden_net = False
+ for n in reg:
+ if n.startswith("$"):
+ hidden_net = True
+ print(" %sUUT.%s = %d'b%s;" % ("// " if hidden_net else "", ".".join(reg), len(val), val), file=f)
+
+ mems = sorted(smt.hiermems(topmod))
+ for mempath in mems:
+ abits, width, ports = smt.mem_info(topmod, "s%d" % steps_start, mempath)
+ mem = smt.mem_expr(topmod, "s%d" % steps_start, mempath)
+
+ addr_expr_list = list()
+ for i in range(steps_start, steps_stop):
+ for j in range(ports):
+ addr_expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, j))
+
+ addr_list = set()
+ for val in smt.get_list(addr_expr_list):
+ addr_list.add(smt.bv2int(val))
+
+ expr_list = list()
+ for i in addr_list:
+ expr_list.append("(select %s #b%s)" % (mem, format(i, "0%db" % abits)))
+
+ for i, val in zip(addr_list, smt.get_list(expr_list)):
+ val = smt.bv2bin(val)
+ print(" UUT.%s[%d] = %d'b%s;" % (".".join(mempath), i, len(val), val), file=f)
+
+ for i in range(steps_start, steps_stop):
+ pi_names = [[name] for name, _ in primary_inputs if name not in clock_inputs]
+ pi_values = smt.get_net_bin_list(topmod, pi_names, "s%d" % i)
+
+ print(" #1;", file=f)
+ print(" // state %d" % i, file=f)
+ if i > 0:
+ print(" @(posedge clock);", file=f)
+ for name, val in zip(pi_names, pi_values):
+ print(" PI_%s <= %d'b%s;" % (".".join(name), len(val), val), file=f)
+
+ print(" genclock = 0;", file=f)
+ print(" end", file=f)
+
+ print("endmodule", file=f)
+
+
+def write_constr_trace(steps_start, steps_stop, index):
+ filename = outconstr.replace("%", index)
+ print_msg("Writing trace to constraints file: %s" % (filename))
+
+ with open(filename, "w") as f:
+ primary_inputs = list()
+
+ for name in smt.modinfo[topmod].inputs:
+ width = smt.modinfo[topmod].wsize[name]
+ primary_inputs.append((name, width))
+
+ if steps_start == 0:
+ print("initial", file=f)
+ else:
+ print("state %d" % steps_start, file=f)
+
+ regnames = sorted(smt.hiernets(topmod, regs_only=True))
+ regvals = smt.get_net_list(topmod, regnames, "s%d" % steps_start)
+
+ for name, val in zip(regnames, regvals):
+ print("assume (= [%s] %s)" % (".".join(name), val), file=f)
+
+ mems = sorted(smt.hiermems(topmod))
+ for mempath in mems:
+ abits, width, ports = smt.mem_info(topmod, "s%d" % steps_start, mempath)
+ mem = smt.mem_expr(topmod, "s%d" % steps_start, mempath)
+
+ addr_expr_list = list()
+ for i in range(steps_start, steps_stop):
+ for j in range(ports):
+ addr_expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, j))
+
+ addr_list = set((smt.bv2int(val) for val in smt.get_list(addr_expr_list)))
+
+ expr_list = list()
+ for i in addr_list:
+ expr_list.append("(select %s #b%s)" % (mem, format(i, "0%db" % abits)))
+
+ for i, val in zip(addr_list, smt.get_list(expr_list)):
+ print("assume (= (select [%s] #b%s) %s)" % (".".join(mempath), format(i, "0%db" % abits), val), file=f)
+
+ for k in range(steps_start, steps_stop):
+ print("", file=f)
+ print("state %d" % k, file=f)
+
+ pi_names = [[name] for name, _ in sorted(primary_inputs)]
+ pi_values = smt.get_net_list(topmod, pi_names, "s%d" % k)
+
+ for name, val in zip(pi_names, pi_values):
+ print("assume (= [%s] %s)" % (".".join(name), val), file=f)
+
+
+def write_trace(steps_start, steps_stop, index):
+ if vcdfile is not None:
+ write_vcd_trace(steps_start, steps_stop, index)
+
+ if vlogtbfile is not None:
+ write_vlogtb_trace(steps_start, steps_stop, index)
+
+ if outconstr is not None:
+ write_constr_trace(steps_start, steps_stop, index)
+
+
+def print_failed_asserts_worker(mod, state, path):
+ assert mod in smt.modinfo
+
+ if smt.get("(|%s_a| %s)" % (mod, state)) in ["true", "#b1"]:
+ return
+
+ for cellname, celltype in smt.modinfo[mod].cells.items():
+ print_failed_asserts_worker(celltype, "(|%s_h %s| %s)" % (mod, cellname, state), path + "." + cellname)
+
+ for assertfun, assertinfo in smt.modinfo[mod].asserts.items():
+ if smt.get("(|%s| %s)" % (assertfun, state)) in ["false", "#b0"]:
+ print_msg("Assert failed in %s: %s" % (path, assertinfo))
-def write_vcd_model(steps):
- print("%s Writing model to VCD file." % smt.timestamp())
+def print_failed_asserts(state, final=False):
+ if noinfo: return
+ loc_list, expr_list, value_list = get_constr_expr(constr_asserts, state, final=final, getvalues=True)
- vcd = mkvcd(open(vcdfile, "w"))
- for netname in sorted(debug_nets):
- width = len(smt.get_net_bin(topmod, netname, "s0"))
- vcd.add_net(netname, width)
+ for loc, expr, value in zip(loc_list, expr_list, value_list):
+ if smt.bv2int(value) == 0:
+ print_msg("Assert %s failed: %s" % (loc, expr))
- for i in range(steps):
- vcd.set_time(i)
- for netname in debug_nets:
- vcd.set_net(netname, smt.get_net_bin(topmod, netname, "s%d" % i))
+ if not final:
+ print_failed_asserts_worker(topmod, "s%d" % state, topmod)
- vcd.set_time(steps)
+
+def print_anyconsts_worker(mod, state, path):
+ assert mod in smt.modinfo
+
+ for cellname, celltype in smt.modinfo[mod].cells.items():
+ print_anyconsts_worker(celltype, "(|%s_h %s| %s)" % (mod, cellname, state), path + "." + cellname)
+
+ for fun, info in smt.modinfo[mod].anyconsts.items():
+ print_msg("Value for anyconst in %s (%s): %d" % (path, info, smt.bv2int(smt.get("(|%s| %s)" % (fun, state)))))
+
+
+def print_anyconsts(state):
+ if noinfo: return
+ print_anyconsts_worker(topmod, "s%d" % state, topmod)
if tempind:
retstatus = False
skip_counter = step_size
for step in range(num_steps, -1, -1):
- smt.write("(declare-fun s%d () %s_s)" % (step, topmod))
- smt.write("(assert (%s_u s%d))" % (topmod, step))
+ smt.write("(declare-fun s%d () |%s_s|)" % (step, topmod))
+ smt.write("(assert (|%s_u| s%d))" % (topmod, step))
+ smt.write("(assert (|%s_h| s%d))" % (topmod, step))
+ smt.write("(assert (not (|%s_is| s%d)))" % (topmod, step))
+ smt.write("(assert %s)" % get_constr_expr(constr_assumes, step))
if step == num_steps:
- smt.write("(assert (not (%s_a s%d)))" % (topmod, step))
+ smt.write("(assert (not (and (|%s_a| s%d) %s)))" % (topmod, step, get_constr_expr(constr_asserts, step)))
else:
- smt.write("(assert (%s_t s%d s%d))" % (topmod, step, step+1))
- smt.write("(assert (%s_a s%d))" % (topmod, step))
+ smt.write("(assert (|%s_t| s%d s%d))" % (topmod, step, step+1))
+ smt.write("(assert (|%s_a| s%d))" % (topmod, step))
+ smt.write("(assert %s)" % get_constr_expr(constr_asserts, step))
if step > num_steps-skip_steps:
- print("%s Skipping induction in step %d.." % (smt.timestamp(), step))
+ print_msg("Skipping induction in step %d.." % (step))
continue
skip_counter += 1
if skip_counter < step_size:
- print("%s Skipping induction in step %d.." % (smt.timestamp(), step))
+ print_msg("Skipping induction in step %d.." % (step))
continue
skip_counter = 0
- print("%s Trying induction in step %d.." % (smt.timestamp(), step))
+ print_msg("Trying induction in step %d.." % (step))
if smt.check_sat() == "sat":
if step == 0:
print("%s Temporal induction failed!" % smt.timestamp())
- if vcdfile is not None:
- write_vcd_model(num_steps+1)
+ print_anyconsts(num_steps)
+ print_failed_asserts(num_steps)
+ write_trace(step, num_steps+1, '%')
+
+ elif dumpall:
+ print_anyconsts(num_steps)
+ print_failed_asserts(num_steps)
+ write_trace(step, num_steps+1, "%d" % step)
else:
print("%s Temporal induction successful." % smt.timestamp())
@@ -164,62 +566,116 @@ if tempind:
break
-else: # not tempind
+else: # not tempind
step = 0
retstatus = True
while step < num_steps:
- smt.write("(declare-fun s%d () %s_s)" % (step, topmod))
- smt.write("(assert (%s_u s%d))" % (topmod, step))
+ smt.write("(declare-fun s%d () |%s_s|)" % (step, topmod))
+ smt.write("(assert (|%s_u| s%d))" % (topmod, step))
+ smt.write("(assert (|%s_h| s%d))" % (topmod, step))
+ smt.write("(assert %s)" % get_constr_expr(constr_assumes, step))
if step == 0:
- smt.write("(assert (%s_i s0))" % (topmod))
+ smt.write("(assert (|%s_i| s0))" % (topmod))
+ smt.write("(assert (|%s_is| s0))" % (topmod))
else:
- smt.write("(assert (%s_t s%d s%d))" % (topmod, step-1, step))
+ smt.write("(assert (|%s_t| s%d s%d))" % (topmod, step-1, step))
+ smt.write("(assert (not (|%s_is| s%d)))" % (topmod, step))
if step < skip_steps:
if assume_skipped is not None and step >= assume_skipped:
- print("%s Skipping step %d (and assuming pass).." % (smt.timestamp(), step))
- smt.write("(assert (%s_a s%d))" % (topmod, step))
+ print_msg("Skipping step %d (and assuming pass).." % (step))
+ smt.write("(assert (|%s_a| s%d))" % (topmod, step))
+ smt.write("(assert %s)" % get_constr_expr(constr_asserts, step))
else:
- print("%s Skipping step %d.." % (smt.timestamp(), step))
+ print_msg("Skipping step %d.." % (step))
step += 1
continue
last_check_step = step
for i in range(1, step_size):
if step+i < num_steps:
- smt.write("(declare-fun s%d () %s_s)" % (step+i, topmod))
- smt.write("(assert (%s_u s%d))" % (topmod, step+i))
- smt.write("(assert (%s_t s%d s%d))" % (topmod, step+i-1, step+i))
+ smt.write("(declare-fun s%d () |%s_s|)" % (step+i, topmod))
+ smt.write("(assert (|%s_u| s%d))" % (topmod, step+i))
+ smt.write("(assert (|%s_h| s%d))" % (topmod, step+i))
+ smt.write("(assert (|%s_t| s%d s%d))" % (topmod, step+i-1, step+i))
+ smt.write("(assert %s)" % get_constr_expr(constr_assumes, step+i))
last_check_step = step+i
- if last_check_step == step:
- print("%s Checking asserts in step %d.." % (smt.timestamp(), step))
- else:
- print("%s Checking asserts in steps %d to %d.." % (smt.timestamp(), step, last_check_step))
- smt.write("(push 1)")
+ if not gentrace:
+ if not final_only:
+ if last_check_step == step:
+ print_msg("Checking asserts in step %d.." % (step))
+ else:
+ print_msg("Checking asserts in steps %d to %d.." % (step, last_check_step))
+ smt.write("(push 1)")
- smt.write("(assert (not (and %s)))" % " ".join(["(%s_a s%d)" % (topmod, i) for i in range(step, last_check_step+1)]))
+ smt.write("(assert (not (and %s)))" % " ".join(["(|%s_a| s%d)" % (topmod, i) for i in range(step, last_check_step+1)] +
+ [get_constr_expr(constr_asserts, i) for i in range(step, last_check_step+1)]))
- if smt.check_sat() == "sat":
- print("%s BMC failed!" % smt.timestamp())
- if vcdfile is not None:
- write_vcd_model(step+step_size)
- retstatus = False
- break
+ if smt.check_sat() == "sat":
+ print("%s BMC failed!" % smt.timestamp())
+ print_anyconsts(step)
+ for i in range(step, last_check_step+1):
+ print_failed_asserts(i)
+ write_trace(0, last_check_step+1, '%')
+ retstatus = False
+ break
+
+ smt.write("(pop 1)")
- else: # unsat
- smt.write("(pop 1)")
for i in range(step, last_check_step+1):
- smt.write("(assert (%s_a s%d))" % (topmod, i))
+ smt.write("(assert (|%s_a| s%d))" % (topmod, i))
+ smt.write("(assert %s)" % get_constr_expr(constr_asserts, i))
+
+ if constr_final_start is not None:
+ for i in range(step, last_check_step+1):
+ if i < constr_final_start:
+ continue
+
+ print_msg("Checking final constraints in step %d.." % (i))
+ smt.write("(push 1)")
+
+ smt.write("(assert %s)" % get_constr_expr(constr_assumes, i, final=True))
+ smt.write("(assert (not %s))" % get_constr_expr(constr_asserts, i, final=True))
+
+ if smt.check_sat() == "sat":
+ print("%s BMC failed!" % smt.timestamp())
+ print_anyconsts(i)
+ print_failed_asserts(i, final=True)
+ write_trace(0, i+1, '%')
+ retstatus = False
+ break
+
+ smt.write("(pop 1)")
+ if not retstatus:
+ break
+
+ else: # gentrace
+ for i in range(step, last_check_step+1):
+ smt.write("(assert (|%s_a| s%d))" % (topmod, i))
+ smt.write("(assert %s)" % get_constr_expr(constr_asserts, i))
+
+ print_msg("Solving for step %d.." % (last_check_step))
+ if smt.check_sat() != "sat":
+ print("%s No solution found!" % smt.timestamp())
+ retstatus = False
+ break
+
+ elif dumpall:
+ print_anyconsts(0)
+ write_trace(0, last_check_step+1, "%d" % step)
step += step_size
+ if gentrace:
+ print_anyconsts(0)
+ write_trace(0, num_steps, '%')
+
smt.write("(exit)")
smt.wait()
-print("%s Status: %s" % (smt.timestamp(), "PASSED" if retstatus else "FAILED (!)"))
+print_msg("Status: %s" % ("PASSED" if retstatus else "FAILED (!)"))
sys.exit(0 if retstatus else 1)
-
diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py
index 6e8bded7..58554572 100644
--- a/backends/smt2/smtio.py
+++ b/backends/smt2/smtio.py
@@ -17,36 +17,59 @@
# OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
#
-import sys
-import subprocess
+import sys, subprocess, re
+from copy import deepcopy
from select import select
from time import time
-class smtio:
- def __init__(self, solver=None, debug_print=None, debug_file=None, timeinfo=None, opts=None):
+
+hex_dict = {
+ "0": "0000", "1": "0001", "2": "0010", "3": "0011",
+ "4": "0100", "5": "0101", "6": "0110", "7": "0111",
+ "8": "1000", "9": "1001", "A": "1010", "B": "1011",
+ "C": "1100", "D": "1101", "E": "1110", "F": "1111",
+ "a": "1010", "b": "1011", "c": "1100", "d": "1101",
+ "e": "1110", "f": "1111"
+}
+
+
+class SmtModInfo:
+ def __init__(self):
+ self.inputs = set()
+ self.outputs = set()
+ self.registers = set()
+ self.memories = dict()
+ self.wires = set()
+ self.wsize = dict()
+ self.cells = dict()
+ self.asserts = dict()
+ self.anyconsts = dict()
+
+
+class SmtIo:
+ def __init__(self, opts=None):
+ self.logic = None
+ self.logic_qf = True
+ self.logic_ax = True
+ self.logic_uf = True
+ self.logic_bv = True
+
if opts is not None:
+ self.logic = opts.logic
self.solver = opts.solver
self.debug_print = opts.debug_print
self.debug_file = opts.debug_file
+ self.dummy_file = opts.dummy_file
self.timeinfo = opts.timeinfo
+ self.unroll = opts.unroll
else:
self.solver = "z3"
self.debug_print = False
self.debug_file = None
+ self.dummy_file = None
self.timeinfo = True
-
- if solver is not None:
- self.solver = solver
-
- if debug_print is not None:
- self.debug_print = debug_print
-
- if debug_file is not None:
- self.debug_file = debug_file
-
- if timeinfo is not None:
- self.timeinfo = timeinfo
+ self.unroll = False
if self.solver == "yices":
popen_vargs = ['yices-smt2', '--incremental']
@@ -60,44 +83,265 @@ class smtio:
if self.solver == "mathsat":
popen_vargs = ['mathsat']
- self.p = subprocess.Popen(popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT)
+ if self.solver == "boolector":
+ popen_vargs = ['boolector', '--smt2', '-i']
+ self.unroll = True
+
+ if self.solver == "dummy":
+ assert self.dummy_file is not None
+ self.dummy_fd = open(self.dummy_file, "r")
+ else:
+ if self.dummy_file is not None:
+ self.dummy_fd = open(self.dummy_file, "w")
+ self.p = subprocess.Popen(popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT)
+
+ if self.unroll:
+ self.logic_uf = False
+ self.unroll_idcnt = 0
+ self.unroll_buffer = ""
+ self.unroll_sorts = set()
+ self.unroll_objs = set()
+ self.unroll_decls = dict()
+ self.unroll_cache = dict()
+ self.unroll_stack = list()
+
self.start_time = time()
- def setup(self, logic="ALL", info=None):
- self.write("(set-logic %s)" % logic)
- if info is not None:
- self.write("(set-info :source |%s|)" % info)
- self.write("(set-info :smt-lib-version 2.5)")
- self.write("(set-info :category \"industrial\")")
+ self.modinfo = dict()
+ self.curmod = None
+ self.topmod = None
+ self.setup_done = False
+
+ def setup(self):
+ assert not self.setup_done
+
+ if self.logic is None:
+ self.logic = ""
+ if self.logic_qf: self.logic += "QF_"
+ if self.logic_ax: self.logic += "A"
+ if self.logic_uf: self.logic += "UF"
+ if self.logic_bv: self.logic += "BV"
+
+ self.setup_done = True
+ self.write("(set-option :produce-models true)")
+ self.write("(set-logic %s)" % self.logic)
def timestamp(self):
secs = int(time() - self.start_time)
return "## %6d %3d:%02d:%02d " % (secs, secs // (60*60), (secs // 60) % 60, secs % 60)
- def write(self, stmt):
+ def replace_in_stmt(self, stmt, pat, repl):
+ if stmt == pat:
+ return repl
+
+ if isinstance(stmt, list):
+ return [self.replace_in_stmt(s, pat, repl) for s in stmt]
+
+ return stmt
+
+ def unroll_stmt(self, stmt):
+ if not isinstance(stmt, list):
+ return stmt
+
+ stmt = [self.unroll_stmt(s) for s in stmt]
+
+ if len(stmt) >= 2 and not isinstance(stmt[0], list) and stmt[0] in self.unroll_decls:
+ assert stmt[1] in self.unroll_objs
+
+ key = tuple(stmt)
+ if key not in self.unroll_cache:
+ decl = deepcopy(self.unroll_decls[key[0]])
+
+ self.unroll_cache[key] = "|UNROLL#%d|" % self.unroll_idcnt
+ decl[1] = self.unroll_cache[key]
+ self.unroll_idcnt += 1
+
+ if decl[0] == "declare-fun":
+ if isinstance(decl[3], list) or decl[3] not in self.unroll_sorts:
+ self.unroll_objs.add(decl[1])
+ decl[2] = list()
+ else:
+ self.unroll_objs.add(decl[1])
+ decl = list()
+
+ elif decl[0] == "define-fun":
+ arg_index = 1
+ for arg_name, arg_sort in decl[2]:
+ decl[4] = self.replace_in_stmt(decl[4], arg_name, key[arg_index])
+ arg_index += 1
+ decl[2] = list()
+
+ if len(decl) > 0:
+ decl = self.unroll_stmt(decl)
+ self.write(self.unparse(decl), unroll=False)
+
+ return self.unroll_cache[key]
+
+ return stmt
+
+ def write(self, stmt, unroll=True):
+ if stmt.startswith(";"):
+ self.info(stmt)
+ elif not self.setup_done:
+ self.setup()
+
stmt = stmt.strip()
+
+ if unroll and self.unroll:
+ if stmt.startswith(";"):
+ return
+
+ stmt = re.sub(r" ;.*", "", stmt)
+ stmt = self.unroll_buffer + stmt
+ self.unroll_buffer = ""
+
+ s = re.sub(r"\|[^|]*\|", "", stmt)
+ if s.count("(") != s.count(")"):
+ self.unroll_buffer = stmt + " "
+ return
+
+ s = self.parse(stmt)
+
+ if self.debug_print:
+ print("-> %s" % s)
+
+ if len(s) == 3 and s[0] == "declare-sort" and s[2] == "0":
+ self.unroll_sorts.add(s[1])
+ return
+
+ elif len(s) == 4 and s[0] == "declare-fun" and s[2] == [] and s[3] in self.unroll_sorts:
+ self.unroll_objs.add(s[1])
+ return
+
+ elif len(s) >= 4 and s[0] == "declare-fun":
+ for arg_sort in s[2]:
+ if arg_sort in self.unroll_sorts:
+ self.unroll_decls[s[1]] = s
+ return
+
+ elif len(s) >= 4 and s[0] == "define-fun":
+ for arg_name, arg_sort in s[2]:
+ if arg_sort in self.unroll_sorts:
+ self.unroll_decls[s[1]] = s
+ return
+
+ stmt = self.unparse(self.unroll_stmt(s))
+
+ if stmt == "(push 1)":
+ self.unroll_stack.append((
+ deepcopy(self.unroll_sorts),
+ deepcopy(self.unroll_objs),
+ deepcopy(self.unroll_decls),
+ deepcopy(self.unroll_cache),
+ ))
+
+ if stmt == "(pop 1)":
+ self.unroll_sorts, self.unroll_objs, self.unroll_decls, self.unroll_cache = self.unroll_stack.pop()
+
if self.debug_print:
print("> %s" % stmt)
+
if self.debug_file:
print(stmt, file=self.debug_file)
self.debug_file.flush()
- self.p.stdin.write(bytes(stmt + "\n", "ascii"))
- self.p.stdin.flush()
+
+ if self.solver != "dummy":
+ self.p.stdin.write(bytes(stmt + "\n", "ascii"))
+ self.p.stdin.flush()
+
+ def info(self, stmt):
+ if not stmt.startswith("; yosys-smt2-"):
+ return
+
+ fields = stmt.split()
+
+ if fields[1] == "yosys-smt2-nomem":
+ if self.logic is None:
+ self.logic_ax = False
+
+ if fields[1] == "yosys-smt2-nobv":
+ if self.logic is None:
+ self.logic_bv = False
+
+ if fields[1] == "yosys-smt2-module":
+ self.curmod = fields[2]
+ self.modinfo[self.curmod] = SmtModInfo()
+
+ if fields[1] == "yosys-smt2-cell":
+ self.modinfo[self.curmod].cells[fields[3]] = fields[2]
+
+ if fields[1] == "yosys-smt2-topmod":
+ self.topmod = fields[2]
+
+ if fields[1] == "yosys-smt2-input":
+ self.modinfo[self.curmod].inputs.add(fields[2])
+ self.modinfo[self.curmod].wsize[fields[2]] = int(fields[3])
+
+ if fields[1] == "yosys-smt2-output":
+ self.modinfo[self.curmod].outputs.add(fields[2])
+ self.modinfo[self.curmod].wsize[fields[2]] = int(fields[3])
+
+ if fields[1] == "yosys-smt2-register":
+ self.modinfo[self.curmod].registers.add(fields[2])
+ self.modinfo[self.curmod].wsize[fields[2]] = int(fields[3])
+
+ if fields[1] == "yosys-smt2-memory":
+ self.modinfo[self.curmod].memories[fields[2]] = (int(fields[3]), int(fields[4]), int(fields[5]))
+
+ if fields[1] == "yosys-smt2-wire":
+ self.modinfo[self.curmod].wires.add(fields[2])
+ self.modinfo[self.curmod].wsize[fields[2]] = int(fields[3])
+
+ if fields[1] == "yosys-smt2-assert":
+ self.modinfo[self.curmod].asserts[fields[2]] = fields[3]
+
+ if fields[1] == "yosys-smt2-anyconst":
+ self.modinfo[self.curmod].anyconsts[fields[2]] = fields[3]
+
+ def hiernets(self, top, regs_only=False):
+ def hiernets_worker(nets, mod, cursor):
+ for netname in sorted(self.modinfo[mod].wsize.keys()):
+ if not regs_only or netname in self.modinfo[mod].registers:
+ nets.append(cursor + [netname])
+ for cellname, celltype in sorted(self.modinfo[mod].cells.items()):
+ hiernets_worker(nets, celltype, cursor + [cellname])
+
+ nets = list()
+ hiernets_worker(nets, top, [])
+ return nets
+
+ def hiermems(self, top):
+ def hiermems_worker(mems, mod, cursor):
+ for memname in sorted(self.modinfo[mod].memories.keys()):
+ mems.append(cursor + [memname])
+ for cellname, celltype in sorted(self.modinfo[mod].cells.items()):
+ hiermems_worker(mems, celltype, cursor + [cellname])
+
+ mems = list()
+ hiermems_worker(mems, top, [])
+ return mems
def read(self):
stmt = []
count_brackets = 0
while True:
- line = self.p.stdout.readline().decode("ascii").strip()
+ if self.solver == "dummy":
+ line = self.dummy_fd.readline().strip()
+ else:
+ line = self.p.stdout.readline().decode("ascii").strip()
+ if self.dummy_file is not None:
+ self.dummy_fd.write(line + "\n")
+
count_brackets += line.count("(")
count_brackets -= line.count(")")
stmt.append(line)
+
if self.debug_print:
print("< %s" % line)
if count_brackets == 0:
break
- if not self.p.poll():
+ if self.solver != "dummy" and self.p.poll():
print("SMT Solver terminated unexpectedly: %s" % "".join(stmt))
sys.exit(1)
@@ -115,43 +359,44 @@ class smtio:
print("; running check-sat..", file=self.debug_file)
self.debug_file.flush()
- self.p.stdin.write(bytes("(check-sat)\n", "ascii"))
- self.p.stdin.flush()
+ if self.solver != "dummy":
+ self.p.stdin.write(bytes("(check-sat)\n", "ascii"))
+ self.p.stdin.flush()
- if self.timeinfo:
- i = 0
- s = "/-\|"
+ if self.timeinfo:
+ i = 0
+ s = "/-\|"
- count = 0
- num_bs = 0
- while select([self.p.stdout], [], [], 0.1) == ([], [], []):
- count += 1
+ count = 0
+ num_bs = 0
+ while select([self.p.stdout], [], [], 0.1) == ([], [], []):
+ count += 1
- if count < 25:
- continue
+ if count < 25:
+ continue
- if count % 10 == 0 or count == 25:
- secs = count // 10
+ if count % 10 == 0 or count == 25:
+ secs = count // 10
- if secs < 60:
- m = "(%d seconds)" % secs
- elif secs < 60*60:
- m = "(%d seconds -- %d:%02d)" % (secs, secs // 60, secs % 60)
- else:
- m = "(%d seconds -- %d:%02d:%02d)" % (secs, secs // (60*60), (secs // 60) % 60, secs % 60)
+ if secs < 60:
+ m = "(%d seconds)" % secs
+ elif secs < 60*60:
+ m = "(%d seconds -- %d:%02d)" % (secs, secs // 60, secs % 60)
+ else:
+ m = "(%d seconds -- %d:%02d:%02d)" % (secs, secs // (60*60), (secs // 60) % 60, secs % 60)
- print("%s %s %c" % ("\b \b" * num_bs, m, s[i]), end="", file=sys.stderr)
- num_bs = len(m) + 3
+ print("%s %s %c" % ("\b \b" * num_bs, m, s[i]), end="", file=sys.stderr)
+ num_bs = len(m) + 3
- else:
- print("\b" + s[i], end="", file=sys.stderr)
+ else:
+ print("\b" + s[i], end="", file=sys.stderr)
- sys.stderr.flush()
- i = (i + 1) % len(s)
+ sys.stderr.flush()
+ i = (i + 1) % len(s)
- if num_bs != 0:
- print("\b \b" * num_bs, end="", file=sys.stderr)
- sys.stderr.flush()
+ if num_bs != 0:
+ print("\b \b" * num_bs, end="", file=sys.stderr)
+ sys.stderr.flush()
result = self.read()
if self.debug_file:
@@ -192,9 +437,14 @@ class smtio:
return expr, cursor
return worker(stmt)[0]
+ def unparse(self, stmt):
+ if isinstance(stmt, list):
+ return "(" + " ".join([self.unparse(s) for s in stmt]) + ")"
+ return stmt
+
def bv2hex(self, v):
h = ""
- v = bv2bin(v)
+ v = self.bv2bin(v)
while len(v) > 0:
d = 0
if len(v) > 0 and v[-1] == "1": d += 1
@@ -212,66 +462,130 @@ class smtio:
if v.startswith("#b"):
return v[2:]
if v.startswith("#x"):
- digits = []
- for d in v[2:]:
- if d == "0": digits.append("0000")
- if d == "1": digits.append("0001")
- if d == "2": digits.append("0010")
- if d == "3": digits.append("0011")
- if d == "4": digits.append("0100")
- if d == "5": digits.append("0101")
- if d == "6": digits.append("0110")
- if d == "7": digits.append("0111")
- if d == "8": digits.append("1000")
- if d == "9": digits.append("1001")
- if d in ("a", "A"): digits.append("1010")
- if d in ("b", "B"): digits.append("1011")
- if d in ("c", "C"): digits.append("1100")
- if d in ("d", "D"): digits.append("1101")
- if d in ("e", "E"): digits.append("1110")
- if d in ("f", "F"): digits.append("1111")
- return "".join(digits)
+ return "".join(hex_dict.get(x) for x in v[2:])
assert False
+ def bv2int(self, v):
+ return int(self.bv2bin(v), 2)
+
def get(self, expr):
self.write("(get-value (%s))" % (expr))
return self.parse(self.read())[0][1]
- def get_net(self, mod_name, net_name, state_name):
- return self.get("(|%s_n %s| %s)" % (mod_name, net_name, state_name))
+ def get_list(self, expr_list):
+ if len(expr_list) == 0:
+ return []
+ self.write("(get-value (%s))" % " ".join(expr_list))
+ return [n[1] for n in self.parse(self.read())]
+
+ def get_path(self, mod, path):
+ assert mod in self.modinfo
+ path = path.split(".")
+
+ for i in range(len(path)-1):
+ first = ".".join(path[0:i+1])
+ second = ".".join(path[i+1:])
+
+ if first in self.modinfo[mod].cells:
+ nextmod = self.modinfo[mod].cells[first]
+ return [first] + self.get_path(nextmod, second)
+
+ return [".".join(path)]
+
+ def net_expr(self, mod, base, path):
+ if len(path) == 1:
+ assert mod in self.modinfo
+ if path[0] in self.modinfo[mod].wsize:
+ return "(|%s_n %s| %s)" % (mod, path[0], base)
+ if path[0] in self.modinfo[mod].memories:
+ return "(|%s_m %s| %s)" % (mod, path[0], base)
+ assert 0
+
+ assert mod in self.modinfo
+ assert path[0] in self.modinfo[mod].cells
+
+ nextmod = self.modinfo[mod].cells[path[0]]
+ nextbase = "(|%s_h %s| %s)" % (mod, path[0], base)
+ return self.net_expr(nextmod, nextbase, path[1:])
+
+ def net_width(self, mod, net_path):
+ for i in range(len(net_path)-1):
+ assert mod in self.modinfo
+ assert net_path[i] in self.modinfo[mod].cells
+ mod = self.modinfo[mod].cells[net_path[i]]
- def get_net_bool(self, mod_name, net_name, state_name):
- v = self.get_net(mod_name, net_name, state_name)
- assert v in ["true", "false"]
- return 1 if v == "true" else 0
+ assert mod in self.modinfo
+ assert net_path[-1] in self.modinfo[mod].wsize
+ return self.modinfo[mod].wsize[net_path[-1]]
- def get_net_hex(self, mod_name, net_name, state_name):
- return self.bv2hex(self.get_net(mod_name, net_name, state_name))
+ def mem_expr(self, mod, base, path, portidx=None, infomode=False):
+ if len(path) == 1:
+ assert mod in self.modinfo
+ assert path[0] in self.modinfo[mod].memories
+ if infomode:
+ return self.modinfo[mod].memories[path[0]]
+ return "(|%s_m%s %s| %s)" % (mod, "" if portidx is None else ":%d" % portidx, path[0], base)
- def get_net_bin(self, mod_name, net_name, state_name):
- return self.bv2bin(self.get_net(mod_name, net_name, state_name))
+ assert mod in self.modinfo
+ assert path[0] in self.modinfo[mod].cells
+
+ nextmod = self.modinfo[mod].cells[path[0]]
+ nextbase = "(|%s_h %s| %s)" % (mod, path[0], base)
+ return self.mem_expr(nextmod, nextbase, path[1:], portidx=portidx, infomode=infomode)
+
+ def mem_info(self, mod, base, path):
+ return self.mem_expr(mod, base, path, infomode=True)
+
+ def get_net(self, mod_name, net_path, state_name):
+ return self.get(self.net_expr(mod_name, state_name, net_path))
+
+ def get_net_list(self, mod_name, net_path_list, state_name):
+ return self.get_list([self.net_expr(mod_name, state_name, n) for n in net_path_list])
+
+ def get_net_hex(self, mod_name, net_path, state_name):
+ return self.bv2hex(self.get_net(mod_name, net_path, state_name))
+
+ def get_net_hex_list(self, mod_name, net_path_list, state_name):
+ return [self.bv2hex(v) for v in self.get_net_list(mod_name, net_path_list, state_name)]
+
+ def get_net_bin(self, mod_name, net_path, state_name):
+ return self.bv2bin(self.get_net(mod_name, net_path, state_name))
+
+ def get_net_bin_list(self, mod_name, net_path_list, state_name):
+ return [self.bv2bin(v) for v in self.get_net_list(mod_name, net_path_list, state_name)]
def wait(self):
- self.p.wait()
+ if self.solver != "dummy":
+ self.p.wait()
-class smtopts:
+class SmtOpts:
def __init__(self):
- self.optstr = "s:d:vp"
+ self.shortopts = "s:v"
+ self.longopts = ["unroll", "no-progress", "dump-smt2=", "logic=", "dummy="]
self.solver = "z3"
self.debug_print = False
self.debug_file = None
+ self.dummy_file = None
+ self.unroll = False
self.timeinfo = True
+ self.logic = None
def handle(self, o, a):
if o == "-s":
self.solver = a
elif o == "-v":
self.debug_print = True
- elif o == "-p":
+ elif o == "--unroll":
+ self.unroll = True
+ elif o == "--no-progress":
self.timeinfo = True
- elif o == "-d":
+ elif o == "--dump-smt2":
self.debug_file = open(a, "w")
+ elif o == "--logic":
+ self.logic = a
+ elif o == "--dummy":
+ self.dummy_file = a
else:
return False
return True
@@ -279,47 +593,70 @@ class smtopts:
def helpmsg(self):
return """
-s <solver>
- set SMT solver: z3, cvc4, yices, mathsat
+ set SMT solver: z3, cvc4, yices, mathsat, boolector, dummy
default: z3
+ --logic <smt2_logic>
+ use the specified SMT2 logic (e.g. QF_AUFBV)
+
+ --dummy <filename>
+ if solver is "dummy", read solver output from that file
+ otherwise: write solver output to that file
+
-v
enable debug output
- -p
+ --unroll
+ unroll uninterpreted functions
+
+ --no-progress
disable timer display during solving
- -d <filename>
+ --dump-smt2 <filename>
write smt2 statements to file
"""
-class mkvcd:
+class MkVcd:
def __init__(self, f):
self.f = f
self.t = -1
self.nets = dict()
- def add_net(self, name, width):
+ def add_net(self, path, width):
+ path = tuple(path)
assert self.t == -1
key = "n%d" % len(self.nets)
- self.nets[name] = (key, width)
+ self.nets[path] = (key, width)
- def set_net(self, name, bits):
- assert name in self.nets
+ def set_net(self, path, bits):
+ path = tuple(path)
assert self.t >= 0
- print("b%s %s" % (bits, self.nets[name][0]), file=self.f)
+ assert path in self.nets
+ print("b%s %s" % (bits, self.nets[path][0]), file=self.f)
def set_time(self, t):
assert t >= self.t
if t != self.t:
if self.t == -1:
+ print("$var integer 32 t smt_step $end", file=self.f)
print("$var event 1 ! smt_clock $end", file=self.f)
- for name in sorted(self.nets):
- key, width = self.nets[name]
- print("$var wire %d %s %s $end" % (width, key, name), file=self.f)
+ scope = []
+ for path in sorted(self.nets):
+ while len(scope)+1 > len(path) or (len(scope) > 0 and scope[-1] != path[len(scope)-1]):
+ print("$upscope $end", file=self.f)
+ scope = scope[:-1]
+ while len(scope)+1 < len(path):
+ print("$scope module %s $end" % path[len(scope)], file=self.f)
+ scope.append(path[len(scope)-1])
+ key, width = self.nets[path]
+ print("$var wire %d %s %s $end" % (width, key, path[-1]), file=self.f)
+ for i in range(len(scope)):
+ print("$upscope $end", file=self.f)
print("$enddefinitions $end", file=self.f)
self.t = t
assert self.t >= 0
- print("#%d" % self.t, file=self.f)
+ print("#%d" % (10 * self.t), file=self.f)
print("1!", file=self.f)
+ print("b%s t" % format(self.t, "032b"), file=self.f)
diff --git a/backends/smv/smv.cc b/backends/smv/smv.cc
index b29a88ac..162ce490 100644
--- a/backends/smv/smv.cc
+++ b/backends/smv/smv.cc
@@ -694,7 +694,7 @@ struct SmvBackend : public Backend {
std::ifstream template_f;
bool verbose = false;
- log_header("Executing SMV backend.\n");
+ log_header(design, "Executing SMV backend.\n");
size_t argidx;
for (argidx = 1; argidx < args.size(); argidx++)
diff --git a/backends/spice/spice.cc b/backends/spice/spice.cc
index 12e2c669..4101cbf9 100644
--- a/backends/spice/spice.cc
+++ b/backends/spice/spice.cc
@@ -27,13 +27,33 @@
USING_YOSYS_NAMESPACE
PRIVATE_NAMESPACE_BEGIN
-static void print_spice_net(std::ostream &f, RTLIL::SigBit s, std::string &neg, std::string &pos, std::string &ncpf, int &nc_counter)
+static string spice_id2str(IdString id)
+{
+ static const char *escape_chars = "$\\[]()<>=";
+ string s = RTLIL::unescape_id(id);
+
+ for (auto &ch : s)
+ if (strchr(escape_chars, ch) != nullptr) ch = '_';
+
+ return s;
+}
+
+static string spice_id2str(IdString id, bool use_inames, idict<IdString, 1> &inums)
+{
+ if (!use_inames && *id.c_str() == '$')
+ return stringf("%d", inums(id));
+ return spice_id2str(id);
+}
+
+static void print_spice_net(std::ostream &f, RTLIL::SigBit s, std::string &neg, std::string &pos, std::string &ncpf, int &nc_counter, bool use_inames, idict<IdString, 1> &inums)
{
if (s.wire) {
+ if (s.wire->port_id)
+ use_inames = true;
if (s.wire->width > 1)
- f << stringf(" %s[%d]", RTLIL::id2cstr(s.wire->name), s.offset);
+ f << stringf(" %s.%d", spice_id2str(s.wire->name, use_inames, inums).c_str(), s.offset);
else
- f << stringf(" %s", RTLIL::id2cstr(s.wire->name));
+ f << stringf(" %s", spice_id2str(s.wire->name, use_inames, inums).c_str());
} else {
if (s == RTLIL::State::S0)
f << stringf(" %s", neg.c_str());
@@ -44,9 +64,10 @@ static void print_spice_net(std::ostream &f, RTLIL::SigBit s, std::string &neg,
}
}
-static void print_spice_module(std::ostream &f, RTLIL::Module *module, RTLIL::Design *design, std::string &neg, std::string &pos, std::string &ncpf, bool big_endian)
+static void print_spice_module(std::ostream &f, RTLIL::Module *module, RTLIL::Design *design, std::string &neg, std::string &pos, std::string &ncpf, bool big_endian, bool use_inames)
{
SigMap sigmap(module);
+ idict<IdString, 1> inums;
int cell_counter = 0, conn_counter = 0, nc_counter = 0;
for (auto &cell_it : module->cells_)
@@ -59,7 +80,7 @@ static void print_spice_module(std::ostream &f, RTLIL::Module *module, RTLIL::De
if (design->modules_.count(cell->type) == 0)
{
log_warning("no (blackbox) module for cell type `%s' (%s.%s) found! Guessing order of ports.\n",
- RTLIL::id2cstr(cell->type), RTLIL::id2cstr(module->name), RTLIL::id2cstr(cell->name));
+ log_id(cell->type), log_id(module), log_id(cell));
for (auto &conn : cell->connections()) {
RTLIL::SigSpec sig = sigmap(conn.second);
port_sigs.push_back(sig);
@@ -93,18 +114,18 @@ static void print_spice_module(std::ostream &f, RTLIL::Module *module, RTLIL::De
for (auto &sig : port_sigs) {
for (int i = 0; i < sig.size(); i++) {
RTLIL::SigSpec s = sig.extract(big_endian ? sig.size() - 1 - i : i, 1);
- print_spice_net(f, s, neg, pos, ncpf, nc_counter);
+ print_spice_net(f, s, neg, pos, ncpf, nc_counter, use_inames, inums);
}
}
- f << stringf(" %s\n", RTLIL::id2cstr(cell->type));
+ f << stringf(" %s\n", spice_id2str(cell->type).c_str());
}
for (auto &conn : module->connections())
for (int i = 0; i < conn.first.size(); i++) {
f << stringf("V%d", conn_counter++);
- print_spice_net(f, conn.first.extract(i, 1), neg, pos, ncpf, nc_counter);
- print_spice_net(f, conn.second.extract(i, 1), neg, pos, ncpf, nc_counter);
+ print_spice_net(f, conn.first.extract(i, 1), neg, pos, ncpf, nc_counter, use_inames, inums);
+ print_spice_net(f, conn.second.extract(i, 1), neg, pos, ncpf, nc_counter, use_inames, inums);
f << stringf(" DC 0\n");
}
}
@@ -132,6 +153,10 @@ struct SpiceBackend : public Backend {
log(" -nc_prefix\n");
log(" prefix for not-connected nets (default: _NC)\n");
log("\n");
+ log(" -inames\n");
+ log(" include names of internal ($-prefixed) nets in outputs\n");
+ log(" (default is to use net numbers instead)\n");
+ log("\n");
log(" -top top_module\n");
log(" set the specified module as design top module\n");
log("\n");
@@ -140,10 +165,10 @@ struct SpiceBackend : public Backend {
{
std::string top_module_name;
RTLIL::Module *top_module = NULL;
- bool big_endian = false;
+ bool big_endian = false, use_inames = false;
std::string neg = "Vss", pos = "Vdd", ncpf = "_NC";
- log_header("Executing SPICE backend.\n");
+ log_header(design, "Executing SPICE backend.\n");
size_t argidx;
for (argidx = 1; argidx < args.size(); argidx++)
@@ -152,6 +177,10 @@ struct SpiceBackend : public Backend {
big_endian = true;
continue;
}
+ if (args[argidx] == "-inames") {
+ use_inames = true;
+ continue;
+ }
if (args[argidx] == "-neg" && argidx+1 < args.size()) {
neg = args[++argidx];
continue;
@@ -187,9 +216,9 @@ struct SpiceBackend : public Backend {
continue;
if (module->processes.size() != 0)
- log_error("Found unmapped processes in module %s: unmapped processes are not supported in SPICE backend!\n", RTLIL::id2cstr(module->name));
+ log_error("Found unmapped processes in module %s: unmapped processes are not supported in SPICE backend!\n", log_id(module));
if (module->memories.size() != 0)
- log_error("Found munmapped emories in module %s: unmapped memories are not supported in SPICE backend!\n", RTLIL::id2cstr(module->name));
+ log_error("Found unmapped memories in module %s: unmapped memories are not supported in SPICE backend!\n", log_id(module));
if (module->name == RTLIL::escape_id(top_module_name)) {
top_module = module;
@@ -206,24 +235,24 @@ struct SpiceBackend : public Backend {
ports.at(wire->port_id-1) = wire;
}
- *f << stringf(".SUBCKT %s", RTLIL::id2cstr(module->name));
+ *f << stringf(".SUBCKT %s", spice_id2str(module->name).c_str());
for (RTLIL::Wire *wire : ports) {
log_assert(wire != NULL);
if (wire->width > 1) {
for (int i = 0; i < wire->width; i++)
- *f << stringf(" %s[%d]", RTLIL::id2cstr(wire->name), big_endian ? wire->width - 1 - i : i);
+ *f << stringf(" %s.%d", spice_id2str(wire->name).c_str(), big_endian ? wire->width - 1 - i : i);
} else
- *f << stringf(" %s", RTLIL::id2cstr(wire->name));
+ *f << stringf(" %s", spice_id2str(wire->name).c_str());
}
*f << stringf("\n");
- print_spice_module(*f, module, design, neg, pos, ncpf, big_endian);
- *f << stringf(".ENDS %s\n\n", RTLIL::id2cstr(module->name));
+ print_spice_module(*f, module, design, neg, pos, ncpf, big_endian, use_inames);
+ *f << stringf(".ENDS %s\n\n", spice_id2str(module->name).c_str());
}
if (!top_module_name.empty()) {
if (top_module == NULL)
log_error("Can't find top module `%s'!\n", top_module_name.c_str());
- print_spice_module(*f, top_module, design, neg, pos, ncpf, big_endian);
+ print_spice_module(*f, top_module, design, neg, pos, ncpf, big_endian, use_inames);
*f << stringf("\n");
}
diff --git a/backends/verilog/verilog_backend.cc b/backends/verilog/verilog_backend.cc
index 10f10e3c..52cf861d 100644
--- a/backends/verilog/verilog_backend.cc
+++ b/backends/verilog/verilog_backend.cc
@@ -19,11 +19,6 @@
*
* A simple and straightforward Verilog backend.
*
- * Note that RTLIL processes can't always be mapped easily to a Verilog
- * process. Therefore this frontend should only be used to export a
- * Verilog netlist (i.e. after the "proc" pass has converted all processes
- * to logic networks and registers).
- *
*/
#include "kernel/register.h"
@@ -38,7 +33,7 @@
USING_YOSYS_NAMESPACE
PRIVATE_NAMESPACE_BEGIN
-bool norename, noattr, attr2comment, noexpr;
+bool norename, noattr, attr2comment, noexpr, nodec, nostr, defparam;
int auto_name_counter, auto_name_offset, auto_name_digits;
std::map<RTLIL::IdString, int> auto_name_map;
std::set<RTLIL::IdString> reg_wires, reg_ct;
@@ -146,6 +141,9 @@ bool is_reg_wire(RTLIL::SigSpec sig, std::string &reg_name)
if (sig.size() != chunk.wire->width) {
if (sig.size() == 1)
reg_name += stringf("[%d]", chunk.wire->start_offset + chunk.offset);
+ else if (chunk.wire->upto)
+ reg_name += stringf("[%d:%d]", (chunk.wire->width - (chunk.offset + chunk.width - 1) - 1) + chunk.wire->start_offset,
+ (chunk.wire->width - chunk.offset - 1) + chunk.wire->start_offset);
else
reg_name += stringf("[%d:%d]", chunk.wire->start_offset + chunk.offset + chunk.width - 1,
chunk.wire->start_offset + chunk.offset);
@@ -158,8 +156,10 @@ void dump_const(std::ostream &f, const RTLIL::Const &data, int width = -1, int o
{
if (width < 0)
width = data.bits.size() - offset;
+ if (nostr)
+ goto dump_bits;
if ((data.flags & RTLIL::CONST_FLAG_STRING) == 0 || width != (int)data.bits.size()) {
- if (width == 32 && !no_decimal) {
+ if (width == 32 && !no_decimal && !nodec) {
int32_t val = 0;
for (int i = offset+width-1; i >= offset; i--) {
log_assert(i < (int)data.bits.size());
@@ -169,9 +169,9 @@ void dump_const(std::ostream &f, const RTLIL::Const &data, int width = -1, int o
val |= 1 << (i - offset);
}
if (set_signed && val < 0)
- f << stringf("-32'sd %u", -val);
+ f << stringf("-32'sd%u", -val);
else
- f << stringf("32'%sd %u", set_signed ? "s" : "", val);
+ f << stringf("32'%sd%u", set_signed ? "s" : "", val);
} else {
dump_bits:
f << stringf("%d'%sb", width, set_signed ? "s" : "");
@@ -827,12 +827,13 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
std::vector<std::string> lof_reg_declarations;
int nread_ports = cell->parameters["\\RD_PORTS"].as_int();
- RTLIL::SigSpec sig_rd_clk, sig_rd_data, sig_rd_addr;
+ RTLIL::SigSpec sig_rd_clk, sig_rd_en, sig_rd_data, sig_rd_addr;
bool use_rd_clk, rd_clk_posedge, rd_transparent;
// read ports
for (int i=0; i < nread_ports; i++)
{
sig_rd_clk = cell->getPort("\\RD_CLK").extract(i);
+ sig_rd_en = cell->getPort("\\RD_EN").extract(i);
sig_rd_data = cell->getPort("\\RD_DATA").extract(i*width, width);
sig_rd_addr = cell->getPort("\\RD_ADDR").extract(i*abits, abits);
use_rd_clk = cell->parameters["\\RD_CLK_ENABLE"].extract(i).as_bool();
@@ -850,15 +851,22 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
// for clocked read ports make something like:
// reg [..] temp_id;
// always @(posedge clk)
- // temp_id <= array_reg[r_addr];
+ // if (rd_en) temp_id <= array_reg[r_addr];
// assign r_data = temp_id;
std::string temp_id = next_auto_id();
lof_reg_declarations.push_back( stringf("reg [%d:0] %s;\n", sig_rd_data.size() - 1, temp_id.c_str()) );
{
std::ostringstream os;
+ if (sig_rd_en != RTLIL::SigBit(true))
+ {
+ os << stringf("if (");
+ dump_sigspec(os, sig_rd_en);
+ os << stringf(") ");
+ }
+ os << stringf("%s <= %s[", temp_id.c_str(), mem_id.c_str());
dump_sigspec(os, sig_rd_addr);
- std::string line = stringf("%s <= %s[%s];\n", temp_id.c_str(), mem_id.c_str(), os.str().c_str());
- clk_to_lof_body[clk_domain_str].push_back(line);
+ os << stringf("];\n");
+ clk_to_lof_body[clk_domain_str].push_back(os.str());
}
{
std::ostringstream os;
@@ -900,13 +908,9 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
}
int nwrite_ports = cell->parameters["\\WR_PORTS"].as_int();
- RTLIL::SigSpec sig_wr_clk, sig_wr_data, sig_wr_addr, sig_wr_en, sig_wr_en_bit;
- RTLIL::SigBit last_bit;
+ RTLIL::SigSpec sig_wr_clk, sig_wr_data, sig_wr_addr, sig_wr_en;
bool wr_clk_posedge;
- RTLIL::SigSpec lof_wen;
- dict<RTLIL::SigSpec, int> wen_to_width;
SigMap sigmap(active_module);
- int n, wen_width;
// write ports
for (int i=0; i < nwrite_ports; i++)
{
@@ -914,7 +918,6 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
sig_wr_data = cell->getPort("\\WR_DATA").extract(i*width, width);
sig_wr_addr = cell->getPort("\\WR_ADDR").extract(i*abits, abits);
sig_wr_en = cell->getPort("\\WR_EN").extract(i*width, width);
- sig_wr_en_bit = sig_wr_en.extract(0);
wr_clk_posedge = cell->parameters["\\WR_CLK_POLARITY"].extract(i).as_bool();
{
std::ostringstream os;
@@ -923,48 +926,37 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
if( clk_to_lof_body.count(clk_domain_str) == 0 )
clk_to_lof_body[clk_domain_str] = std::vector<std::string>();
}
- // group the wen bits
- last_bit = sig_wr_en.extract(0);
- lof_wen = RTLIL::SigSpec(last_bit);
- wen_to_width.clear();
- wen_to_width[last_bit] = 0;
- for (auto &current_bit : sig_wr_en.bits())
- {
- if (sigmap(current_bit) == sigmap(last_bit)){
- wen_to_width[current_bit] += 1;
- } else {
- lof_wen.append_bit(current_bit);
- wen_to_width[current_bit] = 1;
- }
- last_bit = current_bit;
- }
// make something like:
// always @(posedge clk)
// if (wr_en_bit) memid[w_addr][??] <= w_data[??];
// ...
- n = 0;
- for (auto &wen_bit : lof_wen) {
- wen_width = wen_to_width[wen_bit];
- if (!(wen_bit == RTLIL::SigBit(false)))
+ for (int i = 0; i < GetSize(sig_wr_en); i++)
+ {
+ int start_i = i, width = 1;
+ SigBit wen_bit = sig_wr_en[i];
+
+ while (i+1 < GetSize(sig_wr_en) && sigmap(sig_wr_en[i+1]) == sigmap(wen_bit))
+ i++, width++;
+
+ if (wen_bit == State::S0)
+ continue;
+
+ std::ostringstream os;
+ if (wen_bit != State::S1)
{
- std::ostringstream os;
- if (!(wen_bit == RTLIL::SigBit(true)))
- {
- os << stringf("if (");
- dump_sigspec(os, wen_bit);
- os << stringf(") ");
- }
- os << stringf("%s[", mem_id.c_str());
- dump_sigspec(os, sig_wr_addr);
- if (wen_width == width)
- os << stringf("] <= ");
- else
- os << stringf("][%d:%d] <= ", n+wen_width-1, n);
- dump_sigspec(os, sig_wr_data.extract(n, wen_width));
- os << stringf(";\n");
- clk_to_lof_body[clk_domain_str].push_back(os.str());
+ os << stringf("if (");
+ dump_sigspec(os, wen_bit);
+ os << stringf(") ");
}
- n += wen_width;
+ os << stringf("%s[", mem_id.c_str());
+ dump_sigspec(os, sig_wr_addr);
+ if (width == GetSize(sig_wr_en))
+ os << stringf("] <= ");
+ else
+ os << stringf("][%d:%d] <= ", i, start_i);
+ dump_sigspec(os, sig_wr_data.extract(start_i, width));
+ os << stringf(";\n");
+ clk_to_lof_body[clk_domain_str].push_back(os.str());
}
}
// Output Verilog that looks something like this:
@@ -1029,7 +1021,7 @@ void dump_cell(std::ostream &f, std::string indent, RTLIL::Cell *cell)
dump_attributes(f, indent, cell->attributes);
f << stringf("%s" "%s", indent.c_str(), id(cell->type, false).c_str());
- if (cell->parameters.size() > 0) {
+ if (!defparam && cell->parameters.size() > 0) {
f << stringf(" #(");
for (auto it = cell->parameters.begin(); it != cell->parameters.end(); ++it) {
if (it != cell->parameters.begin())
@@ -1079,6 +1071,16 @@ void dump_cell(std::ostream &f, std::string indent, RTLIL::Cell *cell)
f << stringf(")");
}
f << stringf("\n%s" ");\n", indent.c_str());
+
+ if (defparam && cell->parameters.size() > 0) {
+ for (auto it = cell->parameters.begin(); it != cell->parameters.end(); ++it) {
+ f << stringf("%sdefparam %s.%s = ", indent.c_str(), cell_name.c_str(), id(it->first).c_str());
+ bool is_signed = (it->second.flags & RTLIL::CONST_FLAG_SIGNED) != 0;
+ dump_const(f, it->second, -1, 0, false, is_signed);
+ f << stringf(";\n");
+ }
+ }
+
}
void dump_conn(std::ostream &f, std::string indent, const RTLIL::SigSpec &left, const RTLIL::SigSpec &right)
@@ -1135,11 +1137,15 @@ void dump_proc_switch(std::ostream &f, std::string indent, RTLIL::SwitchRule *sw
dump_sigspec(f, sw->signal);
f << stringf(")\n");
+ bool got_default = false;
for (auto it = sw->cases.begin(); it != sw->cases.end(); ++it) {
- f << stringf("%s ", indent.c_str());
- if ((*it)->compare.size() == 0)
- f << stringf("default");
- else {
+ if ((*it)->compare.size() == 0) {
+ if (got_default)
+ continue;
+ f << stringf("%s default", indent.c_str());
+ got_default = true;
+ } else {
+ f << stringf("%s ", indent.c_str());
for (size_t i = 0; i < (*it)->compare.size(); i++) {
if (i > 0)
f << stringf(", ");
@@ -1244,6 +1250,12 @@ void dump_module(std::ostream &f, std::string indent, RTLIL::Module *module)
reset_auto_counter(module);
active_module = module;
+ if (!module->processes.empty())
+ log_warning("Module %s contains unmapped RTLIL proccesses. RTLIL processes\n"
+ "can't always be mapped directly to Verilog always blocks. Unintended\n"
+ "changes in simulation behavior are possible! Use \"proc\" to convert\n"
+ "processes to logic networks and registers.", log_id(module));
+
f << stringf("\n");
for (auto it = module->processes.begin(); it != module->processes.end(); ++it)
dump_process(f, indent + " ", it->second, true);
@@ -1340,6 +1352,21 @@ struct VerilogBackend : public Backend {
log(" without this option all internal cells are converted to Verilog\n");
log(" expressions.\n");
log("\n");
+ log(" -nodec\n");
+ log(" 32-bit constant values are by default dumped as decimal numbers,\n");
+ log(" not bit pattern. This option decativates this feature and instead\n");
+ log(" will write out all constants in binary.\n");
+ log("\n");
+ log(" -nostr\n");
+ log(" Parameters and attributes that are specified as strings in the\n");
+ log(" original input will be output as strings by this back-end. This\n");
+ log(" decativates this feature and instead will write string constants\n");
+ log(" as binary numbers.\n");
+ log("\n");
+ log(" -defparam\n");
+ log(" Use 'defparam' statements instead of the Verilog-2001 syntax for\n");
+ log(" cell parameters.\n");
+ log("\n");
log(" -blackboxes\n");
log(" usually modules with the 'blackbox' attribute are ignored. with\n");
log(" this option set only the modules with the 'blackbox' attribute\n");
@@ -1349,15 +1376,24 @@ struct VerilogBackend : public Backend {
log(" only write selected modules. modules must be selected entirely or\n");
log(" not at all.\n");
log("\n");
+ log("Note that RTLIL processes can't always be mapped directly to Verilog\n");
+ log("always blocks. This frontend should only be used to export an RTLIL\n");
+ log("netlist, i.e. after the \"proc\" pass has been used to convert all\n");
+ log("processes to logic networks and registers. A warning is generated when\n");
+ log("this command is called on a design with RTLIL processes.\n");
+ log("\n");
}
virtual void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design)
{
- log_header("Executing Verilog backend.\n");
+ log_header(design, "Executing Verilog backend.\n");
norename = false;
noattr = false;
attr2comment = false;
noexpr = false;
+ nodec = false;
+ nostr = false;
+ defparam = false;
bool blackboxes = false;
bool selected = false;
@@ -1407,6 +1443,18 @@ struct VerilogBackend : public Backend {
noexpr = true;
continue;
}
+ if (arg == "-nodec") {
+ nodec = true;
+ continue;
+ }
+ if (arg == "-nostr") {
+ nostr = true;
+ continue;
+ }
+ if (arg == "-defparam") {
+ defparam = true;
+ continue;
+ }
if (arg == "-blackboxes") {
blackboxes = true;
continue;
generated by cgit v1.2.3 (git 2.25.1) at 2024-04-25 08:25:22 +0000