diff options
Diffstat (limited to 'backends')
| -rw-r--r-- | backends/aiger/aiger.cc | 2 | ||||
| -rw-r--r-- | backends/aiger/xaiger.cc | 2 | ||||
| -rw-r--r-- | backends/blif/blif.cc | 110 | ||||
| -rw-r--r-- | backends/btor/.gitignore | 1 | ||||
| -rw-r--r-- | backends/btor/btor.cc | 221 | ||||
| -rwxr-xr-x[-rw-r--r--] | backends/btor/test_cells.sh | 4 | ||||
| -rw-r--r-- | backends/cxxrtl/cxxrtl.h | 24 | ||||
| -rw-r--r-- | backends/cxxrtl/cxxrtl_backend.cc | 153 | ||||
| -rw-r--r-- | backends/cxxrtl/cxxrtl_capi.h | 72 | ||||
| -rw-r--r-- | backends/edif/edif.cc | 8 | ||||
| -rw-r--r-- | backends/ilang/Makefile.inc | 3 | ||||
| -rw-r--r-- | backends/intersynth/intersynth.cc | 4 | ||||
| -rw-r--r-- | backends/rtlil/Makefile.inc | 3 | ||||
| -rw-r--r-- | backends/rtlil/rtlil_backend.cc (renamed from backends/ilang/ilang_backend.cc) | 65 | ||||
| -rw-r--r-- | backends/rtlil/rtlil_backend.h (renamed from backends/ilang/ilang_backend.h) | 8 | ||||
| -rw-r--r-- | backends/smt2/smt2.cc | 465 | ||||
| -rw-r--r-- | backends/smt2/smtbmc.py | 40 | ||||
| -rw-r--r-- | backends/smv/.gitignore | 1 | ||||
| -rw-r--r-- | backends/verilog/verilog_backend.cc | 937 |
19 files changed, 1157 insertions, 966 deletions
diff --git a/backends/aiger/aiger.cc b/backends/aiger/aiger.cc index 81a3f483b..476b30488 100644 --- a/backends/aiger/aiger.cc +++ b/backends/aiger/aiger.cc @@ -111,7 +111,7 @@ struct AigerWriter // promote public wires for (auto wire : module->wires()) - if (wire->name[0] == '\\') + if (wire->name.isPublic()) sigmap.add(wire); // promote input wires diff --git a/backends/aiger/xaiger.cc b/backends/aiger/xaiger.cc index ef0103c17..27499b64a 100644 --- a/backends/aiger/xaiger.cc +++ b/backends/aiger/xaiger.cc @@ -146,7 +146,7 @@ struct XAigerWriter // promote public wires for (auto wire : module->wires()) - if (wire->name[0] == '\\') + if (wire->name.isPublic()) sigmap.add(wire); // promote input wires diff --git a/backends/blif/blif.cc b/backends/blif/blif.cc index 780a16320..088819042 100644 --- a/backends/blif/blif.cc +++ b/backends/blif/blif.cc @@ -86,20 +86,18 @@ struct BlifDumper } } - vector<shared_str> cstr_buf; pool<SigBit> cstr_bits_seen; - const char *cstr(RTLIL::IdString id) + const std::string str(RTLIL::IdString id) { std::string str = RTLIL::unescape_id(id); for (size_t i = 0; i < str.size(); i++) if (str[i] == '#' || str[i] == '=' || str[i] == '<' || str[i] == '>') str[i] = '?'; - cstr_buf.push_back(str); - return cstr_buf.back().c_str(); + return str; } - const char *cstr(RTLIL::SigBit sig) + const std::string str(RTLIL::SigBit sig) { cstr_bits_seen.insert(sig); @@ -117,11 +115,10 @@ struct BlifDumper if (sig.wire->width != 1) str += stringf("[%d]", sig.wire->upto ? sig.wire->start_offset+sig.wire->width-sig.offset-1 : sig.wire->start_offset+sig.offset); - cstr_buf.push_back(str); - return cstr_buf.back().c_str(); + return str; } - const char *cstr_init(RTLIL::SigBit sig) + const std::string str_init(RTLIL::SigBit sig) { sigmap.apply(sig); @@ -130,8 +127,7 @@ struct BlifDumper string str = stringf(" %d", init_bits.at(sig)); - cstr_buf.push_back(str); - return cstr_buf.back().c_str(); + return str; } const char *subckt_or_gate(std::string cell_type) @@ -168,7 +164,7 @@ struct BlifDumper void dump() { f << stringf("\n"); - f << stringf(".model %s\n", cstr(module->name)); + f << stringf(".model %s\n", str(module->name).c_str()); std::map<int, RTLIL::Wire*> inputs, outputs; @@ -183,7 +179,7 @@ struct BlifDumper for (auto &it : inputs) { RTLIL::Wire *wire = it.second; for (int i = 0; i < wire->width; i++) - f << stringf(" %s", cstr(RTLIL::SigSpec(wire, i))); + f << stringf(" %s", str(RTLIL::SigSpec(wire, i)).c_str()); } f << stringf("\n"); @@ -191,7 +187,7 @@ struct BlifDumper for (auto &it : outputs) { RTLIL::Wire *wire = it.second; for (int i = 0; i < wire->width; i++) - f << stringf(" %s", cstr(RTLIL::SigSpec(wire, i))); + f << stringf(" %s", str(RTLIL::SigSpec(wire, i)).c_str()); } f << stringf("\n"); @@ -233,131 +229,131 @@ struct BlifDumper if (config->unbuf_types.count(cell->type)) { auto portnames = config->unbuf_types.at(cell->type); f << stringf(".names %s %s\n1 1\n", - cstr(cell->getPort(portnames.first)), cstr(cell->getPort(portnames.second))); + str(cell->getPort(portnames.first)).c_str(), str(cell->getPort(portnames.second)).c_str()); continue; } if (!config->icells_mode && cell->type == ID($_NOT_)) { f << stringf(".names %s %s\n0 1\n", - cstr(cell->getPort(ID::A)), cstr(cell->getPort(ID::Y))); + str(cell->getPort(ID::A)).c_str(), str(cell->getPort(ID::Y)).c_str()); goto internal_cell; } if (!config->icells_mode && cell->type == ID($_AND_)) { f << stringf(".names %s %s %s\n11 1\n", - cstr(cell->getPort(ID::A)), cstr(cell->getPort(ID::B)), cstr(cell->getPort(ID::Y))); + str(cell->getPort(ID::A)).c_str(), str(cell->getPort(ID::B)).c_str(), str(cell->getPort(ID::Y)).c_str()); goto internal_cell; } if (!config->icells_mode && cell->type == ID($_OR_)) { f << stringf(".names %s %s %s\n1- 1\n-1 1\n", - cstr(cell->getPort(ID::A)), cstr(cell->getPort(ID::B)), cstr(cell->getPort(ID::Y))); + str(cell->getPort(ID::A)).c_str(), str(cell->getPort(ID::B)).c_str(), str(cell->getPort(ID::Y)).c_str()); goto internal_cell; } if (!config->icells_mode && cell->type == ID($_XOR_)) { f << stringf(".names %s %s %s\n10 1\n01 1\n", - cstr(cell->getPort(ID::A)), cstr(cell->getPort(ID::B)), cstr(cell->getPort(ID::Y))); + str(cell->getPort(ID::A)).c_str(), str(cell->getPort(ID::B)).c_str(), str(cell->getPort(ID::Y)).c_str()); goto internal_cell; } if (!config->icells_mode && cell->type == ID($_NAND_)) { f << stringf(".names %s %s %s\n0- 1\n-0 1\n", - cstr(cell->getPort(ID::A)), cstr(cell->getPort(ID::B)), cstr(cell->getPort(ID::Y))); + str(cell->getPort(ID::A)).c_str(), str(cell->getPort(ID::B)).c_str(), str(cell->getPort(ID::Y)).c_str()); goto internal_cell; } if (!config->icells_mode && cell->type == ID($_NOR_)) { f << stringf(".names %s %s %s\n00 1\n", - cstr(cell->getPort(ID::A)), cstr(cell->getPort(ID::B)), cstr(cell->getPort(ID::Y))); + str(cell->getPort(ID::A)).c_str(), str(cell->getPort(ID::B)).c_str(), str(cell->getPort(ID::Y)).c_str()); goto internal_cell; } if (!config->icells_mode && cell->type == ID($_XNOR_)) { f << stringf(".names %s %s %s\n11 1\n00 1\n", - cstr(cell->getPort(ID::A)), cstr(cell->getPort(ID::B)), cstr(cell->getPort(ID::Y))); + str(cell->getPort(ID::A)).c_str(), str(cell->getPort(ID::B)).c_str(), str(cell->getPort(ID::Y)).c_str()); goto internal_cell; } if (!config->icells_mode && cell->type == ID($_ANDNOT_)) { f << stringf(".names %s %s %s\n10 1\n", - cstr(cell->getPort(ID::A)), cstr(cell->getPort(ID::B)), cstr(cell->getPort(ID::Y))); + str(cell->getPort(ID::A)).c_str(), str(cell->getPort(ID::B)).c_str(), str(cell->getPort(ID::Y)).c_str()); goto internal_cell; } if (!config->icells_mode && cell->type == ID($_ORNOT_)) { f << stringf(".names %s %s %s\n1- 1\n-0 1\n", - cstr(cell->getPort(ID::A)), cstr(cell->getPort(ID::B)), cstr(cell->getPort(ID::Y))); + str(cell->getPort(ID::A)).c_str(), str(cell->getPort(ID::B)).c_str(), str(cell->getPort(ID::Y)).c_str()); goto internal_cell; } if (!config->icells_mode && cell->type == ID($_AOI3_)) { f << stringf(".names %s %s %s %s\n-00 1\n0-0 1\n", - cstr(cell->getPort(ID::A)), cstr(cell->getPort(ID::B)), cstr(cell->getPort(ID::C)), cstr(cell->getPort(ID::Y))); + str(cell->getPort(ID::A)).c_str(), str(cell->getPort(ID::B)).c_str(), str(cell->getPort(ID::C)).c_str(), str(cell->getPort(ID::Y)).c_str()); goto internal_cell; } if (!config->icells_mode && cell->type == ID($_OAI3_)) { f << stringf(".names %s %s %s %s\n00- 1\n--0 1\n", - cstr(cell->getPort(ID::A)), cstr(cell->getPort(ID::B)), cstr(cell->getPort(ID::C)), cstr(cell->getPort(ID::Y))); + str(cell->getPort(ID::A)).c_str(), str(cell->getPort(ID::B)).c_str(), str(cell->getPort(ID::C)).c_str(), str(cell->getPort(ID::Y)).c_str()); goto internal_cell; } if (!config->icells_mode && cell->type == ID($_AOI4_)) { f << stringf(".names %s %s %s %s %s\n-0-0 1\n-00- 1\n0--0 1\n0-0- 1\n", - cstr(cell->getPort(ID::A)), cstr(cell->getPort(ID::B)), - cstr(cell->getPort(ID::C)), cstr(cell->getPort(ID::D)), cstr(cell->getPort(ID::Y))); + str(cell->getPort(ID::A)).c_str(), str(cell->getPort(ID::B)).c_str(), + str(cell->getPort(ID::C)).c_str(), str(cell->getPort(ID::D)).c_str(), str(cell->getPort(ID::Y)).c_str()); goto internal_cell; } if (!config->icells_mode && cell->type == ID($_OAI4_)) { f << stringf(".names %s %s %s %s %s\n00-- 1\n--00 1\n", - cstr(cell->getPort(ID::A)), cstr(cell->getPort(ID::B)), - cstr(cell->getPort(ID::C)), cstr(cell->getPort(ID::D)), cstr(cell->getPort(ID::Y))); + str(cell->getPort(ID::A)).c_str(), str(cell->getPort(ID::B)).c_str(), + str(cell->getPort(ID::C)).c_str(), str(cell->getPort(ID::D)).c_str(), str(cell->getPort(ID::Y)).c_str()); goto internal_cell; } if (!config->icells_mode && cell->type == ID($_MUX_)) { f << stringf(".names %s %s %s %s\n1-0 1\n-11 1\n", - cstr(cell->getPort(ID::A)), cstr(cell->getPort(ID::B)), - cstr(cell->getPort(ID::S)), cstr(cell->getPort(ID::Y))); + str(cell->getPort(ID::A)).c_str(), str(cell->getPort(ID::B)).c_str(), + str(cell->getPort(ID::S)).c_str(), str(cell->getPort(ID::Y)).c_str()); goto internal_cell; } if (!config->icells_mode && cell->type == ID($_NMUX_)) { f << stringf(".names %s %s %s %s\n0-0 1\n-01 1\n", - cstr(cell->getPort(ID::A)), cstr(cell->getPort(ID::B)), - cstr(cell->getPort(ID::S)), cstr(cell->getPort(ID::Y))); + str(cell->getPort(ID::A)).c_str(), str(cell->getPort(ID::B)).c_str(), + str(cell->getPort(ID::S)).c_str(), str(cell->getPort(ID::Y)).c_str()); goto internal_cell; } if (!config->icells_mode && cell->type == ID($_FF_)) { - f << stringf(".latch %s %s%s\n", cstr(cell->getPort(ID::D)), cstr(cell->getPort(ID::Q)), - cstr_init(cell->getPort(ID::Q))); + f << stringf(".latch %s %s%s\n", str(cell->getPort(ID::D)).c_str(), str(cell->getPort(ID::Q)).c_str(), + str_init(cell->getPort(ID::Q)).c_str()); goto internal_cell; } if (!config->icells_mode && cell->type == ID($_DFF_N_)) { - f << stringf(".latch %s %s fe %s%s\n", cstr(cell->getPort(ID::D)), cstr(cell->getPort(ID::Q)), - cstr(cell->getPort(ID::C)), cstr_init(cell->getPort(ID::Q))); + f << stringf(".latch %s %s fe %s%s\n", str(cell->getPort(ID::D)).c_str(), str(cell->getPort(ID::Q)).c_str(), + str(cell->getPort(ID::C)).c_str(), str_init(cell->getPort(ID::Q)).c_str()); goto internal_cell; } if (!config->icells_mode && cell->type == ID($_DFF_P_)) { - f << stringf(".latch %s %s re %s%s\n", cstr(cell->getPort(ID::D)), cstr(cell->getPort(ID::Q)), - cstr(cell->getPort(ID::C)), cstr_init(cell->getPort(ID::Q))); + f << stringf(".latch %s %s re %s%s\n", str(cell->getPort(ID::D)).c_str(), str(cell->getPort(ID::Q)).c_str(), + str(cell->getPort(ID::C)).c_str(), str_init(cell->getPort(ID::Q)).c_str()); goto internal_cell; } if (!config->icells_mode && cell->type == ID($_DLATCH_N_)) { - f << stringf(".latch %s %s al %s%s\n", cstr(cell->getPort(ID::D)), cstr(cell->getPort(ID::Q)), - cstr(cell->getPort(ID::E)), cstr_init(cell->getPort(ID::Q))); + f << stringf(".latch %s %s al %s%s\n", str(cell->getPort(ID::D)).c_str(), str(cell->getPort(ID::Q)).c_str(), + str(cell->getPort(ID::E)).c_str(), str_init(cell->getPort(ID::Q)).c_str()); goto internal_cell; } if (!config->icells_mode && cell->type == ID($_DLATCH_P_)) { - f << stringf(".latch %s %s ah %s%s\n", cstr(cell->getPort(ID::D)), cstr(cell->getPort(ID::Q)), - cstr(cell->getPort(ID::E)), cstr_init(cell->getPort(ID::Q))); + f << stringf(".latch %s %s ah %s%s\n", str(cell->getPort(ID::D)).c_str(), str(cell->getPort(ID::Q)).c_str(), + str(cell->getPort(ID::E)).c_str(), str_init(cell->getPort(ID::Q)).c_str()); goto internal_cell; } @@ -367,10 +363,10 @@ struct BlifDumper auto width = cell->parameters.at(ID::WIDTH).as_int(); log_assert(inputs.size() == width); for (int i = width-1; i >= 0; i--) - f << stringf(" %s", cstr(inputs.extract(i, 1))); + f << stringf(" %s", str(inputs.extract(i, 1)).c_str()); auto &output = cell->getPort(ID::Y); log_assert(output.size() == 1); - f << stringf(" %s", cstr(output)); + f << stringf(" %s", str(output).c_str()); f << stringf("\n"); RTLIL::SigSpec mask = cell->parameters.at(ID::LUT); for (int i = 0; i < (1 << width); i++) @@ -393,10 +389,10 @@ struct BlifDumper 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))); + f << stringf(" %s", str(inputs.extract(i, 1)).c_str()); auto &output = cell->getPort(ID::Y); log_assert(output.size() == 1); - f << stringf(" %s", cstr(output)); + f << stringf(" %s", str(output).c_str()); f << stringf("\n"); for (int i = 0; i < depth; i++) { for (int j = 0; j < width; j++) { @@ -411,11 +407,11 @@ struct BlifDumper goto internal_cell; } - f << stringf(".%s %s", subckt_or_gate(cell->type.str()), cstr(cell->type)); + f << stringf(".%s %s", subckt_or_gate(cell->type.str()), str(cell->type).c_str()); for (auto &conn : cell->connections()) { if (conn.second.size() == 1) { - f << stringf(" %s=%s", cstr(conn.first), cstr(conn.second[0])); + f << stringf(" %s=%s", str(conn.first).c_str(), str(conn.second[0]).c_str()); continue; } @@ -424,20 +420,20 @@ struct BlifDumper if (w == nullptr) { for (int i = 0; i < GetSize(conn.second); i++) - f << stringf(" %s[%d]=%s", cstr(conn.first), i, cstr(conn.second[i])); + f << stringf(" %s[%d]=%s", str(conn.first).c_str(), i, str(conn.second[i]).c_str()); } else { for (int i = 0; i < std::min(GetSize(conn.second), GetSize(w)); i++) { SigBit sig(w, i); - f << stringf(" %s[%d]=%s", cstr(conn.first), sig.wire->upto ? + f << stringf(" %s[%d]=%s", str(conn.first).c_str(), sig.wire->upto ? sig.wire->start_offset+sig.wire->width-sig.offset-1 : - sig.wire->start_offset+sig.offset, cstr(conn.second[i])); + sig.wire->start_offset+sig.offset, str(conn.second[i]).c_str()); } } } f << stringf("\n"); if (config->cname_mode) - f << stringf(".cname %s\n", cstr(cell->name)); + f << stringf(".cname %s\n", str(cell->name).c_str()); if (config->attr_mode) dump_params(".attr", cell->attributes); if (config->param_mode) @@ -446,7 +442,7 @@ struct BlifDumper if (0) { internal_cell: if (config->iname_mode) - f << stringf(".cname %s\n", cstr(cell->name)); + f << stringf(".cname %s\n", str(cell->name).c_str()); if (config->iattr_mode) dump_params(".attr", cell->attributes); } @@ -462,12 +458,12 @@ struct BlifDumper continue; if (config->conn_mode) - f << stringf(".conn %s %s\n", cstr(rhs_bit), cstr(lhs_bit)); + f << stringf(".conn %s %s\n", str(rhs_bit).c_str(), str(lhs_bit).c_str()); 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(rhs_bit), config->buf_out.c_str(), cstr(lhs_bit)); + config->buf_in.c_str(), str(rhs_bit).c_str(), config->buf_out.c_str(), str(lhs_bit).c_str()); else - f << stringf(".names %s %s\n1 1\n", cstr(rhs_bit), cstr(lhs_bit)); + f << stringf(".names %s %s\n1 1\n", str(rhs_bit).c_str(), str(lhs_bit).c_str()); } f << stringf(".end\n"); diff --git a/backends/btor/.gitignore b/backends/btor/.gitignore new file mode 100644 index 000000000..d23d492d7 --- /dev/null +++ b/backends/btor/.gitignore @@ -0,0 +1 @@ +/test_cells.tmp/ diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc index e5da6c1e7..639c6f129 100644 --- a/backends/btor/btor.cc +++ b/backends/btor/btor.cc @@ -27,6 +27,7 @@ #include "kernel/sigtools.h" #include "kernel/celltypes.h" #include "kernel/log.h" +#include "kernel/mem.h" #include <string> USING_YOSYS_NAMESPACE @@ -68,12 +69,15 @@ struct BtorWorker // ff inputs that need to be evaluated (<nid>, <ff_cell>) vector<pair<int, Cell*>> ff_todo; + vector<pair<int, Mem*>> mem_todo; pool<Cell*> cell_recursion_guard; vector<int> bad_properties; dict<SigBit, bool> initbits; pool<Wire*> statewires; pool<string> srcsymbols; + vector<Mem> memories; + dict<Cell*, Mem*> mem_cells; string indent, info_filename; vector<string> info_lines; @@ -205,9 +209,8 @@ struct BtorWorker if (cell->type.in(ID($xnor), ID($_XNOR_))) btor_op = "xnor"; log_assert(!btor_op.empty()); - int width = GetSize(cell->getPort(ID::Y)); - width = std::max(width, GetSize(cell->getPort(ID::A))); - width = std::max(width, GetSize(cell->getPort(ID::B))); + int width_ay = std::max(GetSize(cell->getPort(ID::A)), GetSize(cell->getPort(ID::Y))); + int width = std::max(width_ay, GetSize(cell->getPort(ID::B))); bool a_signed = cell->hasParam(ID::A_SIGNED) ? cell->getParam(ID::A_SIGNED).as_bool() : false; bool b_signed = cell->hasParam(ID::B_SIGNED) ? cell->getParam(ID::B_SIGNED).as_bool() : false; @@ -224,11 +227,23 @@ struct BtorWorker int sid = get_bv_sid(width); int nid; + int nid_a; + if (cell->type.in(ID($shl), ID($shr), ID($shift), ID($shiftx)) && a_signed && width_ay < width) { + // sign-extend A up to the width of Y + int nid_a_padded = get_sig_nid(cell->getPort(ID::A), width_ay, a_signed); + + // zero-extend the rest + int zeroes = get_sig_nid(Const(0, width-width_ay)); + nid_a = next_nid++; + btorf("%d concat %d %d %d\n", nid_a, sid, zeroes, nid_a_padded); + } else { + nid_a = get_sig_nid(cell->getPort(ID::A), width, a_signed); + } + + int nid_b = get_sig_nid(cell->getPort(ID::B), width, b_signed); + if (btor_op == "shift") { - int nid_a = get_sig_nid(cell->getPort(ID::A), width, false); - int nid_b = get_sig_nid(cell->getPort(ID::B), width, b_signed); - int nid_r = next_nid++; btorf("%d srl %d %d %d\n", nid_r, sid, nid_a, nid_b); @@ -248,9 +263,6 @@ struct BtorWorker } else { - int nid_a = get_sig_nid(cell->getPort(ID::A), width, a_signed); - int nid_b = get_sig_nid(cell->getPort(ID::B), width, b_signed); - nid = next_nid++; btorf("%d %s %d %d %d%s\n", nid, btor_op.c_str(), sid, nid_a, nid_b, getinfo(cell).c_str()); } @@ -696,49 +708,45 @@ struct BtorWorker goto okay; } - if (cell->type == ID($mem)) + if (cell->type.in(ID($mem), ID($memrd), ID($memwr), ID($meminit))) { - int abits = cell->getParam(ID::ABITS).as_int(); - int width = cell->getParam(ID::WIDTH).as_int(); - int nwords = cell->getParam(ID::SIZE).as_int(); - int rdports = cell->getParam(ID::RD_PORTS).as_int(); - int wrports = cell->getParam(ID::WR_PORTS).as_int(); + Mem *mem = mem_cells[cell]; - Const wr_clk_en = cell->getParam(ID::WR_CLK_ENABLE); - Const rd_clk_en = cell->getParam(ID::RD_CLK_ENABLE); + int abits = ceil_log2(mem->size); - bool asyncwr = wr_clk_en.is_fully_zero(); + bool asyncwr = false; + bool syncwr = false; - if (!asyncwr && !wr_clk_en.is_fully_ones()) - log_error("Memory %s.%s has mixed async/sync write ports.\n", - log_id(module), log_id(cell)); - - if (!rd_clk_en.is_fully_zero()) - log_error("Memory %s.%s has sync read ports.\n", - log_id(module), log_id(cell)); + for (auto &port : mem->wr_ports) { + if (port.clk_enable) + syncwr = true; + else + asyncwr = true; + } - SigSpec sig_rd_addr = sigmap(cell->getPort(ID::RD_ADDR)); - SigSpec sig_rd_data = sigmap(cell->getPort(ID::RD_DATA)); + if (asyncwr && syncwr) + log_error("Memory %s.%s has mixed async/sync write ports.\n", + log_id(module), log_id(mem->memid)); - SigSpec sig_wr_addr = sigmap(cell->getPort(ID::WR_ADDR)); - SigSpec sig_wr_data = sigmap(cell->getPort(ID::WR_DATA)); - SigSpec sig_wr_en = sigmap(cell->getPort(ID::WR_EN)); + for (auto &port : mem->rd_ports) + if (port.clk_enable) + log_error("Memory %s.%s has sync read ports.\n", + log_id(module), log_id(mem->memid)); - int data_sid = get_bv_sid(width); + int data_sid = get_bv_sid(mem->width); int bool_sid = get_bv_sid(1); - int sid = get_mem_sid(abits, width); + int sid = get_mem_sid(abits, mem->width); - Const initdata = cell->getParam(ID::INIT); - initdata.exts(nwords*width); int nid_init_val = -1; - if (!initdata.is_fully_undef()) + if (!mem->inits.empty()) { + Const initdata = mem->get_init_data(); bool constword = true; - Const firstword = initdata.extract(0, width); + Const firstword = initdata.extract(0, mem->width); - for (int i = 1; i < nwords; i++) { - Const thisword = initdata.extract(i*width, width); + for (int i = 1; i < mem->size; i++) { + Const thisword = initdata.extract(i*mem->width, mem->width); if (thisword != firstword) { constword = false; break; @@ -756,8 +764,8 @@ struct BtorWorker nid_init_val = next_nid++; btorf("%d state %d\n", nid_init_val, sid); - for (int i = 0; i < nwords; i++) { - Const thisword = initdata.extract(i*width, width); + for (int i = 0; i < mem->size; i++) { + Const thisword = initdata.extract(i*mem->width, mem->width); if (thisword.is_fully_undef()) continue; Const thisaddr(i, abits); @@ -776,10 +784,10 @@ struct BtorWorker int nid = next_nid++; int nid_head = nid; - if (cell->name[0] == '$') + if (mem->memid[0] == '$') btorf("%d state %d\n", nid, sid); else - btorf("%d state %d %s\n", nid, sid, log_id(cell)); + btorf("%d state %d %s\n", nid, sid, log_id(mem->memid)); if (nid_init_val >= 0) { @@ -789,15 +797,14 @@ struct BtorWorker if (asyncwr) { - for (int port = 0; port < wrports; port++) + for (auto &port : mem->wr_ports) { - SigSpec wa = sig_wr_addr.extract(port*abits, abits); - SigSpec wd = sig_wr_data.extract(port*width, width); - SigSpec we = sig_wr_en.extract(port*width, width); + SigSpec wa = port.addr; + wa.extend_u0(abits); int wa_nid = get_sig_nid(wa); - int wd_nid = get_sig_nid(wd); - int we_nid = get_sig_nid(we); + int wd_nid = get_sig_nid(port.data); + int we_nid = get_sig_nid(port.en); int nid2 = next_nid++; btorf("%d read %d %d %d\n", nid2, data_sid, nid_head, wa_nid); @@ -827,22 +834,22 @@ struct BtorWorker } } - for (int port = 0; port < rdports; port++) + for (auto &port : mem->rd_ports) { - SigSpec ra = sig_rd_addr.extract(port*abits, abits); - SigSpec rd = sig_rd_data.extract(port*width, width); + SigSpec ra = port.addr; + ra.extend_u0(abits); int ra_nid = get_sig_nid(ra); int rd_nid = next_nid++; btorf("%d read %d %d %d\n", rd_nid, data_sid, nid_head, ra_nid); - add_nid_sig(rd_nid, rd); + add_nid_sig(rd_nid, port.data); } if (!asyncwr) { - ff_todo.push_back(make_pair(nid, cell)); + mem_todo.push_back(make_pair(nid, mem)); } else { @@ -1057,6 +1064,15 @@ struct BtorWorker if (!info_filename.empty()) infof("name %s\n", log_id(module)); + memories = Mem::get_all_memories(module); + + dict<IdString, Mem*> mem_dict; + for (auto &mem : memories) + mem_dict[mem.memid] = &mem; + for (auto cell : module->cells()) + if (cell->type.in(ID($mem), ID($memwr), ID($memrd), ID($meminit))) + mem_cells[cell] = mem_dict[cell->parameters.at(ID::MEMID).decode_string()]; + btorf_push("inputs"); for (auto wire : module->wires()) @@ -1193,7 +1209,7 @@ struct BtorWorker continue; } - while (!ff_todo.empty()) + while (!ff_todo.empty() || !mem_todo.empty()) { vector<pair<int, Cell*>> todo; todo.swap(ff_todo); @@ -1205,70 +1221,71 @@ struct BtorWorker btorf_push(stringf("next %s", log_id(cell))); - if (cell->type == ID($mem)) - { - int abits = cell->getParam(ID::ABITS).as_int(); - int width = cell->getParam(ID::WIDTH).as_int(); - int wrports = cell->getParam(ID::WR_PORTS).as_int(); + SigSpec sig = sigmap(cell->getPort(ID::D)); + int nid_q = get_sig_nid(sig); + int sid = get_bv_sid(GetSize(sig)); + btorf("%d next %d %d %d%s\n", next_nid++, sid, nid, nid_q, getinfo(cell).c_str()); - SigSpec sig_wr_addr = sigmap(cell->getPort(ID::WR_ADDR)); - SigSpec sig_wr_data = sigmap(cell->getPort(ID::WR_DATA)); - SigSpec sig_wr_en = sigmap(cell->getPort(ID::WR_EN)); + btorf_pop(stringf("next %s", log_id(cell))); + } - int data_sid = get_bv_sid(width); - int bool_sid = get_bv_sid(1); - int sid = get_mem_sid(abits, width); - int nid_head = nid; + vector<pair<int, Mem*>> mtodo; + mtodo.swap(mem_todo); - for (int port = 0; port < wrports; port++) - { - SigSpec wa = sig_wr_addr.extract(port*abits, abits); - SigSpec wd = sig_wr_data.extract(port*width, width); - SigSpec we = sig_wr_en.extract(port*width, width); + for (auto &it : mtodo) + { + int nid = it.first; + Mem *mem = it.second; + + btorf_push(stringf("next %s", log_id(mem->memid))); + + int abits = ceil_log2(mem->size); - int wa_nid = get_sig_nid(wa); - int wd_nid = get_sig_nid(wd); - int we_nid = get_sig_nid(we); + int data_sid = get_bv_sid(mem->width); + int bool_sid = get_bv_sid(1); + int sid = get_mem_sid(abits, mem->width); + int nid_head = nid; - int nid2 = next_nid++; - btorf("%d read %d %d %d\n", nid2, data_sid, nid_head, wa_nid); + for (auto &port : mem->wr_ports) + { + SigSpec wa = port.addr; + wa.extend_u0(abits); - int nid3 = next_nid++; - btorf("%d not %d %d\n", nid3, data_sid, we_nid); + int wa_nid = get_sig_nid(wa); + int wd_nid = get_sig_nid(port.data); + int we_nid = get_sig_nid(port.en); - int nid4 = next_nid++; - btorf("%d and %d %d %d\n", nid4, data_sid, nid2, nid3); + int nid2 = next_nid++; + btorf("%d read %d %d %d\n", nid2, data_sid, nid_head, wa_nid); + + int nid3 = next_nid++; + btorf("%d not %d %d\n", nid3, data_sid, we_nid); - int nid5 = next_nid++; - btorf("%d and %d %d %d\n", nid5, data_sid, wd_nid, we_nid); + int nid4 = next_nid++; + btorf("%d and %d %d %d\n", nid4, data_sid, nid2, nid3); - int nid6 = next_nid++; - btorf("%d or %d %d %d\n", nid6, data_sid, nid5, nid4); + int nid5 = next_nid++; + btorf("%d and %d %d %d\n", nid5, data_sid, wd_nid, we_nid); - int nid7 = next_nid++; - btorf("%d write %d %d %d %d\n", nid7, sid, nid_head, wa_nid, nid6); + int nid6 = next_nid++; + btorf("%d or %d %d %d\n", nid6, data_sid, nid5, nid4); - int nid8 = next_nid++; - btorf("%d redor %d %d\n", nid8, bool_sid, we_nid); + int nid7 = next_nid++; + btorf("%d write %d %d %d %d\n", nid7, sid, nid_head, wa_nid, nid6); - int nid9 = next_nid++; - btorf("%d ite %d %d %d %d\n", nid9, sid, nid8, nid7, nid_head); + int nid8 = next_nid++; + btorf("%d redor %d %d\n", nid8, bool_sid, we_nid); - nid_head = nid9; - } + int nid9 = next_nid++; + btorf("%d ite %d %d %d %d\n", nid9, sid, nid8, nid7, nid_head); - int nid2 = next_nid++; - btorf("%d next %d %d %d%s\n", nid2, sid, nid, nid_head, getinfo(cell).c_str()); - } - else - { - SigSpec sig = sigmap(cell->getPort(ID::D)); - int nid_q = get_sig_nid(sig); - int sid = get_bv_sid(GetSize(sig)); - btorf("%d next %d %d %d%s\n", next_nid++, sid, nid, nid_q, getinfo(cell).c_str()); + nid_head = nid9; } - btorf_pop(stringf("next %s", log_id(cell))); + int nid2 = next_nid++; + btorf("%d next %d %d %d%s\n", nid2, sid, nid, nid_head, (mem->cell ? getinfo(mem->cell) : getinfo(mem->mem)).c_str()); + + btorf_pop(stringf("next %s", log_id(mem->memid))); } } diff --git a/backends/btor/test_cells.sh b/backends/btor/test_cells.sh index 3f077201a..0a011932d 100644..100755 --- a/backends/btor/test_cells.sh +++ b/backends/btor/test_cells.sh @@ -6,7 +6,7 @@ rm -rf test_cells.tmp mkdir -p test_cells.tmp cd test_cells.tmp -../../../yosys -p 'test_cell -n 5 -w test all /$alu /$fa /$lcu /$lut /$sop /$macc /$mul /$div /$mod /$divfloor /$modfloor' +../../../yosys -p 'test_cell -n 5 -w test all /$alu /$fa /$lcu /$lut /$sop /$macc /$mul /$div /$mod /$divfloor /$modfloor /$shiftx' for fn in test_*.il; do ../../../yosys -p " @@ -19,7 +19,7 @@ for fn in test_*.il; do hierarchy -top main write_btor ${fn%.il}.btor " - boolectormc -kmax 1 --trace-gen --stop-first -v ${fn%.il}.btor > ${fn%.il}.out + btormc -kmax 1 --trace-gen --stop-first -v ${fn%.il}.btor > ${fn%.il}.out if grep " SATISFIABLE" ${fn%.il}.out; then echo "Check failed for ${fn%.il}." exit 1 diff --git a/backends/cxxrtl/cxxrtl.h b/backends/cxxrtl/cxxrtl.h index f0d7b9fc7..41089a153 100644 --- a/backends/cxxrtl/cxxrtl.h +++ b/backends/cxxrtl/cxxrtl.h @@ -452,10 +452,11 @@ struct value : public expr_base<value<Bits>> { bool carry = CarryIn; for (size_t n = 0; n < result.chunks; n++) { result.data[n] = data[n] + (Invert ? ~other.data[n] : other.data[n]) + carry; + if (result.chunks - 1 == n) + result.data[result.chunks - 1] &= result.msb_mask; carry = (result.data[n] < data[n]) || (result.data[n] == data[n] && carry); } - result.data[result.chunks - 1] &= result.msb_mask; return {result, carry}; } @@ -823,6 +824,7 @@ struct debug_alias {}; // To avoid violating strict aliasing rules, this structure has to be a subclass of the one used // in the C API, or it would not be possible to cast between the pointers to these. struct debug_item : ::cxxrtl_object { + // Object types. enum : uint32_t { VALUE = CXXRTL_VALUE, WIRE = CXXRTL_WIRE, @@ -830,13 +832,24 @@ struct debug_item : ::cxxrtl_object { ALIAS = CXXRTL_ALIAS, }; + // Object flags. + enum : uint32_t { + INPUT = CXXRTL_INPUT, + OUTPUT = CXXRTL_OUTPUT, + INOUT = CXXRTL_INOUT, + DRIVEN_SYNC = CXXRTL_DRIVEN_SYNC, + DRIVEN_COMB = CXXRTL_DRIVEN_COMB, + UNDRIVEN = CXXRTL_UNDRIVEN, + }; + debug_item(const ::cxxrtl_object &object) : cxxrtl_object(object) {} template<size_t Bits> - debug_item(value<Bits> &item, size_t lsb_offset = 0) { + debug_item(value<Bits> &item, size_t lsb_offset = 0, uint32_t flags_ = 0) { static_assert(sizeof(item) == value<Bits>::chunks * sizeof(chunk_t), "value<Bits> is not compatible with C layout"); type = VALUE; + flags = flags_; width = Bits; lsb_at = lsb_offset; depth = 1; @@ -850,6 +863,7 @@ struct debug_item : ::cxxrtl_object { static_assert(sizeof(item) == value<Bits>::chunks * sizeof(chunk_t), "value<Bits> is not compatible with C layout"); type = VALUE; + flags = DRIVEN_COMB; width = Bits; lsb_at = lsb_offset; depth = 1; @@ -859,11 +873,12 @@ struct debug_item : ::cxxrtl_object { } template<size_t Bits> - debug_item(wire<Bits> &item, size_t lsb_offset = 0) { + debug_item(wire<Bits> &item, size_t lsb_offset = 0, uint32_t flags_ = 0) { static_assert(sizeof(item.curr) == value<Bits>::chunks * sizeof(chunk_t) && sizeof(item.next) == value<Bits>::chunks * sizeof(chunk_t), "wire<Bits> is not compatible with C layout"); type = WIRE; + flags = flags_; width = Bits; lsb_at = lsb_offset; depth = 1; @@ -877,6 +892,7 @@ struct debug_item : ::cxxrtl_object { static_assert(sizeof(item.data[0]) == value<Width>::chunks * sizeof(chunk_t), "memory<Width> is not compatible with C layout"); type = MEMORY; + flags = 0; width = Width; lsb_at = 0; depth = item.data.size(); @@ -890,6 +906,7 @@ struct debug_item : ::cxxrtl_object { static_assert(sizeof(item) == value<Bits>::chunks * sizeof(chunk_t), "value<Bits> is not compatible with C layout"); type = ALIAS; + flags = DRIVEN_COMB; width = Bits; lsb_at = lsb_offset; depth = 1; @@ -904,6 +921,7 @@ struct debug_item : ::cxxrtl_object { sizeof(item.next) == value<Bits>::chunks * sizeof(chunk_t), "wire<Bits> is not compatible with C layout"); type = ALIAS; + flags = DRIVEN_COMB; width = Bits; lsb_at = lsb_offset; depth = 1; diff --git a/backends/cxxrtl/cxxrtl_backend.cc b/backends/cxxrtl/cxxrtl_backend.cc index 6d3c2f4f9..a48ea5b23 100644 --- a/backends/cxxrtl/cxxrtl_backend.cc +++ b/backends/cxxrtl/cxxrtl_backend.cc @@ -22,6 +22,7 @@ #include "kernel/sigtools.h" #include "kernel/utils.h" #include "kernel/celltypes.h" +#include "kernel/mem.h" #include "kernel/log.h" USING_YOSYS_NAMESPACE @@ -200,16 +201,12 @@ bool is_elidable_cell(RTLIL::IdString type) ID($mux), ID($concat), ID($slice), ID($pmux)); } -bool is_sync_ff_cell(RTLIL::IdString type) -{ - return type.in( - ID($dff), ID($dffe), ID($sdff), ID($sdffe), ID($sdffce)); -} - bool is_ff_cell(RTLIL::IdString type) { - return is_sync_ff_cell(type) || type.in( - ID($adff), ID($adffe), ID($dffsr), ID($dffsre), ID($dlatch), ID($adlatch), ID($dlatchsr), ID($sr)); + return type.in( + ID($dff), ID($dffe), ID($sdff), ID($sdffe), ID($sdffce), + ID($adff), ID($adffe), ID($dffsr), ID($dffsre), + ID($dlatch), ID($adlatch), ID($dlatchsr), ID($sr)); } bool is_internal_cell(RTLIL::IdString type) @@ -277,6 +274,7 @@ struct FlowGraph { std::vector<Node*> nodes; dict<const RTLIL::Wire*, pool<Node*, hash_ptr_ops>> wire_comb_defs, wire_sync_defs, wire_uses; dict<const RTLIL::Wire*, bool> wire_def_elidable, wire_use_elidable; + dict<RTLIL::SigBit, bool> bit_has_state; ~FlowGraph() { @@ -284,17 +282,24 @@ struct FlowGraph { delete node; } - void add_defs(Node *node, const RTLIL::SigSpec &sig, bool fully_sync, bool elidable) + void add_defs(Node *node, const RTLIL::SigSpec &sig, bool is_ff, bool elidable) { for (auto chunk : sig.chunks()) if (chunk.wire) { - if (fully_sync) + if (is_ff) { + // A sync def means that a wire holds design state because it is driven directly by + // a flip-flop output. Such a wire can never be unbuffered. wire_sync_defs[chunk.wire].insert(node); - else + } else { + // A comb def means that a wire doesn't hold design state. It might still be connected, + // indirectly, to a flip-flop output. wire_comb_defs[chunk.wire].insert(node); + } } + for (auto bit : sig.bits()) + bit_has_state[bit] |= is_ff; // Only comb defs of an entire wire in the right order can be elided. - if (!fully_sync && sig.is_wire()) + if (!is_ff && sig.is_wire()) wire_def_elidable[sig.as_wire()] = elidable; } @@ -322,7 +327,7 @@ struct FlowGraph { // Connections void add_connect_defs_uses(Node *node, const RTLIL::SigSig &conn) { - add_defs(node, conn.first, /*fully_sync=*/false, /*elidable=*/true); + add_defs(node, conn.first, /*is_ff=*/false, /*elidable=*/true); add_uses(node, conn.second); } @@ -369,7 +374,7 @@ struct FlowGraph { if (cell->output(conn.first)) if (is_cxxrtl_sync_port(cell, conn.first)) { // See note regarding elidability below. - add_defs(node, conn.second, /*fully_sync=*/false, /*elidable=*/false); + add_defs(node, conn.second, /*is_ff=*/false, /*elidable=*/false); } } @@ -378,18 +383,18 @@ struct FlowGraph { for (auto conn : cell->connections()) { if (cell->output(conn.first)) { if (is_elidable_cell(cell->type)) - add_defs(node, conn.second, /*fully_sync=*/false, /*elidable=*/true); - else if (is_sync_ff_cell(cell->type) || (cell->type == ID($memrd) && cell->getParam(ID::CLK_ENABLE).as_bool())) - add_defs(node, conn.second, /*fully_sync=*/true, /*elidable=*/false); + add_defs(node, conn.second, /*is_ff=*/false, /*elidable=*/true); + else if (is_ff_cell(cell->type) || (cell->type == ID($memrd) && cell->getParam(ID::CLK_ENABLE).as_bool())) + add_defs(node, conn.second, /*is_ff=*/true, /*elidable=*/false); else if (is_internal_cell(cell->type)) - add_defs(node, conn.second, /*fully_sync=*/false, /*elidable=*/false); + add_defs(node, conn.second, /*is_ff=*/false, /*elidable=*/false); else if (!is_cxxrtl_sync_port(cell, conn.first)) { // Although at first it looks like outputs of user-defined cells may always be elided, the reality is // more complex. Fully sync outputs produce no defs and so don't participate in elision. Fully comb // outputs are assigned in a different way depending on whether the cell's eval() immediately converged. // Unknown/mixed outputs could be elided, but should be rare in practical designs and don't justify // the infrastructure required to elide outputs of cells with many of them. - add_defs(node, conn.second, /*fully_sync=*/false, /*elidable=*/false); + add_defs(node, conn.second, /*is_ff=*/false, /*elidable=*/false); } } if (cell->input(conn.first)) @@ -427,7 +432,7 @@ struct FlowGraph { void add_case_defs_uses(Node *node, const RTLIL::CaseRule *case_) { for (auto &action : case_->actions) { - add_defs(node, action.first, /*is_sync=*/false, /*elidable=*/false); + add_defs(node, action.first, /*is_ff=*/false, /*elidable=*/false); add_uses(node, action.second); } for (auto sub_switch : case_->switches) { @@ -446,9 +451,9 @@ struct FlowGraph { for (auto sync : process->syncs) for (auto action : sync->actions) { if (sync->type == RTLIL::STp || sync->type == RTLIL::STn || sync->type == RTLIL::STe) - add_defs(node, action.first, /*is_sync=*/true, /*elidable=*/false); + add_defs(node, action.first, /*is_ff=*/true, /*elidable=*/false); else - add_defs(node, action.first, /*is_sync=*/false, /*elidable=*/false); + add_defs(node, action.first, /*is_ff=*/false, /*elidable=*/false); add_uses(node, action.second); } } @@ -522,6 +527,7 @@ struct CxxrtlWorker { std::ostream *impl_f = nullptr; std::ostream *intf_f = nullptr; + bool run_hierarchy = false; bool run_flatten = false; bool run_proc = false; @@ -549,6 +555,7 @@ struct CxxrtlWorker { pool<const RTLIL::Wire*> localized_wires; dict<const RTLIL::Wire*, const RTLIL::Wire*> debug_alias_wires; dict<const RTLIL::Wire*, RTLIL::Const> debug_const_wires; + dict<RTLIL::SigBit, bool> bit_has_state; dict<const RTLIL::Module*, pool<std::string>> blackbox_specializations; dict<const RTLIL::Module*, bool> eval_converges; @@ -1142,7 +1149,7 @@ struct CxxrtlWorker { } // The generated code has two bounds checks; one in an assertion, and another that guards the read. // This is done so that the code does not invoke undefined behavior under any conditions, but nevertheless - // loudly crashes if an illegal condition is encountered. The assert may be turned off with -NDEBUG not + // loudly crashes if an illegal condition is encountered. The assert may be turned off with -DNDEBUG not // just for release builds, but also to make sure the simulator (which is presumably embedded in some // larger program) will never crash the code that calls into it. // @@ -1635,6 +1642,10 @@ struct CxxrtlWorker { size_t count_alias_wires = 0; size_t count_member_wires = 0; size_t count_skipped_wires = 0; + size_t count_driven_sync = 0; + size_t count_driven_comb = 0; + size_t count_undriven = 0; + size_t count_mixed_driver = 0; inc_indent(); f << indent << "assert(path.empty() || path[path.size() - 1] == ' ');\n"; for (auto wire : module->wires()) { @@ -1660,9 +1671,55 @@ struct CxxrtlWorker { count_alias_wires++; } else if (!localized_wires.count(wire)) { // Member wire + std::vector<std::string> flags; + + if (wire->port_input && wire->port_output) + flags.push_back("INOUT"); + else if (wire->port_input) + flags.push_back("INPUT"); + else if (wire->port_output) + flags.push_back("OUTPUT"); + + bool has_driven_sync = false; + bool has_driven_comb = false; + bool has_undriven = false; + SigSpec sig(wire); + for (auto bit : sig.bits()) + if (!bit_has_state.count(bit)) + has_undriven = true; + else if (bit_has_state[bit]) + has_driven_sync = true; + else + has_driven_comb = true; + if (has_driven_sync) + flags.push_back("DRIVEN_SYNC"); + if (has_driven_sync && !has_driven_comb && !has_undriven) + count_driven_sync++; + if (has_driven_comb) + flags.push_back("DRIVEN_COMB"); + if (!has_driven_sync && has_driven_comb && !has_undriven) + count_driven_comb++; + if (has_undriven) + flags.push_back("UNDRIVEN"); + if (!has_driven_sync && !has_driven_comb && has_undriven) + count_undriven++; + if (has_driven_sync + has_driven_comb + has_undriven > 1) + count_mixed_driver++; + f << indent << "items.add(path + " << escape_cxx_string(get_hdl_name(wire)); f << ", debug_item(" << mangle(wire) << ", "; - f << wire->start_offset << "));\n"; + f << wire->start_offset; + bool first = true; + for (auto flag : flags) { + if (first) { + first = false; + f << ", "; + } else { + f << "|"; + } + f << "debug_item::" << flag; + } + f << "));\n"; count_member_wires++; } else { count_skipped_wires++; @@ -1690,7 +1747,11 @@ struct CxxrtlWorker { log_debug(" Public wires: %zu, of which:\n", count_public_wires); log_debug(" Const wires: %zu\n", count_const_wires); log_debug(" Alias wires: %zu\n", count_alias_wires); - log_debug(" Member wires: %zu\n", count_member_wires); + log_debug(" Member wires: %zu, of which:\n", count_member_wires); + log_debug(" Driven sync: %zu\n", count_driven_sync); + log_debug(" Driven comb: %zu\n", count_driven_comb); + log_debug(" Undriven: %zu\n", count_undriven); + log_debug(" Mixed driver: %zu\n", count_mixed_driver); log_debug(" Other wires: %zu (no debug information)\n", count_skipped_wires); } @@ -2123,6 +2184,8 @@ struct CxxrtlWorker { if (wire->name.begins_with("$") && !elide_internal) continue; if (wire->name.begins_with("\\") && !elide_public) continue; if (edge_wires[wire]) continue; + if (flow.wire_comb_defs[wire].size() > 1) + log_cmd_error("Wire %s.%s has multiple drivers.\n", log_id(module), log_id(wire)); log_assert(flow.wire_comb_defs[wire].size() == 1); elided_wires[wire] = **flow.wire_comb_defs[wire].begin(); } @@ -2209,6 +2272,9 @@ struct CxxrtlWorker { eval_converges[module] = feedback_wires.empty() && buffered_comb_wires.empty(); + for (auto item : flow.bit_has_state) + bit_has_state.insert(item); + if (debug_info) { // Find wires that alias other wires or are tied to a constant; debug information can be enriched with these // at essentially zero additional cost. @@ -2264,9 +2330,9 @@ struct CxxrtlWorker { } } - void check_design(RTLIL::Design *design, bool &has_sync_init, bool &has_packed_mem) + void check_design(RTLIL::Design *design, bool &has_top, bool &has_sync_init, bool &has_packed_mem) { - has_sync_init = has_packed_mem = false; + has_sync_init = has_packed_mem = has_top = false; for (auto module : design->modules()) { if (module->get_blackbox_attribute() && !module->has_attribute(ID(cxxrtl_blackbox))) @@ -2278,13 +2344,17 @@ struct CxxrtlWorker { if (!design->selected_module(module)) continue; + if (module->get_bool_attribute(ID::top)) + has_top = true; + for (auto proc : module->processes) for (auto sync : proc.second->syncs) if (sync->type == RTLIL::STi) has_sync_init = true; - for (auto cell : module->cells()) - if (cell->type == ID($mem)) + // The Mem constructor also checks for well-formedness of $meminit cells, if any. + for (auto &mem : Mem::get_all_memories(module)) + if (mem.packed) has_packed_mem = true; } } @@ -2292,9 +2362,13 @@ struct CxxrtlWorker { void prepare_design(RTLIL::Design *design) { bool did_anything = false; - bool has_sync_init, has_packed_mem; + bool has_top, has_sync_init, has_packed_mem; log_push(); - check_design(design, has_sync_init, has_packed_mem); + check_design(design, has_top, has_sync_init, has_packed_mem); + if (run_hierarchy && !has_top) { + Pass::call(design, "hierarchy -auto-top"); + did_anything = true; + } if (run_flatten) { Pass::call(design, "flatten"); did_anything = true; @@ -2315,9 +2389,9 @@ struct CxxrtlWorker { did_anything = true; } // Recheck the design if it was modified. - if (has_sync_init || has_packed_mem) - check_design(design, has_sync_init, has_packed_mem); - log_assert(!(has_sync_init || has_packed_mem)); + if (did_anything) + check_design(design, has_top, has_sync_init, has_packed_mem); + log_assert(has_top && !has_sync_init && !has_packed_mem); log_pop(); if (did_anything) log_spacer(); @@ -2499,6 +2573,11 @@ struct CxxrtlBackend : public Backend { log(" place the generated code into namespace <ns-name>. if not specified,\n"); log(" \"cxxrtl_design\" is used.\n"); log("\n"); + log(" -nohierarchy\n"); + log(" use design hierarchy as-is. in most designs, a top module should be\n"); + log(" present as it is exposed through the C API and has unbuffered outputs\n"); + log(" for improved performance; it will be determined automatically if absent.\n"); + log("\n"); log(" -noflatten\n"); log(" don't flatten the design. fully flattened designs can evaluate within\n"); log(" one delta cycle if they have no combinatorial feedback.\n"); @@ -2555,6 +2634,7 @@ struct CxxrtlBackend : public Backend { void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) override { + bool nohierarchy = false; bool noflatten = false; bool noproc = false; int opt_level = DEFAULT_OPT_LEVEL; @@ -2566,6 +2646,10 @@ struct CxxrtlBackend : public Backend { size_t argidx; for (argidx = 1; argidx < args.size(); argidx++) { + if (args[argidx] == "-nohierarchy") { + nohierarchy = true; + continue; + } if (args[argidx] == "-noflatten") { noflatten = true; continue; @@ -2611,6 +2695,7 @@ struct CxxrtlBackend : public Backend { } extra_args(f, filename, args, argidx); + worker.run_hierarchy = !nohierarchy; worker.run_flatten = !noflatten; worker.run_proc = !noproc; switch (opt_level) { diff --git a/backends/cxxrtl/cxxrtl_capi.h b/backends/cxxrtl/cxxrtl_capi.h index 1f1942803..385d6dcf3 100644 --- a/backends/cxxrtl/cxxrtl_capi.h +++ b/backends/cxxrtl/cxxrtl_capi.h @@ -73,6 +73,10 @@ int cxxrtl_commit(cxxrtl_handle handle); size_t cxxrtl_step(cxxrtl_handle handle); // Type of a simulated object. +// +// The type of a simulated object indicates the way it is stored and the operations that are legal +// to perform on it (i.e. won't crash the simulation). It says very little about object semantics, +// which is specified through flags. enum cxxrtl_type { // Values correspond to singly buffered netlist nodes, i.e. nodes driven exclusively by // combinatorial cells, or toplevel input nodes. @@ -86,7 +90,8 @@ enum cxxrtl_type { CXXRTL_VALUE = 0, // Wires correspond to doubly buffered netlist nodes, i.e. nodes driven, at least in part, by - // storage cells, or by combinatorial cells that are a part of a feedback path. + // storage cells, or by combinatorial cells that are a part of a feedback path. They are also + // present in non-optimized builds. // // Wires can be inspected via the `curr` pointer and modified via the `next` pointer (which are // distinct for wires). Note that changes to the bits driven by combinatorial cells will be @@ -103,7 +108,7 @@ enum cxxrtl_type { CXXRTL_MEMORY = 2, // Aliases correspond to netlist nodes driven by another node such that their value is always - // exactly equal, or driven by a constant value. + // exactly equal. // // Aliases can be inspected via the `curr` pointer. They cannot be modified, and the `next` // pointer is always NULL. @@ -112,6 +117,66 @@ enum cxxrtl_type { // More object types may be added in the future, but the existing ones will never change. }; +// Flags of a simulated object. +// +// The flags of a simulated object indicate its role in the netlist: +// * The flags `CXXRTL_INPUT` and `CXXRTL_OUTPUT` designate module ports. +// * The flags `CXXRTL_DRIVEN_SYNC`, `CXXRTL_DRIVEN_COMB`, and `CXXRTL_UNDRIVEN` specify +// the semantics of node state. An object with several of these flags set has different bits +// follow different semantics. +enum cxxrtl_flag { + // Node is a module input port. + // + // This flag can be set on objects of type `CXXRTL_VALUE` and `CXXRTL_WIRE`. It may be combined + // with `CXXRTL_OUTPUT`, as well as other flags. + CXXRTL_INPUT = 1 << 0, + + // Node is a module output port. + // + // This flag can be set on objects of type `CXXRTL_WIRE`. It may be combined with `CXXRTL_INPUT`, + // as well as other flags. + CXXRTL_OUTPUT = 1 << 1, + + // Node is a module inout port. + // + // This flag can be set on objects of type `CXXRTL_WIRE`. It may be combined with other flags. + CXXRTL_INOUT = (CXXRTL_INPUT|CXXRTL_OUTPUT), + + // Node has bits that are driven by a storage cell. + // + // This flag can be set on objects of type `CXXRTL_WIRE`. It may be combined with + // `CXXRTL_DRIVEN_COMB` and `CXXRTL_UNDRIVEN`, as well as other flags. + // + // This flag is set on wires that have bits connected directly to the output of a flip-flop or + // a latch, and hold its state. Many `CXXRTL_WIRE` objects may not have the `CXXRTL_DRIVEN_SYNC` + // flag set; for example, output ports and feedback wires generally won't. Writing to the `next` + // pointer of these wires updates stored state, and for designs without combinatorial loops, + // capturing the value from every of these wires through the `curr` pointer creates a complete + // snapshot of the design state. + CXXRTL_DRIVEN_SYNC = 1 << 2, + + // Node has bits that are driven by a combinatorial cell or another node. + // + // This flag can be set on objects of type `CXXRTL_VALUE` and `CXXRTL_WIRE`. It may be combined + // with `CXXRTL_DRIVEN_SYNC` and `CXXRTL_UNDRIVEN`, as well as other flags. + // + // This flag is set on objects that have bits connected to the output of a combinatorial cell, + // or directly to another node. For designs without combinatorial loops, writing to such bits + // through the `next` pointer (if it is not NULL) has no effect. + CXXRTL_DRIVEN_COMB = 1 << 3, + + // Node has bits that are not driven. + // + // This flag can be set on objects of type `CXXRTL_VALUE` and `CXXRTL_WIRE`. It may be combined + // with `CXXRTL_DRIVEN_SYNC` and `CXXRTL_DRIVEN_COMB`, as well as other flags. + // + // This flag is set on objects that have bits not driven by an output of any cell or by another + // node, such as inputs and dangling wires. + CXXRTL_UNDRIVEN = 1 << 4, + + // More object flags may be added in the future, but the existing ones will never change. +}; + // Description of a simulated object. // // The `data` array can be accessed directly to inspect and, if applicable, modify the bits @@ -123,6 +188,9 @@ struct cxxrtl_object { // determines all other properties of the object. uint32_t type; // actually `enum cxxrtl_type` + // Flags of the object. + uint32_t flags; // actually bit mask of `enum cxxrtl_flags` + // Width of the object in bits. size_t width; diff --git a/backends/edif/edif.cc b/backends/edif/edif.cc index 5e6becfd0..e0013238c 100644 --- a/backends/edif/edif.cc +++ b/backends/edif/edif.cc @@ -330,7 +330,7 @@ struct EdifBackend : public Backend { } *f << stringf("\n (property %s (string \"%d'h%s\"))", EDIF_DEF(name), GetSize(val.bits), hex_string.c_str()); } - }; + }; for (auto module : sorted_modules) { if (module->get_blackbox_attribute()) @@ -373,8 +373,8 @@ struct EdifBackend : public Backend { } { - int c1 = w1->name[0] == '\\'; - int c2 = w2->name[0] == '\\'; + int c1 = w1->name.isPublic(); + int c2 = w2->name.isPublic(); if (c1 > c2) goto promote; if (c1 < c2) goto nopromote; @@ -524,7 +524,7 @@ struct EdifBackend : public Backend { *f << stringf(" (portRef %c (instanceRef GND))\n", gndvccy ? 'Y' : 'G'); if (sig == RTLIL::State::S1) *f << stringf(" (portRef %c (instanceRef VCC))\n", gndvccy ? 'Y' : 'P'); - } + } *f << stringf(" )"); if (attr_properties && sig.wire != NULL) for (auto &p : sig.wire->attributes) diff --git a/backends/ilang/Makefile.inc b/backends/ilang/Makefile.inc deleted file mode 100644 index 52fc2b891..000000000 --- a/backends/ilang/Makefile.inc +++ /dev/null @@ -1,3 +0,0 @@ - -OBJS += backends/ilang/ilang_backend.o - diff --git a/backends/intersynth/intersynth.cc b/backends/intersynth/intersynth.cc index 98a14173b..a6b36de6c 100644 --- a/backends/intersynth/intersynth.cc +++ b/backends/intersynth/intersynth.cc @@ -59,7 +59,7 @@ struct IntersynthBackend : public Backend { log(" do not generate celltypes and conntypes commands. i.e. just output\n"); log(" the netlists. this is used for postsilicon synthesis.\n"); log("\n"); - log(" -lib <verilog_or_ilang_file>\n"); + log(" -lib <verilog_or_rtlil_file>\n"); log(" Use the specified library file for determining whether cell ports are\n"); log(" inputs or outputs. This option can be used multiple times to specify\n"); log(" more than one library.\n"); @@ -108,7 +108,7 @@ struct IntersynthBackend : public Backend { if (f.fail()) log_error("Can't open lib file `%s'.\n", filename.c_str()); RTLIL::Design *lib = new RTLIL::Design; - Frontend::frontend_call(lib, &f, filename, (filename.size() > 3 && filename.compare(filename.size()-3, std::string::npos, ".il") == 0 ? "ilang" : "verilog")); + Frontend::frontend_call(lib, &f, filename, (filename.size() > 3 && filename.compare(filename.size()-3, std::string::npos, ".il") == 0 ? "rtlil" : "verilog")); libs.push_back(lib); } diff --git a/backends/rtlil/Makefile.inc b/backends/rtlil/Makefile.inc new file mode 100644 index 000000000..f691282ca --- /dev/null +++ b/backends/rtlil/Makefile.inc @@ -0,0 +1,3 @@ + +OBJS += backends/rtlil/rtlil_backend.o + diff --git a/backends/ilang/ilang_backend.cc b/backends/rtlil/rtlil_backend.cc index aa5a175ca..01b4bde53 100644 --- a/backends/ilang/ilang_backend.cc +++ b/backends/rtlil/rtlil_backend.cc @@ -18,19 +18,19 @@ * --- * * A very simple and straightforward backend for the RTLIL text - * representation (as understood by the 'ilang' frontend). + * representation. * */ -#include "ilang_backend.h" +#include "rtlil_backend.h" #include "kernel/yosys.h" #include <errno.h> USING_YOSYS_NAMESPACE -using namespace ILANG_BACKEND; +using namespace RTLIL_BACKEND; YOSYS_NAMESPACE_BEGIN -void ILANG_BACKEND::dump_const(std::ostream &f, const RTLIL::Const &data, int width, int offset, bool autoint) +void RTLIL_BACKEND::dump_const(std::ostream &f, const RTLIL::Const &data, int width, int offset, bool autoint) { if (width < 0) width = data.bits.size() - offset; @@ -83,7 +83,7 @@ void ILANG_BACKEND::dump_const(std::ostream &f, const RTLIL::Const &data, int wi } } -void ILANG_BACKEND::dump_sigchunk(std::ostream &f, const RTLIL::SigChunk &chunk, bool autoint) +void RTLIL_BACKEND::dump_sigchunk(std::ostream &f, const RTLIL::SigChunk &chunk, bool autoint) { if (chunk.wire == NULL) { dump_const(f, chunk.data, chunk.width, chunk.offset, autoint); @@ -97,7 +97,7 @@ void ILANG_BACKEND::dump_sigchunk(std::ostream &f, const RTLIL::SigChunk &chunk, } } -void ILANG_BACKEND::dump_sigspec(std::ostream &f, const RTLIL::SigSpec &sig, bool autoint) +void RTLIL_BACKEND::dump_sigspec(std::ostream &f, const RTLIL::SigSpec &sig, bool autoint) { if (sig.is_chunk()) { dump_sigchunk(f, sig.as_chunk(), autoint); @@ -111,7 +111,7 @@ void ILANG_BACKEND::dump_sigspec(std::ostream &f, const RTLIL::SigSpec &sig, boo } } -void ILANG_BACKEND::dump_wire(std::ostream &f, std::string indent, const RTLIL::Wire *wire) +void RTLIL_BACKEND::dump_wire(std::ostream &f, std::string indent, const RTLIL::Wire *wire) { for (auto &it : wire->attributes) { f << stringf("%s" "attribute %s ", indent.c_str(), it.first.c_str()); @@ -136,7 +136,7 @@ void ILANG_BACKEND::dump_wire(std::ostream &f, std::string indent, const RTLIL:: f << stringf("%s\n", wire->name.c_str()); } -void ILANG_BACKEND::dump_memory(std::ostream &f, std::string indent, const RTLIL::Memory *memory) +void RTLIL_BACKEND::dump_memory(std::ostream &f, std::string indent, const RTLIL::Memory *memory) { for (auto &it : memory->attributes) { f << stringf("%s" "attribute %s ", indent.c_str(), it.first.c_str()); @@ -153,7 +153,7 @@ void ILANG_BACKEND::dump_memory(std::ostream &f, std::string indent, const RTLIL f << stringf("%s\n", memory->name.c_str()); } -void ILANG_BACKEND::dump_cell(std::ostream &f, std::string indent, const RTLIL::Cell *cell) +void RTLIL_BACKEND::dump_cell(std::ostream &f, std::string indent, const RTLIL::Cell *cell) { for (auto &it : cell->attributes) { f << stringf("%s" "attribute %s ", indent.c_str(), it.first.c_str()); @@ -177,7 +177,7 @@ void ILANG_BACKEND::dump_cell(std::ostream &f, std::string indent, const RTLIL:: f << stringf("%s" "end\n", indent.c_str()); } -void ILANG_BACKEND::dump_proc_case_body(std::ostream &f, std::string indent, const RTLIL::CaseRule *cs) +void RTLIL_BACKEND::dump_proc_case_body(std::ostream &f, std::string indent, const RTLIL::CaseRule *cs) { for (auto it = cs->actions.begin(); it != cs->actions.end(); ++it) { @@ -192,7 +192,7 @@ void ILANG_BACKEND::dump_proc_case_body(std::ostream &f, std::string indent, con dump_proc_switch(f, indent, *it); } -void ILANG_BACKEND::dump_proc_switch(std::ostream &f, std::string indent, const RTLIL::SwitchRule *sw) +void RTLIL_BACKEND::dump_proc_switch(std::ostream &f, std::string indent, const RTLIL::SwitchRule *sw) { for (auto it = sw->attributes.begin(); it != sw->attributes.end(); ++it) { f << stringf("%s" "attribute %s ", indent.c_str(), it->first.c_str()); @@ -225,7 +225,7 @@ void ILANG_BACKEND::dump_proc_switch(std::ostream &f, std::string indent, const f << stringf("%s" "end\n", indent.c_str()); } -void ILANG_BACKEND::dump_proc_sync(std::ostream &f, std::string indent, const RTLIL::SyncRule *sy) +void RTLIL_BACKEND::dump_proc_sync(std::ostream &f, std::string indent, const RTLIL::SyncRule *sy) { f << stringf("%s" "sync ", indent.c_str()); switch (sy->type) { @@ -251,7 +251,7 @@ void ILANG_BACKEND::dump_proc_sync(std::ostream &f, std::string indent, const RT } } -void ILANG_BACKEND::dump_proc(std::ostream &f, std::string indent, const RTLIL::Process *proc) +void RTLIL_BACKEND::dump_proc(std::ostream &f, std::string indent, const RTLIL::Process *proc) { for (auto it = proc->attributes.begin(); it != proc->attributes.end(); ++it) { f << stringf("%s" "attribute %s ", indent.c_str(), it->first.c_str()); @@ -265,7 +265,7 @@ void ILANG_BACKEND::dump_proc(std::ostream &f, std::string indent, const RTLIL:: f << stringf("%s" "end\n", indent.c_str()); } -void ILANG_BACKEND::dump_conn(std::ostream &f, std::string indent, const RTLIL::SigSpec &left, const RTLIL::SigSpec &right) +void RTLIL_BACKEND::dump_conn(std::ostream &f, std::string indent, const RTLIL::SigSpec &left, const RTLIL::SigSpec &right) { f << stringf("%s" "connect ", indent.c_str()); dump_sigspec(f, left); @@ -274,7 +274,7 @@ void ILANG_BACKEND::dump_conn(std::ostream &f, std::string indent, const RTLIL:: f << stringf("\n"); } -void ILANG_BACKEND::dump_module(std::ostream &f, std::string indent, RTLIL::Module *module, RTLIL::Design *design, bool only_selected, bool flag_m, bool flag_n) +void RTLIL_BACKEND::dump_module(std::ostream &f, std::string indent, RTLIL::Module *module, RTLIL::Design *design, bool only_selected, bool flag_m, bool flag_n) { bool print_header = flag_m || design->selected_whole_module(module->name); bool print_body = !flag_n || !design->selected_whole_module(module->name); @@ -360,7 +360,7 @@ void ILANG_BACKEND::dump_module(std::ostream &f, std::string indent, RTLIL::Modu f << stringf("%s" "end\n", indent.c_str()); } -void ILANG_BACKEND::dump_design(std::ostream &f, RTLIL::Design *design, bool only_selected, bool flag_m, bool flag_n) +void RTLIL_BACKEND::dump_design(std::ostream &f, RTLIL::Design *design, bool only_selected, bool flag_m, bool flag_n) { int init_autoidx = autoidx; @@ -396,15 +396,15 @@ void ILANG_BACKEND::dump_design(std::ostream &f, RTLIL::Design *design, bool onl YOSYS_NAMESPACE_END PRIVATE_NAMESPACE_BEGIN -struct IlangBackend : public Backend { - IlangBackend() : Backend("ilang", "write design to ilang file") { } +struct RTLILBackend : public Backend { + RTLILBackend() : Backend("rtlil", "write design to RTLIL file") { } void help() override { // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| log("\n"); - log(" write_ilang [filename]\n"); + log(" write_rtlil [filename]\n"); log("\n"); - log("Write the current design to an 'ilang' file. (ilang is a text representation\n"); + log("Write the current design to an RTLIL file. (RTLIL is a text representation\n"); log("of a design in yosys's internal format.)\n"); log("\n"); log(" -selected\n"); @@ -415,7 +415,7 @@ struct IlangBackend : public Backend { { bool selected = false; - log_header(design, "Executing ILANG backend.\n"); + log_header(design, "Executing RTLIL backend.\n"); size_t argidx; for (argidx = 1; argidx < args.size(); argidx++) { @@ -432,12 +432,27 @@ struct IlangBackend : public Backend { log("Output filename: %s\n", filename.c_str()); *f << stringf("# Generated by %s\n", yosys_version_str); - ILANG_BACKEND::dump_design(*f, design, selected, true, false); + RTLIL_BACKEND::dump_design(*f, design, selected, true, false); + } +} RTLILBackend; + +struct IlangBackend : public Backend { + IlangBackend() : Backend("ilang", "(deprecated) alias of write_rtlil") { } + void help() override + { + // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| + log("\n"); + log("See `help write_rtlil`.\n"); + log("\n"); + } + void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) override + { + RTLILBackend.execute(f, filename, args, design); } } IlangBackend; struct DumpPass : public Pass { - DumpPass() : Pass("dump", "print parts of the design in ilang format") { } + DumpPass() : Pass("dump", "print parts of the design in RTLIL format") { } void help() override { // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| @@ -445,7 +460,7 @@ struct DumpPass : public Pass { log(" dump [options] [selection]\n"); log("\n"); log("Write the selected parts of the design to the console or specified file in\n"); - log("ilang format.\n"); + log("RTLIL format.\n"); log("\n"); log(" -m\n"); log(" also dump the module headers, even if only parts of a single\n"); @@ -508,7 +523,7 @@ struct DumpPass : public Pass { f = &buf; } - ILANG_BACKEND::dump_design(*f, design, true, flag_m, flag_n); + RTLIL_BACKEND::dump_design(*f, design, true, flag_m, flag_n); if (!filename.empty()) { delete f; diff --git a/backends/ilang/ilang_backend.h b/backends/rtlil/rtlil_backend.h index 97dcbb628..77eea353c 100644 --- a/backends/ilang/ilang_backend.h +++ b/backends/rtlil/rtlil_backend.h @@ -18,19 +18,19 @@ * --- * * A very simple and straightforward backend for the RTLIL text - * representation (as understood by the 'ilang' frontend). + * representation. * */ -#ifndef ILANG_BACKEND_H -#define ILANG_BACKEND_H +#ifndef RTLIL_BACKEND_H +#define RTLIL_BACKEND_H #include "kernel/yosys.h" #include <stdio.h> YOSYS_NAMESPACE_BEGIN -namespace ILANG_BACKEND { +namespace RTLIL_BACKEND { void dump_const(std::ostream &f, const RTLIL::Const &data, int width = -1, int offset = 0, bool autoint = true); void dump_sigchunk(std::ostream &f, const RTLIL::SigChunk &chunk, bool autoint = true); void dump_sigspec(std::ostream &f, const RTLIL::SigSpec &sig, bool autoint = true); diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index a79c0bd99..a185fdd74 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -22,6 +22,7 @@ #include "kernel/sigtools.h" #include "kernel/celltypes.h" #include "kernel/log.h" +#include "kernel/mem.h" #include <string> USING_YOSYS_NAMESPACE @@ -40,12 +41,15 @@ struct Smt2Worker std::map<RTLIL::SigBit, RTLIL::Cell*> bit_driver; std::set<RTLIL::Cell*> exported_cells, hiercells, hiercells_queue; pool<Cell*> recursive_cells, registers; + std::vector<Mem> memories; + dict<Cell*, Mem*> mem_cells; + std::set<Mem*> memory_queue; pool<SigBit> clock_posedge, clock_negedge; vector<string> ex_state_eq, ex_input_eq; std::map<RTLIL::SigBit, std::pair<int, int>> fcache; - std::map<Cell*, int> memarrays; + std::map<Mem*, int> memarrays; std::map<int, int> bvsizes; dict<IdString, char*> ids; @@ -116,12 +120,73 @@ struct Smt2Worker makebits(stringf("%s_is", get_id(module))); + dict<IdString, Mem*> mem_dict; + memories = Mem::get_all_memories(module); + for (auto &mem : memories) + { + mem_dict[mem.memid] = &mem; + for (auto &port : mem.wr_ports) + { + if (port.clk_enable) { + SigSpec clk = sigmap(port.clk); + for (int i = 0; i < GetSize(clk); i++) + { + if (clk[i].wire == nullptr) + continue; + if (port.clk_polarity) + clock_posedge.insert(clk[i]); + else + clock_negedge.insert(clk[i]); + } + } + for (auto bit : sigmap(port.en)) + noclock.insert(bit); + for (auto bit : sigmap(port.addr)) + noclock.insert(bit); + for (auto bit : sigmap(port.data)) + noclock.insert(bit); + } + for (auto &port : mem.rd_ports) + { + if (port.clk_enable) { + SigSpec clk = sigmap(port.clk); + for (int i = 0; i < GetSize(clk); i++) + { + if (clk[i].wire == nullptr) + continue; + if (port.clk_polarity) + clock_posedge.insert(clk[i]); + else + clock_negedge.insert(clk[i]); + } + } + for (auto bit : sigmap(port.en)) + noclock.insert(bit); + for (auto bit : sigmap(port.addr)) + noclock.insert(bit); + for (auto bit : sigmap(port.data)) + noclock.insert(bit); + Cell *driver = port.cell ? port.cell : mem.cell; + for (auto bit : sigmap(port.data)) { + if (bit_driver.count(bit)) + log_error("Found multiple drivers for %s.\n", log_signal(bit)); + bit_driver[bit] = driver; + } + } + } + for (auto cell : module->cells()) for (auto &conn : cell->connections()) { if (GetSize(conn.second) == 0) continue; + // Handled above. + if (cell->type.in(ID($mem), ID($memrd), ID($memwr), ID($meminit))) { + mem_cells[cell] = mem_dict[cell->parameters.at(ID::MEMID).decode_string()]; + continue; + } + bool is_input = ct.cell_input(cell->type, conn.first); bool is_output = ct.cell_output(cell->type, conn.first); @@ -135,24 +200,6 @@ struct Smt2Worker log_error("Unsupported or unknown directionality on port %s of cell %s.%s (%s).\n", log_id(conn.first), log_id(module), log_id(cell), log_id(cell->type)); - if (cell->type.in(ID($mem)) && conn.first.in(ID::RD_CLK, ID::WR_CLK)) - { - SigSpec clk = sigmap(conn.second); - for (int i = 0; i < GetSize(clk); i++) - { - if (clk[i].wire == nullptr) - continue; - - if (cell->getParam(conn.first == ID::RD_CLK ? ID::RD_CLK_ENABLE : ID::WR_CLK_ENABLE)[i] != State::S1) - continue; - - if (cell->getParam(conn.first == ID::RD_CLK ? ID::RD_CLK_POLARITY : ID::WR_CLK_POLARITY)[i] == State::S1) - clock_posedge.insert(clk[i]); - else - clock_negedge.insert(clk[i]); - } - } - else if (cell->type.in(ID($dff), ID($_DFF_P_), ID($_DFF_N_)) && conn.first.in(ID::CLK, ID::C)) { bool posedge = (cell->type == ID($_DFF_N_)) || (cell->type == ID($dff) && cell->getParam(ID::CLK_POLARITY).as_bool()); @@ -647,27 +694,35 @@ struct Smt2Worker // FIXME: $slice $concat } - if (memmode && cell->type == ID($mem)) + if (memmode && cell->type.in(ID($mem), ID($memrd), ID($memwr), ID($meminit))) { + Mem *mem = mem_cells[cell]; + + if (memarrays.count(mem)) { + recursive_cells.erase(cell); + return; + } + int arrayid = idcounter++; - memarrays[cell] = arrayid; - - int abits = cell->getParam(ID::ABITS).as_int(); - int width = cell->getParam(ID::WIDTH).as_int(); - int rd_ports = cell->getParam(ID::RD_PORTS).as_int(); - int wr_ports = cell->getParam(ID::WR_PORTS).as_int(); - - bool async_read = false; - if (!cell->getParam(ID::WR_CLK_ENABLE).is_fully_ones()) { - if (!cell->getParam(ID::WR_CLK_ENABLE).is_fully_zero()) - log_error("Memory %s.%s has mixed clocked/nonclocked write ports. This is not supported by \"write_smt2\".\n", log_id(cell), log_id(module)); - async_read = true; + memarrays[mem] = arrayid; + + int abits = ceil_log2(mem->size); + + bool has_sync_wr = false; + bool has_async_wr = false; + for (auto &port : mem->wr_ports) { + if (port.clk_enable) + has_sync_wr = true; + else + has_async_wr = true; } + if (has_async_wr && has_sync_wr) + log_error("Memory %s.%s has mixed clocked/nonclocked write ports. This is not supported by \"write_smt2\".\n", log_id(cell), log_id(module)); - decls.push_back(stringf("; yosys-smt2-memory %s %d %d %d %d %s\n", get_id(cell), abits, width, rd_ports, wr_ports, async_read ? "async" : "sync")); + decls.push_back(stringf("; yosys-smt2-memory %s %d %d %d %d %s\n", get_id(mem->memid), abits, mem->width, GetSize(mem->rd_ports), GetSize(mem->wr_ports), has_async_wr ? "async" : "sync")); string memstate; - if (async_read) { + if (has_async_wr) { memstate = stringf("%s#%d#final", get_id(module), arrayid); } else { memstate = stringf("%s#%d#0", get_id(module), arrayid); @@ -675,80 +730,79 @@ struct Smt2Worker if (statebv) { - int mem_size = cell->getParam(ID::SIZE).as_int(); - int mem_offset = cell->getParam(ID::OFFSET).as_int(); - - makebits(memstate, width*mem_size, get_id(cell)); + makebits(memstate, mem->width*mem->size, get_id(mem->memid)); decls.push_back(stringf("(define-fun |%s_m %s| ((state |%s_s|)) (_ BitVec %d) (|%s| state))\n", - get_id(module), get_id(cell), get_id(module), width*mem_size, memstate.c_str())); + get_id(module), get_id(mem->memid), get_id(module), mem->width*mem->size, memstate.c_str())); - for (int i = 0; i < rd_ports; i++) + for (int i = 0; i < GetSize(mem->rd_ports); i++) { - SigSpec addr_sig = cell->getPort(ID::RD_ADDR).extract(abits*i, abits); - SigSpec data_sig = cell->getPort(ID::RD_DATA).extract(width*i, width); + auto &port = mem->rd_ports[i]; + SigSpec addr_sig = port.addr; + addr_sig.extend_u0(abits); std::string addr = get_bv(addr_sig); - if (cell->getParam(ID::RD_CLK_ENABLE).extract(i).as_bool()) + if (port.clk_enable) 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)); + "Call \"memory\" with -nordff to avoid this error.\n", i, log_signal(port.data), log_id(mem->memid), log_id(module)); decls.push_back(stringf("(define-fun |%s_m:R%dA %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))); + get_id(module), i, get_id(mem->memid), get_id(module), abits, addr.c_str(), log_signal(addr_sig))); std::string read_expr = "#b"; - for (int k = 0; k < width; k++) + for (int k = 0; k < mem->width; k++) read_expr += "0"; - for (int k = 0; k < mem_size; k++) + for (int k = 0; k < mem->size; k++) read_expr = stringf("(ite (= (|%s_m:R%dA %s| state) #b%s) ((_ extract %d %d) (|%s| state))\n %s)", - get_id(module), i, get_id(cell), Const(k+mem_offset, abits).as_string().c_str(), - width*(k+1)-1, width*k, memstate.c_str(), read_expr.c_str()); + get_id(module), i, get_id(mem->memid), Const(k+mem->start_offset, abits).as_string().c_str(), + mem->width*(k+1)-1, mem->width*k, memstate.c_str(), read_expr.c_str()); decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) (_ BitVec %d)\n %s) ; %s\n", - get_id(module), idcounter, get_id(module), width, read_expr.c_str(), log_signal(data_sig))); + get_id(module), idcounter, get_id(module), mem->width, read_expr.c_str(), log_signal(port.data))); decls.push_back(stringf("(define-fun |%s_m:R%dD %s| ((state |%s_s|)) (_ BitVec %d) (|%s#%d| state))\n", - get_id(module), i, get_id(cell), get_id(module), width, get_id(module), idcounter)); + get_id(module), i, get_id(mem->memid), get_id(module), mem->width, get_id(module), idcounter)); - register_bv(data_sig, idcounter++); + register_bv(port.data, idcounter++); } } else { if (statedt) dtmembers.push_back(stringf(" (|%s| (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n", - memstate.c_str(), abits, width, get_id(cell))); + memstate.c_str(), abits, mem->width, get_id(mem->memid))); else decls.push_back(stringf("(declare-fun |%s| (|%s_s|) (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n", - memstate.c_str(), get_id(module), abits, width, get_id(cell))); + memstate.c_str(), get_id(module), abits, mem->width, get_id(mem->memid))); decls.push_back(stringf("(define-fun |%s_m %s| ((state |%s_s|)) (Array (_ BitVec %d) (_ BitVec %d)) (|%s| state))\n", - get_id(module), get_id(cell), get_id(module), abits, width, memstate.c_str())); + get_id(module), get_id(mem->memid), get_id(module), abits, mem->width, memstate.c_str())); - for (int i = 0; i < rd_ports; i++) + for (int i = 0; i < GetSize(mem->rd_ports); i++) { - SigSpec addr_sig = cell->getPort(ID::RD_ADDR).extract(abits*i, abits); - SigSpec data_sig = cell->getPort(ID::RD_DATA).extract(width*i, width); + auto &port = mem->rd_ports[i]; + SigSpec addr_sig = port.addr; + addr_sig.extend_u0(abits); std::string addr = get_bv(addr_sig); - if (cell->getParam(ID::RD_CLK_ENABLE).extract(i).as_bool()) + if (port.clk_enable) 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)); + "Call \"memory\" with -nordff to avoid this error.\n", i, log_signal(port.data), log_id(mem->memid), log_id(module)); decls.push_back(stringf("(define-fun |%s_m:R%dA %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))); + get_id(module), i, get_id(mem->memid), 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| state) (|%s_m:R%dA %s| state))) ; %s\n", - get_id(module), idcounter, get_id(module), width, memstate.c_str(), get_id(module), i, get_id(cell), log_signal(data_sig))); + get_id(module), idcounter, get_id(module), mem->width, memstate.c_str(), get_id(module), i, get_id(mem->memid), log_signal(port.data))); decls.push_back(stringf("(define-fun |%s_m:R%dD %s| ((state |%s_s|)) (_ BitVec %d) (|%s#%d| state))\n", - get_id(module), i, get_id(cell), get_id(module), width, get_id(module), idcounter)); + get_id(module), i, get_id(mem->memid), get_id(module), mem->width, get_id(module), idcounter)); - register_bv(data_sig, idcounter++); + register_bv(port.data, idcounter++); } } - registers.insert(cell); + memory_queue.insert(mem); recursive_cells.erase(cell); return; } @@ -822,40 +876,51 @@ struct Smt2Worker for (auto bit : SigSpec(wire)) if (reg_bits.count(bit)) is_register = true; - if (wire->port_id || is_register || wire->get_bool_attribute(ID::keep) || (wiresmode && wire->name[0] == '\\')) { + if (wire->port_id || is_register || wire->get_bool_attribute(ID::keep) || (wiresmode && wire->name.isPublic())) { RTLIL::SigSpec sig = sigmap(wire); + std::vector<std::string> comments; if (wire->port_input) - decls.push_back(stringf("; yosys-smt2-input %s %d\n", get_id(wire), wire->width)); + comments.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", get_id(wire), wire->width)); + comments.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", get_id(wire), wire->width)); - if (wire->get_bool_attribute(ID::keep) || (wiresmode && wire->name[0] == '\\')) - decls.push_back(stringf("; yosys-smt2-wire %s %d\n", get_id(wire), wire->width)); + comments.push_back(stringf("; yosys-smt2-register %s %d\n", get_id(wire), wire->width)); + if (wire->get_bool_attribute(ID::keep) || (wiresmode && wire->name.isPublic())) + comments.push_back(stringf("; yosys-smt2-wire %s %d\n", get_id(wire), wire->width)); if (GetSize(wire) == 1 && (clock_posedge.count(sig) || clock_negedge.count(sig))) - decls.push_back(stringf("; yosys-smt2-clock %s%s%s\n", get_id(wire), + comments.push_back(stringf("; yosys-smt2-clock %s%s%s\n", get_id(wire), clock_posedge.count(sig) ? " posedge" : "", clock_negedge.count(sig) ? " negedge" : "")); if (bvmode && GetSize(sig) > 1) { + std::string sig_bv = get_bv(sig); + if (!comments.empty()) + decls.insert(decls.end(), comments.begin(), comments.end()); decls.push_back(stringf("(define-fun |%s_n %s| ((state |%s_s|)) (_ BitVec %d) %s)\n", - get_id(module), get_id(wire), get_id(module), GetSize(sig), get_bv(sig).c_str())); + get_id(module), get_id(wire), get_id(module), GetSize(sig), sig_bv.c_str())); if (wire->port_input) ex_input_eq.push_back(stringf(" (= (|%s_n %s| state) (|%s_n %s| other_state))", get_id(module), get_id(wire), get_id(module), get_id(wire))); } else { - for (int i = 0; i < GetSize(sig); i++) + std::vector<std::string> sig_bool; + for (int i = 0; i < GetSize(sig); i++) { + sig_bool.push_back(get_bool(sig[i])); + } + if (!comments.empty()) + decls.insert(decls.end(), comments.begin(), comments.end()); + 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", - get_id(module), get_id(wire), i, get_id(module), get_bool(sig[i]).c_str())); + get_id(module), get_id(wire), i, get_id(module), sig_bool[i].c_str())); if (wire->port_input) ex_input_eq.push_back(stringf(" (= (|%s_n %s %d| state) (|%s_n %s %d| other_state))", get_id(module), get_id(wire), i, get_id(module), get_id(wire), i)); } else { decls.push_back(stringf("(define-fun |%s_n %s| ((state |%s_s|)) Bool %s)\n", - get_id(module), get_id(wire), get_id(module), get_bool(sig[i]).c_str())); + get_id(module), get_id(wire), get_id(module), sig_bool[i].c_str())); if (wire->port_input) ex_input_eq.push_back(stringf(" (= (|%s_n %s| state) (|%s_n %s| other_state))", get_id(module), get_id(wire), get_id(module), get_id(wire))); } + } } } } @@ -966,7 +1031,7 @@ struct Smt2Worker } } - for (int iter = 1; !registers.empty(); iter++) + for (int iter = 1; !registers.empty() || !memory_queue.empty(); iter++) { pool<Cell*> this_regs; this_regs.swap(registers); @@ -999,152 +1064,156 @@ struct Smt2Worker if (cell->type == ID($anyconst)) ex_state_eq.push_back(stringf("(= %s %s)", get_bv(cell->getPort(ID::Y)).c_str(), get_bv(cell->getPort(ID::Y), "other_state").c_str())); } + } - if (cell->type == ID($mem)) - { - int arrayid = memarrays.at(cell); + std::set<Mem*> this_mems; + this_mems.swap(memory_queue); - int abits = cell->getParam(ID::ABITS).as_int(); - int width = cell->getParam(ID::WIDTH).as_int(); - int wr_ports = cell->getParam(ID::WR_PORTS).as_int(); + for (auto mem : this_mems) + { + int arrayid = memarrays.at(mem); - bool async_read = false; - string initial_memstate, final_memstate; + int abits = ceil_log2(mem->size);; - if (!cell->getParam(ID::WR_CLK_ENABLE).is_fully_ones()) { - log_assert(cell->getParam(ID::WR_CLK_ENABLE).is_fully_zero()); - async_read = true; - initial_memstate = stringf("%s#%d#0", get_id(module), arrayid); - final_memstate = stringf("%s#%d#final", get_id(module), arrayid); + bool has_sync_wr = false; + bool has_async_wr = false; + for (auto &port : mem->wr_ports) { + if (port.clk_enable) + has_sync_wr = true; + else + has_async_wr = true; + } + + string initial_memstate, final_memstate; + + if (has_async_wr) { + log_assert(!has_sync_wr); + initial_memstate = stringf("%s#%d#0", get_id(module), arrayid); + final_memstate = stringf("%s#%d#final", get_id(module), arrayid); + } + + if (statebv) + { + if (has_async_wr) { + makebits(final_memstate, mem->width*mem->size, get_id(mem->memid)); } - if (statebv) + for (int i = 0; i < GetSize(mem->wr_ports); i++) { - int mem_size = cell->getParam(ID::SIZE).as_int(); - int mem_offset = cell->getParam(ID::OFFSET).as_int(); - - if (async_read) { - makebits(final_memstate, width*mem_size, get_id(cell)); + auto &port = mem->wr_ports[i]; + SigSpec addr_sig = port.addr; + addr_sig.extend_u0(abits); + + std::string addr = get_bv(addr_sig); + std::string data = get_bv(port.data); + std::string mask = get_bv(port.en); + + decls.push_back(stringf("(define-fun |%s_m:W%dA %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n", + get_id(module), i, get_id(mem->memid), get_id(module), abits, addr.c_str(), log_signal(addr_sig))); + addr = stringf("(|%s_m:W%dA %s| state)", get_id(module), i, get_id(mem->memid)); + + decls.push_back(stringf("(define-fun |%s_m:W%dD %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n", + get_id(module), i, get_id(mem->memid), get_id(module), mem->width, data.c_str(), log_signal(port.data))); + data = stringf("(|%s_m:W%dD %s| state)", get_id(module), i, get_id(mem->memid)); + + decls.push_back(stringf("(define-fun |%s_m:W%dM %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n", + get_id(module), i, get_id(mem->memid), get_id(module), mem->width, mask.c_str(), log_signal(port.en))); + mask = stringf("(|%s_m:W%dM %s| state)", get_id(module), i, get_id(mem->memid)); + + std::string data_expr; + + for (int k = mem->size-1; k >= 0; k--) { + std::string new_data = stringf("(bvor (bvand %s %s) (bvand ((_ extract %d %d) (|%s#%d#%d| state)) (bvnot %s)))", + data.c_str(), mask.c_str(), mem->width*(k+1)-1, mem->width*k, get_id(module), arrayid, i, mask.c_str()); + data_expr += stringf("\n (ite (= %s #b%s) %s ((_ extract %d %d) (|%s#%d#%d| state)))", + addr.c_str(), Const(k+mem->start_offset, abits).as_string().c_str(), new_data.c_str(), + mem->width*(k+1)-1, mem->width*k, get_id(module), arrayid, i); } - for (int i = 0; i < wr_ports; i++) - { - SigSpec addr_sig = cell->getPort(ID::WR_ADDR).extract(abits*i, abits); - SigSpec data_sig = cell->getPort(ID::WR_DATA).extract(width*i, width); - SigSpec mask_sig = cell->getPort(ID::WR_EN).extract(width*i, width); + decls.push_back(stringf("(define-fun |%s#%d#%d| ((state |%s_s|)) (_ BitVec %d) (concat%s)) ; %s\n", + get_id(module), arrayid, i+1, get_id(module), mem->width*mem->size, data_expr.c_str(), get_id(mem->memid))); + } + } + else + { + if (has_async_wr) { + if (statedt) + dtmembers.push_back(stringf(" (|%s| (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n", + initial_memstate.c_str(), abits, mem->width, get_id(mem->memid))); + else + decls.push_back(stringf("(declare-fun |%s| (|%s_s|) (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n", + initial_memstate.c_str(), get_id(module), abits, mem->width, get_id(mem->memid))); + } - std::string addr = get_bv(addr_sig); - std::string data = get_bv(data_sig); - std::string mask = get_bv(mask_sig); + for (int i = 0; i < GetSize(mem->wr_ports); i++) + { + auto &port = mem->wr_ports[i]; + SigSpec addr_sig = port.addr; + addr_sig.extend_u0(abits); - decls.push_back(stringf("(define-fun |%s_m:W%dA %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))); - addr = stringf("(|%s_m:W%dA %s| state)", get_id(module), i, get_id(cell)); + std::string addr = get_bv(addr_sig); + std::string data = get_bv(port.data); + std::string mask = get_bv(port.en); - decls.push_back(stringf("(define-fun |%s_m:W%dD %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n", - get_id(module), i, get_id(cell), get_id(module), width, data.c_str(), log_signal(data_sig))); - data = stringf("(|%s_m:W%dD %s| state)", get_id(module), i, get_id(cell)); + decls.push_back(stringf("(define-fun |%s_m:W%dA %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n", + get_id(module), i, get_id(mem->memid), get_id(module), abits, addr.c_str(), log_signal(addr_sig))); + addr = stringf("(|%s_m:W%dA %s| state)", get_id(module), i, get_id(mem->memid)); - decls.push_back(stringf("(define-fun |%s_m:W%dM %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n", - get_id(module), i, get_id(cell), get_id(module), width, mask.c_str(), log_signal(mask_sig))); - mask = stringf("(|%s_m:W%dM %s| state)", get_id(module), i, get_id(cell)); + decls.push_back(stringf("(define-fun |%s_m:W%dD %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n", + get_id(module), i, get_id(mem->memid), get_id(module), mem->width, data.c_str(), log_signal(port.data))); + data = stringf("(|%s_m:W%dD %s| state)", get_id(module), i, get_id(mem->memid)); - std::string data_expr; + decls.push_back(stringf("(define-fun |%s_m:W%dM %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n", + get_id(module), i, get_id(mem->memid), get_id(module), mem->width, mask.c_str(), log_signal(port.en))); + mask = stringf("(|%s_m:W%dM %s| state)", get_id(module), i, get_id(mem->memid)); - for (int k = mem_size-1; k >= 0; k--) { - std::string new_data = stringf("(bvor (bvand %s %s) (bvand ((_ extract %d %d) (|%s#%d#%d| state)) (bvnot %s)))", - data.c_str(), mask.c_str(), width*(k+1)-1, width*k, get_id(module), arrayid, i, mask.c_str()); - data_expr += stringf("\n (ite (= %s #b%s) %s ((_ extract %d %d) (|%s#%d#%d| state)))", - addr.c_str(), Const(k+mem_offset, abits).as_string().c_str(), new_data.c_str(), - width*(k+1)-1, width*k, get_id(module), arrayid, i); - } + data = stringf("(bvor (bvand %s %s) (bvand (select (|%s#%d#%d| state) %s) (bvnot %s)))", + 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|)) (_ BitVec %d) (concat%s)) ; %s\n", - get_id(module), arrayid, i+1, get_id(module), width*mem_size, data_expr.c_str(), get_id(cell))); - } + 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", + get_id(module), arrayid, i+1, get_id(module), abits, mem->width, + get_id(module), arrayid, i, addr.c_str(), data.c_str(), get_id(mem->memid))); } - else - { - if (async_read) { - if (statedt) - dtmembers.push_back(stringf(" (|%s| (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n", - initial_memstate.c_str(), abits, width, get_id(cell))); - else - decls.push_back(stringf("(declare-fun |%s| (|%s_s|) (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n", - initial_memstate.c_str(), get_id(module), abits, width, get_id(cell))); - } - - for (int i = 0; i < wr_ports; i++) - { - SigSpec addr_sig = cell->getPort(ID::WR_ADDR).extract(abits*i, abits); - SigSpec data_sig = cell->getPort(ID::WR_DATA).extract(width*i, width); - SigSpec mask_sig = cell->getPort(ID::WR_EN).extract(width*i, width); + } - std::string addr = get_bv(addr_sig); - std::string data = get_bv(data_sig); - std::string mask = get_bv(mask_sig); + std::string expr_d = stringf("(|%s#%d#%d| state)", get_id(module), arrayid, GetSize(mem->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(mem->memid))); + ex_state_eq.push_back(stringf("(= (|%s#%d#0| state) (|%s#%d#0| other_state))", get_id(module), arrayid, get_id(module), arrayid)); - decls.push_back(stringf("(define-fun |%s_m:W%dA %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))); - addr = stringf("(|%s_m:W%dA %s| state)", get_id(module), i, get_id(cell)); + if (has_async_wr) + hier.push_back(stringf(" (= %s (|%s| state)) ; %s\n", expr_d.c_str(), final_memstate.c_str(), get_id(mem->memid))); - decls.push_back(stringf("(define-fun |%s_m:W%dD %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n", - get_id(module), i, get_id(cell), get_id(module), width, data.c_str(), log_signal(data_sig))); - data = stringf("(|%s_m:W%dD %s| state)", get_id(module), i, get_id(cell)); + Const init_data = mem->get_init_data(); - decls.push_back(stringf("(define-fun |%s_m:W%dM %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n", - get_id(module), i, get_id(cell), get_id(module), width, mask.c_str(), log_signal(mask_sig))); - mask = stringf("(|%s_m:W%dM %s| state)", get_id(module), i, get_id(cell)); + for (int i = 0; i < mem->size; i++) + { + if (i*mem->width >= GetSize(init_data)) + break; - data = stringf("(bvor (bvand %s %s) (bvand (select (|%s#%d#%d| state) %s) (bvnot %s)))", - data.c_str(), mask.c_str(), get_id(module), arrayid, i, addr.c_str(), mask.c_str()); + Const initword = init_data.extract(i*mem->width, mem->width, State::Sx); + Const initmask = initword; + bool gen_init_constr = false; - 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", - 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))); + for (int k = 0; k < GetSize(initword); k++) { + if (initword[k] == State::S0 || initword[k] == State::S1) { + gen_init_constr = true; + initmask[k] = State::S1; + } else { + initmask[k] = State::S0; + initword[k] = State::S0; } } - 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))); - ex_state_eq.push_back(stringf("(= (|%s#%d#0| state) (|%s#%d#0| other_state))", get_id(module), arrayid, get_id(module), arrayid)); - - if (async_read) - hier.push_back(stringf(" (= %s (|%s| state)) ; %s\n", expr_d.c_str(), final_memstate.c_str(), get_id(cell))); - - Const init_data = cell->getParam(ID::INIT); - int memsize = cell->getParam(ID::SIZE).as_int(); - - for (int i = 0; i < memsize; i++) + if (gen_init_constr) { - if (i*width >= GetSize(init_data)) - break; - - Const initword = init_data.extract(i*width, width, State::Sx); - Const initmask = initword; - bool gen_init_constr = false; - - for (int k = 0; k < GetSize(initword); k++) { - if (initword[k] == State::S0 || initword[k] == State::S1) { - gen_init_constr = true; - initmask[k] = State::S1; - } else { - initmask[k] = State::S0; - initword[k] = State::S0; - } - } - - if (gen_init_constr) - { - if (statebv) - /* FIXME */; - else - init_list.push_back(stringf("(= (bvand (select (|%s#%d#0| state) #b%s) #b%s) #b%s) ; %s[%d]", - get_id(module), arrayid, Const(i, abits).as_string().c_str(), - initmask.as_string().c_str(), initword.as_string().c_str(), get_id(cell), i)); - } + if (statebv) + /* FIXME */; + else + init_list.push_back(stringf("(= (bvand (select (|%s#%d#0| state) #b%s) #b%s) #b%s) ; %s[%d]", + get_id(module), arrayid, Const(i, abits).as_string().c_str(), + initmask.as_string().c_str(), initword.as_string().c_str(), get_id(mem->memid), i)); } } } @@ -1392,7 +1461,7 @@ struct Smt2Backend : public Backend { log(" the given option as a `(set-option ...)` command in the SMT-LIBv2.\n"); log("\n"); log("[1] For more information on SMT-LIBv2 visit http://smt-lib.org/ or read David\n"); - log("R. Cok's tutorial: http://www.grammatech.com/resources/smt/SMTLIBTutorial.pdf\n"); + log("R. Cok's tutorial: https://smtlib.github.io/jSMTLIB/SMTLIBTutorial.pdf\n"); log("\n"); log("---------------------------------------------------------------------------\n"); log("\n"); @@ -1575,7 +1644,7 @@ struct Smt2Backend : public Backend { for (auto module : sorted_modules) { - if (module->get_blackbox_attribute() || module->has_memories_warn() || module->has_processes_warn()) + if (module->get_blackbox_attribute() || module->has_processes_warn()) continue; log("Creating SMT-LIBv2 representation of module %s.\n", log_id(module)); diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index 69dab5590..da5a7f57e 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -817,6 +817,24 @@ def write_vcd_trace(steps_start, steps_stop, index): vcd.set_time(steps_stop) +def char_ok_in_verilog(c,i): + if ('A' <= c <= 'Z'): return True + if ('a' <= c <= 'z'): return True + if ('0' <= c <= '9' and i>0): return True + if (c == '_'): return True + if (c == '$'): return True + return False + +def escape_identifier(identifier): + if type(identifier) is list: + return map(escape_identifier, identifier) + if "." in identifier: + return ".".join(escape_identifier(identifier.split("."))) + if (all(char_ok_in_verilog(identifier[i],i) for i in range(0, len(identifier)))): + return identifier + return "\\"+identifier+" " + + def write_vlogtb_trace(steps_start, steps_stop, index): filename = vlogtbfile.replace("%", index) @@ -858,12 +876,12 @@ def write_vlogtb_trace(steps_start, steps_stop, index): for name, width in primary_inputs: if name in clock_inputs: - print(" wire [%d:0] PI_%s = clock;" % (width-1, name), file=f) + print(" wire [%d:0] %s = clock;" % (width-1, escape_identifier("PI_"+name)), file=f) else: - print(" reg [%d:0] PI_%s;" % (width-1, name), file=f) + print(" reg [%d:0] %s;" % (width-1, escape_identifier("PI_"+name)), file=f) - print(" %s UUT (" % vlogtb_topmod, file=f) - print(",\n".join(" .{name}(PI_{name})".format(name=name) for name, _ in primary_inputs), file=f) + print(" %s UUT (" % escape_identifier(vlogtb_topmod), file=f) + print(",\n".join(" .%s(%s)" % (escape_identifier(name), escape_identifier("PI_"+name)) for name, _ in primary_inputs), file=f) print(" );", file=f) print("`ifndef VERILATOR", file=f) @@ -893,14 +911,14 @@ def write_vlogtb_trace(steps_start, steps_stop, index): 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) + print(" %sUUT.%s = %d'b%s;" % ("// " if hidden_net else "", ".".join(escape_identifier(reg)), len(val), val), file=f) anyconsts = sorted(smt.hieranyconsts(vlogtb_topmod)) for info in anyconsts: if info[3] is not None: modstate = smt.net_expr(vlogtb_topmod, vlogtb_state.replace("@@step_idx@@", str(steps_start)), info[0]) value = smt.bv2bin(smt.get("(|%s| %s)" % (info[1], modstate))) - print(" UUT.%s = %d'b%s;" % (".".join(info[0] + [info[3]]), len(value), value), file=f); + print(" UUT.%s = %d'b%s;" % (".".join(escape_identifier(info[0] + [info[3]])), len(value), value), file=f); mems = sorted(smt.hiermems(vlogtb_topmod)) for mempath in mems: @@ -924,7 +942,7 @@ def write_vlogtb_trace(steps_start, steps_stop, index): addr_data[addr] = data for addr, data in addr_data.items(): - print(" UUT.%s[%d'b%s] = %d'b%s;" % (".".join(mempath), len(addr), addr, len(data), data), file=f) + print(" UUT.%s[%d'b%s] = %d'b%s;" % (".".join(escape_identifier(mempath)), len(addr), addr, len(data), data), file=f) print("", file=f) anyseqs = sorted(smt.hieranyseqs(vlogtb_topmod)) @@ -940,18 +958,18 @@ def write_vlogtb_trace(steps_start, steps_stop, index): for name, val in zip(pi_names, pi_values): if i > 0: - print(" PI_%s <= %d'b%s;" % (".".join(name), len(val), val), file=f) + print(" %s <= %d'b%s;" % (escape_identifier("PI_"+".".join(name)), len(val), val), file=f) else: - print(" PI_%s = %d'b%s;" % (".".join(name), len(val), val), file=f) + print(" %s = %d'b%s;" % (escape_identifier("PI_"+".".join(name)), len(val), val), file=f) for info in anyseqs: if info[3] is not None: modstate = smt.net_expr(vlogtb_topmod, vlogtb_state.replace("@@step_idx@@", str(i)), info[0]) value = smt.bv2bin(smt.get("(|%s| %s)" % (info[1], modstate))) if i > 0: - print(" UUT.%s <= %d'b%s;" % (".".join(info[0] + [info[3]]), len(value), value), file=f); + print(" UUT.%s <= %d'b%s;" % (".".join(escape_identifier(info[0] + [info[3]])), len(value), value), file=f); else: - print(" UUT.%s = %d'b%s;" % (".".join(info[0] + [info[3]]), len(value), value), file=f); + print(" UUT.%s = %d'b%s;" % (".".join(escape_identifier(info[0] + [info[3]])), len(value), value), file=f); if i > 0: print(" end", file=f) diff --git a/backends/smv/.gitignore b/backends/smv/.gitignore new file mode 100644 index 000000000..d23d492d7 --- /dev/null +++ b/backends/smv/.gitignore @@ -0,0 +1 @@ +/test_cells.tmp/ diff --git a/backends/verilog/verilog_backend.cc b/backends/verilog/verilog_backend.cc index 71f71554b..9523f4a52 100644 --- a/backends/verilog/verilog_backend.cc +++ b/backends/verilog/verilog_backend.cc @@ -25,6 +25,8 @@ #include "kernel/celltypes.h" #include "kernel/log.h" #include "kernel/sigtools.h" +#include "kernel/ff.h" +#include "kernel/mem.h" #include <string> #include <sstream> #include <set> @@ -36,7 +38,7 @@ PRIVATE_NAMESPACE_BEGIN bool verbose, norename, noattr, attr2comment, noexpr, nodec, nohex, nostr, extmem, defparam, decimal, siminit, systemverilog; int auto_name_counter, auto_name_offset, auto_name_digits, extmem_counter; std::map<RTLIL::IdString, int> auto_name_map; -std::set<RTLIL::IdString> reg_wires, reg_ct; +std::set<RTLIL::IdString> reg_wires; std::string auto_prefix, extmem_prefix; RTLIL::Module *active_module; @@ -433,10 +435,250 @@ void dump_wire(std::ostream &f, std::string indent, RTLIL::Wire *wire) #endif } -void dump_memory(std::ostream &f, std::string indent, RTLIL::Memory *memory) +void dump_memory(std::ostream &f, std::string indent, Mem &mem) { - dump_attributes(f, indent, memory->attributes); - f << stringf("%s" "reg [%d:0] %s [%d:%d];\n", indent.c_str(), memory->width-1, id(memory->name).c_str(), memory->size+memory->start_offset-1, memory->start_offset); + std::string mem_id = id(mem.memid); + + dump_attributes(f, indent, mem.attributes); + f << stringf("%s" "reg [%d:0] %s [%d:%d];\n", indent.c_str(), mem.width-1, mem_id.c_str(), mem.size+mem.start_offset-1, mem.start_offset); + + // for memory block make something like: + // reg [7:0] memid [3:0]; + // initial begin + // memid[0] = ... + // end + if (!mem.inits.empty()) + { + if (extmem) + { + std::string extmem_filename = stringf("%s-%d.mem", extmem_prefix.c_str(), extmem_counter++); + + std::string extmem_filename_esc; + for (auto c : extmem_filename) + { + if (c == '\n') + extmem_filename_esc += "\\n"; + else if (c == '\t') + extmem_filename_esc += "\\t"; + else if (c < 32) + extmem_filename_esc += stringf("\\%03o", c); + else if (c == '"') + extmem_filename_esc += "\\\""; + else if (c == '\\') + extmem_filename_esc += "\\\\"; + else + extmem_filename_esc += c; + } + f << stringf("%s" "initial $readmemb(\"%s\", %s);\n", indent.c_str(), extmem_filename_esc.c_str(), mem_id.c_str()); + + std::ofstream extmem_f(extmem_filename, std::ofstream::trunc); + if (extmem_f.fail()) + log_error("Can't open file `%s' for writing: %s\n", extmem_filename.c_str(), strerror(errno)); + else + { + Const data = mem.get_init_data(); + for (int i=0; i<mem.size; i++) + { + RTLIL::Const element = data.extract(i*mem.width, mem.width); + for (int j=0; j<element.size(); j++) + { + switch (element[element.size()-j-1]) + { + case State::S0: extmem_f << '0'; break; + case State::S1: extmem_f << '1'; break; + case State::Sx: extmem_f << 'x'; break; + case State::Sz: extmem_f << 'z'; break; + case State::Sa: extmem_f << '_'; break; + case State::Sm: log_error("Found marker state in final netlist."); + } + } + extmem_f << '\n'; + } + } + } + else + { + f << stringf("%s" "initial begin\n", indent.c_str()); + for (auto &init : mem.inits) { + int words = GetSize(init.data) / mem.width; + int start = init.addr.as_int(); + for (int i=0; i<words; i++) + { + f << stringf("%s" " %s[%d] = ", indent.c_str(), mem_id.c_str(), i + start); + dump_const(f, init.data.extract(i*mem.width, mem.width)); + f << stringf(";\n"); + } + } + f << stringf("%s" "end\n", indent.c_str()); + } + } + + // create a map : "edge clk" -> expressions within that clock domain + dict<std::string, std::vector<std::string>> clk_to_lof_body; + clk_to_lof_body[""] = std::vector<std::string>(); + std::string clk_domain_str; + // create a list of reg declarations + std::vector<std::string> lof_reg_declarations; + + // read ports + for (auto &port : mem.rd_ports) + { + if (port.clk_enable) + { + { + std::ostringstream os; + dump_sigspec(os, port.clk); + clk_domain_str = stringf("%sedge %s", port.clk_polarity ? "pos" : "neg", os.str().c_str()); + if( clk_to_lof_body.count(clk_domain_str) == 0 ) + clk_to_lof_body[clk_domain_str] = std::vector<std::string>(); + } + if (!port.transparent) + { + // for clocked read ports make something like: + // reg [..] temp_id; + // always @(posedge clk) + // 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", port.data.size() - 1, temp_id.c_str()) ); + { + std::ostringstream os; + if (port.en != RTLIL::SigBit(true)) + { + os << stringf("if ("); + dump_sigspec(os, port.en); + os << stringf(") "); + } + os << stringf("%s <= %s[", temp_id.c_str(), mem_id.c_str()); + dump_sigspec(os, port.addr); + os << stringf("];\n"); + clk_to_lof_body[clk_domain_str].push_back(os.str()); + } + { + std::ostringstream os; + dump_sigspec(os, port.data); + std::string line = stringf("assign %s = %s;\n", os.str().c_str(), temp_id.c_str()); + clk_to_lof_body[""].push_back(line); + } + } + else + { + // for rd-transparent read-ports make something like: + // reg [..] temp_id; + // always @(posedge clk) + // temp_id <= r_addr; + // assign r_data = array_reg[temp_id]; + std::string temp_id = next_auto_id(); + lof_reg_declarations.push_back( stringf("reg [%d:0] %s;\n", port.addr.size() - 1, temp_id.c_str()) ); + { + std::ostringstream os; + dump_sigspec(os, port.addr); + std::string line = stringf("%s <= %s;\n", temp_id.c_str(), os.str().c_str()); + clk_to_lof_body[clk_domain_str].push_back(line); + } + { + std::ostringstream os; + dump_sigspec(os, port.data); + std::string line = stringf("assign %s = %s[%s];\n", os.str().c_str(), mem_id.c_str(), temp_id.c_str()); + clk_to_lof_body[""].push_back(line); + } + } + } else { + // for non-clocked read-ports make something like: + // assign r_data = array_reg[r_addr]; + std::ostringstream os, os2; + dump_sigspec(os, port.data); + dump_sigspec(os2, port.addr); + std::string line = stringf("assign %s = %s[%s];\n", os.str().c_str(), mem_id.c_str(), os2.str().c_str()); + clk_to_lof_body[""].push_back(line); + } + } + + // write ports + for (auto &port : mem.wr_ports) + { + { + std::ostringstream os; + dump_sigspec(os, port.clk); + clk_domain_str = stringf("%sedge %s", port.clk_polarity ? "pos" : "neg", os.str().c_str()); + if( clk_to_lof_body.count(clk_domain_str) == 0 ) + clk_to_lof_body[clk_domain_str] = std::vector<std::string>(); + } + // make something like: + // always @(posedge clk) + // if (wr_en_bit) memid[w_addr][??] <= w_data[??]; + // ... + for (int i = 0; i < GetSize(port.en); i++) + { + int start_i = i, width = 1; + SigBit wen_bit = port.en[i]; + + while (i+1 < GetSize(port.en) && active_sigmap(port.en[i+1]) == active_sigmap(wen_bit)) + i++, width++; + + if (wen_bit == State::S0) + continue; + + std::ostringstream os; + if (wen_bit != State::S1) + { + os << stringf("if ("); + dump_sigspec(os, wen_bit); + os << stringf(") "); + } + os << stringf("%s[", mem_id.c_str()); + dump_sigspec(os, port.addr); + if (width == GetSize(port.en)) + os << stringf("] <= "); + else + os << stringf("][%d:%d] <= ", i, start_i); + dump_sigspec(os, port.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: + // reg [..] _3_; + // always @(posedge CLK2) begin + // _3_ <= memory[D1ADDR]; + // if (A1EN) + // memory[A1ADDR] <= A1DATA; + // if (A2EN) + // memory[A2ADDR] <= A2DATA; + // ... + // end + // always @(negedge CLK1) begin + // if (C1EN) + // memory[C1ADDR] <= C1DATA; + // end + // ... + // assign D1DATA = _3_; + // assign D2DATA <= memory[D2ADDR]; + + // the reg ... definitions + for(auto ® : lof_reg_declarations) + { + f << stringf("%s" "%s", indent.c_str(), reg.c_str()); + } + // the block of expressions by clock domain + for(auto &pair : clk_to_lof_body) + { + std::string clk_domain = pair.first; + std::vector<std::string> lof_lines = pair.second; + if( clk_domain != "") + { + f << stringf("%s" "always%s @(%s) begin\n", indent.c_str(), systemverilog ? "_ff" : "", clk_domain.c_str()); + for(auto &line : lof_lines) + f << stringf("%s%s" "%s", indent.c_str(), indent.c_str(), line.c_str()); + f << stringf("%s" "end\n", indent.c_str()); + } + else + { + // the non-clocked assignments + for(auto &line : lof_lines) + f << stringf("%s" "%s", indent.c_str(), line.c_str()); + } + } } void dump_cell_expr_port(std::ostream &f, RTLIL::Cell *cell, std::string port, bool gen_signed = true) @@ -451,7 +693,7 @@ void dump_cell_expr_port(std::ostream &f, RTLIL::Cell *cell, std::string port, b std::string cellname(RTLIL::Cell *cell) { - if (!norename && cell->name[0] == '$' && reg_ct.count(cell->type) && cell->hasPort(ID::Q)) + if (!norename && cell->name[0] == '$' && RTLIL::builtin_ff_cell_types().count(cell->type) && cell->hasPort(ID::Q) && !cell->type.in(ID($ff), ID($_FF_))) { RTLIL::SigSpec sig = cell->getPort(ID::Q); if (GetSize(sig) != 1 || sig.is_fully_const()) @@ -605,93 +847,6 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell) return true; } - if (cell->type.begins_with("$_DFF_")) - { - std::string reg_name = cellname(cell); - bool out_is_reg_wire = is_reg_wire(cell->getPort(ID::Q), reg_name); - - if (!out_is_reg_wire) { - f << stringf("%s" "reg %s", indent.c_str(), reg_name.c_str()); - dump_reg_init(f, cell->getPort(ID::Q)); - f << ";\n"; - } - - dump_attributes(f, indent, cell->attributes); - f << stringf("%s" "always%s @(%sedge ", indent.c_str(), systemverilog ? "_ff" : "", cell->type[6] == 'P' ? "pos" : "neg"); - dump_sigspec(f, cell->getPort(ID::C)); - if (cell->type[7] != '_') { - f << stringf(" or %sedge ", cell->type[7] == 'P' ? "pos" : "neg"); - dump_sigspec(f, cell->getPort(ID::R)); - } - f << stringf(")\n"); - - if (cell->type[7] != '_') { - f << stringf("%s" " if (%s", indent.c_str(), cell->type[7] == 'P' ? "" : "!"); - dump_sigspec(f, cell->getPort(ID::R)); - f << stringf(")\n"); - f << stringf("%s" " %s <= %c;\n", indent.c_str(), reg_name.c_str(), cell->type[8]); - f << stringf("%s" " else\n", indent.c_str()); - } - - f << stringf("%s" " %s <= ", indent.c_str(), reg_name.c_str()); - dump_cell_expr_port(f, cell, "D", false); - f << stringf(";\n"); - - if (!out_is_reg_wire) { - f << stringf("%s" "assign ", indent.c_str()); - dump_sigspec(f, cell->getPort(ID::Q)); - f << stringf(" = %s;\n", reg_name.c_str()); - } - - return true; - } - - if (cell->type.begins_with("$_DFFSR_")) - { - char pol_c = cell->type[8], pol_s = cell->type[9], pol_r = cell->type[10]; - - std::string reg_name = cellname(cell); - bool out_is_reg_wire = is_reg_wire(cell->getPort(ID::Q), reg_name); - - if (!out_is_reg_wire) { - f << stringf("%s" "reg %s", indent.c_str(), reg_name.c_str()); - dump_reg_init(f, cell->getPort(ID::Q)); - f << ";\n"; - } - - dump_attributes(f, indent, cell->attributes); - f << stringf("%s" "always%s @(%sedge ", indent.c_str(), systemverilog ? "_ff" : "", pol_c == 'P' ? "pos" : "neg"); - dump_sigspec(f, cell->getPort(ID::C)); - f << stringf(" or %sedge ", pol_s == 'P' ? "pos" : "neg"); - dump_sigspec(f, cell->getPort(ID::S)); - f << stringf(" or %sedge ", pol_r == 'P' ? "pos" : "neg"); - dump_sigspec(f, cell->getPort(ID::R)); - f << stringf(")\n"); - - f << stringf("%s" " if (%s", indent.c_str(), pol_r == 'P' ? "" : "!"); - dump_sigspec(f, cell->getPort(ID::R)); - f << stringf(")\n"); - f << stringf("%s" " %s <= 0;\n", indent.c_str(), reg_name.c_str()); - - f << stringf("%s" " else if (%s", indent.c_str(), pol_s == 'P' ? "" : "!"); - dump_sigspec(f, cell->getPort(ID::S)); - f << stringf(")\n"); - f << stringf("%s" " %s <= 1;\n", indent.c_str(), reg_name.c_str()); - - f << stringf("%s" " else\n", indent.c_str()); - f << stringf("%s" " %s <= ", indent.c_str(), reg_name.c_str()); - dump_cell_expr_port(f, cell, "D", false); - f << stringf(";\n"); - - if (!out_is_reg_wire) { - f << stringf("%s" "assign ", indent.c_str()); - dump_sigspec(f, cell->getPort(ID::Q)); - f << stringf(" = %s;\n", reg_name.c_str()); - } - - return true; - } - #define HANDLE_UNIOP(_type, _operator) \ if (cell->type ==_type) { dump_cell_expr_uniop(f, indent, cell, _operator); return true; } #define HANDLE_BINOP(_type, _operator) \ @@ -836,21 +991,19 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell) f << stringf(" = "); if (cell->getParam(ID::B_SIGNED).as_bool()) { - f << stringf("$signed("); - dump_sigspec(f, cell->getPort(ID::B)); - f << stringf(")"); + dump_cell_expr_port(f, cell, "B", true); f << stringf(" < 0 ? "); - dump_sigspec(f, cell->getPort(ID::A)); + dump_cell_expr_port(f, cell, "A", true); f << stringf(" << - "); dump_sigspec(f, cell->getPort(ID::B)); f << stringf(" : "); - dump_sigspec(f, cell->getPort(ID::A)); + dump_cell_expr_port(f, cell, "A", true); f << stringf(" >> "); dump_sigspec(f, cell->getPort(ID::B)); } else { - dump_sigspec(f, cell->getPort(ID::A)); + dump_cell_expr_port(f, cell, "A", true); f << stringf(" >> "); dump_sigspec(f, cell->getPort(ID::B)); } @@ -986,423 +1139,198 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell) return true; } - if (cell->type == ID($dffsr)) + if (RTLIL::builtin_ff_cell_types().count(cell->type)) { - SigSpec sig_clk = cell->getPort(ID::CLK); - SigSpec sig_set = cell->getPort(ID::SET); - SigSpec sig_clr = cell->getPort(ID::CLR); - SigSpec sig_d = cell->getPort(ID::D); - SigSpec sig_q = cell->getPort(ID::Q); + FfData ff(nullptr, cell); - int width = cell->parameters[ID::WIDTH].as_int(); - bool pol_clk = cell->parameters[ID::CLK_POLARITY].as_bool(); - bool pol_set = cell->parameters[ID::SET_POLARITY].as_bool(); - bool pol_clr = cell->parameters[ID::CLR_POLARITY].as_bool(); + // $ff / $_FF_ cell: not supported. + if (ff.has_d && !ff.has_clk && !ff.has_en) + return false; std::string reg_name = cellname(cell); - bool out_is_reg_wire = is_reg_wire(sig_q, reg_name); + bool out_is_reg_wire = is_reg_wire(ff.sig_q, reg_name); if (!out_is_reg_wire) { - f << stringf("%s" "reg [%d:0] %s", indent.c_str(), width-1, reg_name.c_str()); - dump_reg_init(f, sig_q); - f << ";\n"; - } - - for (int i = 0; i < width; i++) { - f << stringf("%s" "always%s @(%sedge ", indent.c_str(), systemverilog ? "_ff" : "", pol_clk ? "pos" : "neg"); - dump_sigspec(f, sig_clk); - f << stringf(", %sedge ", pol_set ? "pos" : "neg"); - dump_sigspec(f, sig_set); - f << stringf(", %sedge ", pol_clr ? "pos" : "neg"); - dump_sigspec(f, sig_clr); - f << stringf(")\n"); - - f << stringf("%s" " if (%s", indent.c_str(), pol_clr ? "" : "!"); - dump_sigspec(f, sig_clr); - f << stringf(") %s[%d] <= 1'b0;\n", reg_name.c_str(), i); - - f << stringf("%s" " else if (%s", indent.c_str(), pol_set ? "" : "!"); - dump_sigspec(f, sig_set); - f << stringf(") %s[%d] <= 1'b1;\n", reg_name.c_str(), i); - - f << stringf("%s" " else %s[%d] <= ", indent.c_str(), reg_name.c_str(), i); - dump_sigspec(f, sig_d[i]); - f << stringf(";\n"); - } - - if (!out_is_reg_wire) { - f << stringf("%s" "assign ", indent.c_str()); - dump_sigspec(f, sig_q); - f << stringf(" = %s;\n", reg_name.c_str()); - } - - return true; - } - - if (cell->type.in(ID($dff), ID($adff), ID($dffe))) - { - RTLIL::SigSpec sig_clk, sig_arst, sig_en, val_arst; - bool pol_clk, pol_arst = false, pol_en = false; - - sig_clk = cell->getPort(ID::CLK); - pol_clk = cell->parameters[ID::CLK_POLARITY].as_bool(); - - if (cell->type == ID($adff)) { - sig_arst = cell->getPort(ID::ARST); - pol_arst = cell->parameters[ID::ARST_POLARITY].as_bool(); - val_arst = RTLIL::SigSpec(cell->parameters[ID::ARST_VALUE]); - } - - if (cell->type == ID($dffe)) { - sig_en = cell->getPort(ID::EN); - pol_en = cell->parameters[ID::EN_POLARITY].as_bool(); - } - - std::string reg_name = cellname(cell); - bool out_is_reg_wire = is_reg_wire(cell->getPort(ID::Q), reg_name); - - if (!out_is_reg_wire) { - f << stringf("%s" "reg [%d:0] %s", indent.c_str(), cell->parameters[ID::WIDTH].as_int()-1, reg_name.c_str()); - dump_reg_init(f, cell->getPort(ID::Q)); - f << ";\n"; - } - - f << stringf("%s" "always%s @(%sedge ", indent.c_str(), systemverilog ? "_ff" : "", pol_clk ? "pos" : "neg"); - dump_sigspec(f, sig_clk); - if (cell->type == ID($adff)) { - f << stringf(" or %sedge ", pol_arst ? "pos" : "neg"); - dump_sigspec(f, sig_arst); - } - f << stringf(")\n"); - - if (cell->type == ID($adff)) { - f << stringf("%s" " if (%s", indent.c_str(), pol_arst ? "" : "!"); - dump_sigspec(f, sig_arst); - f << stringf(")\n"); - f << stringf("%s" " %s <= ", indent.c_str(), reg_name.c_str()); - dump_sigspec(f, val_arst); - f << stringf(";\n"); - f << stringf("%s" " else\n", indent.c_str()); - } - - if (cell->type == ID($dffe)) { - f << stringf("%s" " if (%s", indent.c_str(), pol_en ? "" : "!"); - dump_sigspec(f, sig_en); - f << stringf(")\n"); - } - - f << stringf("%s" " %s <= ", indent.c_str(), reg_name.c_str()); - dump_cell_expr_port(f, cell, "D", false); - f << stringf(";\n"); - - if (!out_is_reg_wire) { - f << stringf("%s" "assign ", indent.c_str()); - dump_sigspec(f, cell->getPort(ID::Q)); - f << stringf(" = %s;\n", reg_name.c_str()); - } - - return true; - } - - if (cell->type == ID($dlatch)) - { - RTLIL::SigSpec sig_en; - bool pol_en = false; - - sig_en = cell->getPort(ID::EN); - pol_en = cell->parameters[ID::EN_POLARITY].as_bool(); - - std::string reg_name = cellname(cell); - bool out_is_reg_wire = is_reg_wire(cell->getPort(ID::Q), reg_name); - - if (!out_is_reg_wire) { - f << stringf("%s" "reg [%d:0] %s", indent.c_str(), cell->parameters[ID::WIDTH].as_int()-1, reg_name.c_str()); - dump_reg_init(f, cell->getPort(ID::Q)); + if (ff.width == 1) + f << stringf("%s" "reg %s", indent.c_str(), reg_name.c_str()); + else + f << stringf("%s" "reg [%d:0] %s", indent.c_str(), ff.width-1, reg_name.c_str()); + dump_reg_init(f, ff.sig_q); f << ";\n"; } - f << stringf("%s" "always%s\n", indent.c_str(), systemverilog ? "_latch" : " @*"); + // If the FF has CLR/SET inputs, emit every bit slice separately. + int chunks = ff.has_sr ? ff.width : 1; + bool chunky = ff.has_sr && ff.width != 1; - f << stringf("%s" " if (%s", indent.c_str(), pol_en ? "" : "!"); - dump_sigspec(f, sig_en); - f << stringf(")\n"); - - f << stringf("%s" " %s = ", indent.c_str(), reg_name.c_str()); - dump_cell_expr_port(f, cell, "D", false); - f << stringf(";\n"); - - if (!out_is_reg_wire) { - f << stringf("%s" "assign ", indent.c_str()); - dump_sigspec(f, cell->getPort(ID::Q)); - f << stringf(" = %s;\n", reg_name.c_str()); - } - - return true; - } - - if (cell->type == ID($mem)) - { - RTLIL::IdString memid = cell->parameters[ID::MEMID].decode_string(); - std::string mem_id = id(cell->parameters[ID::MEMID].decode_string()); - int abits = cell->parameters[ID::ABITS].as_int(); - int size = cell->parameters[ID::SIZE].as_int(); - int offset = cell->parameters[ID::OFFSET].as_int(); - int width = cell->parameters[ID::WIDTH].as_int(); - bool use_init = !(RTLIL::SigSpec(cell->parameters[ID::INIT]).is_fully_undef()); - - // for memory block make something like: - // reg [7:0] memid [3:0]; - // initial begin - // memid[0] = ... - // end - dump_attributes(f, indent.c_str(), cell->attributes); - f << stringf("%s" "reg [%d:%d] %s [%d:%d];\n", indent.c_str(), width-1, 0, mem_id.c_str(), size+offset-1, offset); - if (use_init) + for (int i = 0; i < chunks; i++) { - if (extmem) - { - std::string extmem_filename = stringf("%s-%d.mem", extmem_prefix.c_str(), extmem_counter++); - - std::string extmem_filename_esc; - for (auto c : extmem_filename) + SigSpec sig_d; + Const val_arst, val_srst; + std::string reg_bit_name, sig_set_name, sig_clr_name, sig_arst_name; + if (chunky) { + reg_bit_name = stringf("%s[%d]", reg_name.c_str(), i); + if (ff.has_d) + sig_d = ff.sig_d[i]; + } else { + reg_bit_name = reg_name; + if (ff.has_d) + sig_d = ff.sig_d; + } + if (ff.has_arst) + val_arst = chunky ? ff.val_arst[i] : ff.val_arst; + if (ff.has_srst) + val_srst = chunky ? ff.val_srst[i] : ff.val_srst; + + // If there are constants in the sensitivity list, replace them with an intermediate wire + if (ff.has_sr) { + if (ff.sig_set[i].wire == NULL) { - if (c == '\n') - extmem_filename_esc += "\\n"; - else if (c == '\t') - extmem_filename_esc += "\\t"; - else if (c < 32) - extmem_filename_esc += stringf("\\%03o", c); - else if (c == '"') - extmem_filename_esc += "\\\""; - else if (c == '\\') - extmem_filename_esc += "\\\\"; - else - extmem_filename_esc += c; + sig_set_name = next_auto_id(); + f << stringf("%s" "wire %s = ", indent.c_str(), sig_set_name.c_str()); + dump_const(f, ff.sig_set[i].data); + f << stringf(";\n"); } - f << stringf("%s" "initial $readmemb(\"%s\", %s);\n", indent.c_str(), extmem_filename_esc.c_str(), mem_id.c_str()); - - std::ofstream extmem_f(extmem_filename, std::ofstream::trunc); - if (extmem_f.fail()) - log_error("Can't open file `%s' for writing: %s\n", extmem_filename.c_str(), strerror(errno)); - else + if (ff.sig_clr[i].wire == NULL) { - for (int i=0; i<size; i++) - { - RTLIL::Const element = cell->parameters[ID::INIT].extract(i*width, width); - for (int j=0; j<element.size(); j++) - { - switch (element[element.size()-j-1]) - { - case State::S0: extmem_f << '0'; break; - case State::S1: extmem_f << '1'; break; - case State::Sx: extmem_f << 'x'; break; - case State::Sz: extmem_f << 'z'; break; - case State::Sa: extmem_f << '_'; break; - case State::Sm: log_error("Found marker state in final netlist."); - } - } - extmem_f << '\n'; - } + sig_clr_name = next_auto_id(); + f << stringf("%s" "wire %s = ", indent.c_str(), sig_clr_name.c_str()); + dump_const(f, ff.sig_clr[i].data); + f << stringf(";\n"); } - - } - else - { - f << stringf("%s" "initial begin\n", indent.c_str()); - for (int i=0; i<size; i++) + } else if (ff.has_arst) { + if (ff.sig_arst[i].wire == NULL) { - f << stringf("%s" " %s[%d] = ", indent.c_str(), mem_id.c_str(), i); - dump_const(f, cell->parameters[ID::INIT].extract(i*width, width)); + sig_arst_name = next_auto_id(); + f << stringf("%s" "wire %s = ", indent.c_str(), sig_arst_name.c_str()); + dump_const(f, ff.sig_arst[i].data); f << stringf(";\n"); } - f << stringf("%s" "end\n", indent.c_str()); } - } - // create a map : "edge clk" -> expressions within that clock domain - dict<std::string, std::vector<std::string>> clk_to_lof_body; - clk_to_lof_body[""] = std::vector<std::string>(); - std::string clk_domain_str; - // create a list of reg declarations - std::vector<std::string> lof_reg_declarations; - - int nread_ports = cell->parameters[ID::RD_PORTS].as_int(); - 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(ID::RD_CLK).extract(i); - sig_rd_en = cell->getPort(ID::RD_EN).extract(i); - sig_rd_data = cell->getPort(ID::RD_DATA).extract(i*width, width); - sig_rd_addr = cell->getPort(ID::RD_ADDR).extract(i*abits, abits); - use_rd_clk = cell->parameters[ID::RD_CLK_ENABLE].extract(i).as_bool(); - rd_clk_posedge = cell->parameters[ID::RD_CLK_POLARITY].extract(i).as_bool(); - rd_transparent = cell->parameters[ID::RD_TRANSPARENT].extract(i).as_bool(); - if (use_rd_clk) + dump_attributes(f, indent, cell->attributes); + if (ff.has_clk) { - { - std::ostringstream os; - dump_sigspec(os, sig_rd_clk); - clk_domain_str = stringf("%sedge %s", rd_clk_posedge ? "pos" : "neg", os.str().c_str()); - if( clk_to_lof_body.count(clk_domain_str) == 0 ) - clk_to_lof_body[clk_domain_str] = std::vector<std::string>(); + // FFs. + f << stringf("%s" "always%s @(%sedge ", indent.c_str(), systemverilog ? "_ff" : "", ff.pol_clk ? "pos" : "neg"); + dump_sigspec(f, ff.sig_clk); + if (ff.has_sr) { + f << stringf(", %sedge ", ff.pol_set ? "pos" : "neg"); + if (ff.sig_set[i].wire == NULL) + f << stringf("%s", sig_set_name.c_str()); + else + dump_sigspec(f, ff.sig_set[i]); + + f << stringf(", %sedge ", ff.pol_clr ? "pos" : "neg"); + if (ff.sig_clr[i].wire == NULL) + f << stringf("%s", sig_clr_name.c_str()); + else + dump_sigspec(f, ff.sig_clr[i]); + + } else if (ff.has_arst) { + f << stringf(", %sedge ", ff.pol_arst ? "pos" : "neg"); + if (ff.sig_arst[i].wire == NULL) + f << stringf("%s", sig_arst_name.c_str()); + else + dump_sigspec(f, ff.sig_arst); } - if (!rd_transparent) - { - // for clocked read ports make something like: - // reg [..] temp_id; - // always @(posedge clk) - // 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); - os << stringf("];\n"); - clk_to_lof_body[clk_domain_str].push_back(os.str()); - } - { - std::ostringstream os; - dump_sigspec(os, sig_rd_data); - std::string line = stringf("assign %s = %s;\n", os.str().c_str(), temp_id.c_str()); - clk_to_lof_body[""].push_back(line); - } + f << stringf(")\n"); + + f << stringf("%s" " ", indent.c_str()); + if (ff.has_sr) { + f << stringf("if (%s", ff.pol_clr ? "" : "!"); + if (ff.sig_clr[i].wire == NULL) + f << stringf("%s", sig_clr_name.c_str()); + else + dump_sigspec(f, ff.sig_clr[i]); + f << stringf(") %s <= 1'b0;\n", reg_bit_name.c_str()); + f << stringf("%s" " else if (%s", indent.c_str(), ff.pol_set ? "" : "!"); + if (ff.sig_set[i].wire == NULL) + f << stringf("%s", sig_set_name.c_str()); + else + dump_sigspec(f, ff.sig_set[i]); + f << stringf(") %s <= 1'b1;\n", reg_bit_name.c_str()); + f << stringf("%s" " else ", indent.c_str()); + } else if (ff.has_arst) { + f << stringf("if (%s", ff.pol_arst ? "" : "!"); + if (ff.sig_arst[i].wire == NULL) + f << stringf("%s", sig_arst_name.c_str()); + else + dump_sigspec(f, ff.sig_arst); + f << stringf(") %s <= ", reg_bit_name.c_str()); + dump_sigspec(f, val_arst); + f << stringf(";\n"); + f << stringf("%s" " else ", indent.c_str()); } - else - { - // for rd-transparent read-ports make something like: - // reg [..] temp_id; - // always @(posedge clk) - // temp_id <= r_addr; - // assign r_data = array_reg[temp_id]; - std::string temp_id = next_auto_id(); - lof_reg_declarations.push_back( stringf("reg [%d:0] %s;\n", sig_rd_addr.size() - 1, temp_id.c_str()) ); - { - std::ostringstream os; - dump_sigspec(os, sig_rd_addr); - std::string line = stringf("%s <= %s;\n", temp_id.c_str(), os.str().c_str()); - clk_to_lof_body[clk_domain_str].push_back(line); + + if (ff.has_srst && ff.has_en && ff.ce_over_srst) { + f << stringf("if (%s", ff.pol_en ? "" : "!"); + dump_sigspec(f, ff.sig_en); + f << stringf(")\n"); + f << stringf("%s" " if (%s", indent.c_str(), ff.pol_srst ? "" : "!"); + dump_sigspec(f, ff.sig_srst); + f << stringf(") %s <= ", reg_bit_name.c_str()); + dump_sigspec(f, val_srst); + f << stringf(";\n"); + f << stringf("%s" " else ", indent.c_str()); + } else { + if (ff.has_srst) { + f << stringf("if (%s", ff.pol_srst ? "" : "!"); + dump_sigspec(f, ff.sig_srst); + f << stringf(") %s <= ", reg_bit_name.c_str()); + dump_sigspec(f, val_srst); + f << stringf(";\n"); + f << stringf("%s" " else ", indent.c_str()); } - { - std::ostringstream os; - dump_sigspec(os, sig_rd_data); - std::string line = stringf("assign %s = %s[%s];\n", os.str().c_str(), mem_id.c_str(), temp_id.c_str()); - clk_to_lof_body[""].push_back(line); + if (ff.has_en) { + f << stringf("if (%s", ff.pol_en ? "" : "!"); + dump_sigspec(f, ff.sig_en); + f << stringf(") "); } } - } else { - // for non-clocked read-ports make something like: - // assign r_data = array_reg[r_addr]; - std::ostringstream os, os2; - dump_sigspec(os, sig_rd_data); - dump_sigspec(os2, sig_rd_addr); - std::string line = stringf("assign %s = %s[%s];\n", os.str().c_str(), mem_id.c_str(), os2.str().c_str()); - clk_to_lof_body[""].push_back(line); - } - } - int nwrite_ports = cell->parameters[ID::WR_PORTS].as_int(); - RTLIL::SigSpec sig_wr_clk, sig_wr_data, sig_wr_addr, sig_wr_en; - bool wr_clk_posedge; - - // write ports - for (int i=0; i < nwrite_ports; i++) - { - sig_wr_clk = cell->getPort(ID::WR_CLK).extract(i); - sig_wr_data = cell->getPort(ID::WR_DATA).extract(i*width, width); - sig_wr_addr = cell->getPort(ID::WR_ADDR).extract(i*abits, abits); - sig_wr_en = cell->getPort(ID::WR_EN).extract(i*width, width); - wr_clk_posedge = cell->parameters[ID::WR_CLK_POLARITY].extract(i).as_bool(); - { - std::ostringstream os; - dump_sigspec(os, sig_wr_clk); - clk_domain_str = stringf("%sedge %s", wr_clk_posedge ? "pos" : "neg", os.str().c_str()); - if( clk_to_lof_body.count(clk_domain_str) == 0 ) - clk_to_lof_body[clk_domain_str] = std::vector<std::string>(); + f << stringf("%s <= ", reg_bit_name.c_str()); + dump_sigspec(f, sig_d); + f << stringf(";\n"); } - // make something like: - // always @(posedge clk) - // if (wr_en_bit) memid[w_addr][??] <= w_data[??]; - // ... - for (int i = 0; i < GetSize(sig_wr_en); i++) + else { - int start_i = i, width = 1; - SigBit wen_bit = sig_wr_en[i]; - - while (i+1 < GetSize(sig_wr_en) && active_sigmap(sig_wr_en[i+1]) == active_sigmap(wen_bit)) - i++, width++; - - if (wen_bit == State::S0) - continue; - - std::ostringstream os; - if (wen_bit != State::S1) - { - os << stringf("if ("); - dump_sigspec(os, wen_bit); - os << stringf(") "); + // Latches. + f << stringf("%s" "always%s\n", indent.c_str(), systemverilog ? "_latch" : " @*"); + + f << stringf("%s" " ", indent.c_str()); + if (ff.has_sr) { + f << stringf("if (%s", ff.pol_clr ? "" : "!"); + dump_sigspec(f, ff.sig_clr[i]); + f << stringf(") %s = 1'b0;\n", reg_bit_name.c_str()); + f << stringf("%s" " else if (%s", indent.c_str(), ff.pol_set ? "" : "!"); + dump_sigspec(f, ff.sig_set[i]); + f << stringf(") %s = 1'b1;\n", reg_bit_name.c_str()); + if (ff.has_d) + f << stringf("%s" " else ", indent.c_str()); + } else if (ff.has_arst) { + f << stringf("if (%s", ff.pol_arst ? "" : "!"); + dump_sigspec(f, ff.sig_arst); + f << stringf(") %s = ", reg_bit_name.c_str()); + dump_sigspec(f, val_arst); + f << stringf(";\n"); + if (ff.has_d) + f << stringf("%s" " else ", indent.c_str()); + } + if (ff.has_d) { + f << stringf("if (%s", ff.pol_en ? "" : "!"); + dump_sigspec(f, ff.sig_en); + f << stringf(") %s = ", reg_bit_name.c_str()); + dump_sigspec(f, sig_d); + f << stringf(";\n"); } - 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: - // reg [..] _3_; - // always @(posedge CLK2) begin - // _3_ <= memory[D1ADDR]; - // if (A1EN) - // memory[A1ADDR] <= A1DATA; - // if (A2EN) - // memory[A2ADDR] <= A2DATA; - // ... - // end - // always @(negedge CLK1) begin - // if (C1EN) - // memory[C1ADDR] <= C1DATA; - // end - // ... - // assign D1DATA = _3_; - // assign D2DATA <= memory[D2ADDR]; - - // the reg ... definitions - for(auto ® : lof_reg_declarations) - { - f << stringf("%s" "%s", indent.c_str(), reg.c_str()); - } - // the block of expressions by clock domain - for(auto &pair : clk_to_lof_body) - { - std::string clk_domain = pair.first; - std::vector<std::string> lof_lines = pair.second; - if( clk_domain != "") - { - f << stringf("%s" "always%s @(%s) begin\n", indent.c_str(), systemverilog ? "_ff" : "", clk_domain.c_str()); - for(auto &line : lof_lines) - f << stringf("%s%s" "%s", indent.c_str(), indent.c_str(), line.c_str()); - f << stringf("%s" "end\n", indent.c_str()); - } - else - { - // the non-clocked assignments - for(auto &line : lof_lines) - f << stringf("%s" "%s", indent.c_str(), line.c_str()); - } + + if (!out_is_reg_wire) { + f << stringf("%s" "assign ", indent.c_str()); + dump_sigspec(f, ff.sig_q); + f << stringf(" = %s;\n", reg_name.c_str()); } return true; @@ -1528,14 +1456,17 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell) return true; } - // FIXME: $_SR_[PN][PN]_, $_DLATCH_[PN]_, $_DLATCHSR_[PN][PN][PN]_ - // FIXME: $sr, $dlatch, $memrd, $memwr, $fsm + // FIXME: $fsm return false; } void dump_cell(std::ostream &f, std::string indent, RTLIL::Cell *cell) { + // Handled by dump_memory + if (cell->type.in(ID($mem), ID($memwr), ID($memrd), ID($meminit))) + return; + if (cell->type[0] == '$' && !noexpr) { if (dump_cell_expr(f, indent, cell)) return; @@ -1602,7 +1533,7 @@ void dump_cell(std::ostream &f, std::string indent, RTLIL::Cell *cell) } } - if (siminit && reg_ct.count(cell->type) && cell->hasPort(ID::Q)) { + if (siminit && RTLIL::builtin_ff_cell_types().count(cell->type) && cell->hasPort(ID::Q) && !cell->type.in(ID($ff), ID($_FF_))) { std::stringstream ss; dump_reg_init(ss, cell->getPort(ID::Q)); if (!ss.str().empty()) { @@ -1812,7 +1743,7 @@ void dump_module(std::ostream &f, std::string indent, RTLIL::Module *module) std::set<std::pair<RTLIL::Wire*,int>> reg_bits; for (auto cell : module->cells()) { - if (!reg_ct.count(cell->type) || !cell->hasPort(ID::Q)) + if (!RTLIL::builtin_ff_cell_types().count(cell->type) || !cell->hasPort(ID::Q) || cell->type.in(ID($ff), ID($_FF_))) continue; RTLIL::SigSpec sig = cell->getPort(ID::Q); @@ -1858,8 +1789,8 @@ void dump_module(std::ostream &f, std::string indent, RTLIL::Module *module) for (auto w : module->wires()) dump_wire(f, indent + " ", w); - for (auto it = module->memories.begin(); it != module->memories.end(); ++it) - dump_memory(f, indent + " ", it->second); + for (auto &mem : Mem::get_all_memories(module)) + dump_memory(f, indent + " ", mem); for (auto cell : module->cells()) dump_cell(f, indent + " ", cell); @@ -1984,33 +1915,6 @@ struct VerilogBackend : public Backend { auto_name_map.clear(); reg_wires.clear(); - reg_ct.clear(); - - reg_ct.insert(ID($dff)); - reg_ct.insert(ID($adff)); - reg_ct.insert(ID($dffe)); - reg_ct.insert(ID($dlatch)); - - reg_ct.insert(ID($_DFF_N_)); - reg_ct.insert(ID($_DFF_P_)); - - reg_ct.insert(ID($_DFF_NN0_)); - reg_ct.insert(ID($_DFF_NN1_)); - reg_ct.insert(ID($_DFF_NP0_)); - reg_ct.insert(ID($_DFF_NP1_)); - reg_ct.insert(ID($_DFF_PN0_)); - reg_ct.insert(ID($_DFF_PN1_)); - reg_ct.insert(ID($_DFF_PP0_)); - reg_ct.insert(ID($_DFF_PP1_)); - - reg_ct.insert(ID($_DFFSR_NNN_)); - reg_ct.insert(ID($_DFFSR_NNP_)); - reg_ct.insert(ID($_DFFSR_NPN_)); - reg_ct.insert(ID($_DFFSR_NPP_)); - reg_ct.insert(ID($_DFFSR_PNN_)); - reg_ct.insert(ID($_DFFSR_PNP_)); - reg_ct.insert(ID($_DFFSR_PPN_)); - reg_ct.insert(ID($_DFFSR_PPP_)); size_t argidx; for (argidx = 1; argidx < args.size(); argidx++) { @@ -2107,7 +2011,6 @@ struct VerilogBackend : public Backend { auto_name_map.clear(); reg_wires.clear(); - reg_ct.clear(); } } VerilogBackend; |