diff options
Diffstat (limited to 'backends')
| -rw-r--r-- | backends/btor/btor.cc | 195 | ||||
| -rw-r--r-- | backends/smt2/smt2.cc | 430 | ||||
| -rw-r--r-- | backends/verilog/verilog_backend.cc | 525 |
3 files changed, 597 insertions, 553 deletions
diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc index 5abab8978..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; @@ -704,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; @@ -764,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); @@ -784,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) { @@ -797,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); @@ -835,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 { @@ -1065,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()) @@ -1201,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); @@ -1213,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; - int wa_nid = get_sig_nid(wa); - int wd_nid = get_sig_nid(wd); - int we_nid = get_sig_nid(we); + btorf_push(stringf("next %s", log_id(mem->memid))); - int nid2 = next_nid++; - btorf("%d read %d %d %d\n", nid2, data_sid, nid_head, wa_nid); + int abits = ceil_log2(mem->size); - int nid3 = next_nid++; - btorf("%d not %d %d\n", nid3, data_sid, we_nid); + 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 nid4 = next_nid++; - btorf("%d and %d %d %d\n", nid4, data_sid, nid2, nid3); + for (auto &port : mem->wr_ports) + { + SigSpec wa = port.addr; + wa.extend_u0(abits); - int nid5 = next_nid++; - btorf("%d and %d %d %d\n", nid5, data_sid, wd_nid, 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 nid6 = next_nid++; - btorf("%d or %d %d %d\n", nid6, data_sid, nid5, nid4); + int nid2 = next_nid++; + btorf("%d read %d %d %d\n", nid2, data_sid, nid_head, wa_nid); - int nid7 = next_nid++; - btorf("%d write %d %d %d %d\n", nid7, sid, nid_head, wa_nid, nid6); + int nid3 = next_nid++; + btorf("%d not %d %d\n", nid3, data_sid, we_nid); - int nid8 = next_nid++; - btorf("%d redor %d %d\n", nid8, bool_sid, we_nid); + int nid4 = next_nid++; + btorf("%d and %d %d %d\n", nid4, data_sid, nid2, nid3); - int nid9 = next_nid++; - btorf("%d ite %d %d %d %d\n", nid9, sid, nid8, nid7, nid_head); + int nid5 = next_nid++; + btorf("%d and %d %d %d\n", nid5, data_sid, wd_nid, we_nid); - nid_head = nid9; - } + int nid6 = next_nid++; + btorf("%d or %d %d %d\n", nid6, data_sid, nid5, nid4); - 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()); + int nid7 = next_nid++; + btorf("%d write %d %d %d %d\n", nid7, sid, nid_head, wa_nid, nid6); + + int nid8 = next_nid++; + btorf("%d redor %d %d\n", nid8, bool_sid, we_nid); + + int nid9 = next_nid++; + btorf("%d ite %d %d %d %d\n", nid9, sid, nid8, nid7, nid_head); + + 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/smt2/smt2.cc b/backends/smt2/smt2.cc index 0b4e20ac6..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; } @@ -977,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); @@ -1010,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); + + for (auto mem : this_mems) + { + int arrayid = memarrays.at(mem); + + int abits = ceil_log2(mem->size);; - 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(); + 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; + } - bool async_read = false; - string initial_memstate, final_memstate; + string initial_memstate, final_memstate; - 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); + 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)); } } } @@ -1586,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/verilog/verilog_backend.cc b/backends/verilog/verilog_backend.cc index bf980129d..9523f4a52 100644 --- a/backends/verilog/verilog_backend.cc +++ b/backends/verilog/verilog_backend.cc @@ -26,6 +26,7 @@ #include "kernel/log.h" #include "kernel/sigtools.h" #include "kernel/ff.h" +#include "kernel/mem.h" #include <string> #include <sstream> #include <set> @@ -434,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) @@ -1095,274 +1336,6 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell) 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) - { - 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 - { - 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'; - } - } - - } - else - { - f << stringf("%s" "initial begin\n", indent.c_str()); - for (int i=0; i<size; i++) - { - f << stringf("%s" " %s[%d] = ", indent.c_str(), mem_id.c_str(), i); - dump_const(f, cell->parameters[ID::INIT].extract(i*width, 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; - - 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) - { - { - 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>(); - } - 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); - } - } - 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); - } - { - 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); - } - } - } 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>(); - } - // 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++) - { - 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(") "); - } - 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()); - } - } - - return true; - } - if (cell->type.in(ID($assert), ID($assume), ID($cover))) { f << stringf("%s" "always%s if (", indent.c_str(), systemverilog ? "_comb" : " @*"); @@ -1483,13 +1456,17 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell) return true; } - // FIXME: $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; @@ -1812,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); |