diff options
Diffstat (limited to 'backends')
-rw-r--r-- | backends/blif/blif.cc | 105 | ||||
-rw-r--r-- | backends/btor/btor.cc | 2 | ||||
-rwxr-xr-x | backends/btor/verilog2btor.sh | 2 | ||||
-rw-r--r-- | backends/edif/edif.cc | 55 | ||||
-rw-r--r-- | backends/ilang/ilang_backend.cc | 2 | ||||
-rw-r--r-- | backends/intersynth/intersynth.cc | 4 | ||||
-rw-r--r-- | backends/json/json.cc | 16 | ||||
-rw-r--r-- | backends/smt2/smt2.cc | 483 | ||||
-rw-r--r-- | backends/smt2/smtbmc.py | 622 | ||||
-rw-r--r-- | backends/smt2/smtio.py | 545 | ||||
-rw-r--r-- | backends/smv/smv.cc | 2 | ||||
-rw-r--r-- | backends/spice/spice.cc | 67 | ||||
-rw-r--r-- | backends/verilog/verilog_backend.cc | 170 |
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> ¶meters) + void write_parameters(const dict<IdString, Const> ¶meters, bool for_module=false) { bool first = true; for (auto ¶m : 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 ®_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 ¤t_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; |