From: Marcelina Kościelnicka Date: Sun, 18 Oct 2020 01:28:36 +0000 (+0200) Subject: btor: Use Mem helper. X-Git-Tag: working-ls180~225 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2d340cd3559f4e22a910a7fe6e193138dd068996;p=yosys.git btor: Use Mem helper. --- 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 USING_YOSYS_NAMESPACE @@ -68,12 +69,15 @@ struct BtorWorker // ff inputs that need to be evaluated (, ) vector> ff_todo; + vector> mem_todo; pool cell_recursion_guard; vector bad_properties; dict initbits; pool statewires; pool srcsymbols; + vector memories; + dict mem_cells; string indent, info_filename; vector 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 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> 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> 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))); } }