From 883e09d8edcdd5152294cde530faf4c9e4ff19e0 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sun, 9 Aug 2015 13:35:44 +0200 Subject: [PATCH] Use MEMID as name for $mem cell --- backends/smt2/smt2.cc | 7 ++- passes/memory/memory_collect.cc | 89 +++++++++++++++++---------------- 2 files changed, 53 insertions(+), 43 deletions(-) diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index 4f3b2319a..d828d6588 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -440,6 +440,9 @@ struct Smt2Worker decls.push_back(stringf("(declare-fun |%s#%d#0| (|%s_s|) (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n", log_id(module), arrayid, log_id(module), abits, width, log_id(cell))); + decls.push_back(stringf("(define-fun |%s_m %s| ((state |%s_s|)) (Array (_ BitVec %d) (_ BitVec %d)) (|%s#%d#0| state))\n", + log_id(module), log_id(cell), log_id(module), abits, width, log_id(module), arrayid)); + for (int i = 0; i < rd_ports; i++) { std::string addr = get_bv(cell->getPort("\\RD_ADDR").extract(abits*i, abits)); @@ -659,7 +662,9 @@ struct Smt2Backend : public Backend { log(" enable support for memories (via ArraysEx theory). this option\n"); log(" also implies -bv. only $mem cells without merged registers in\n"); log(" read ports are supported. call \"memory\" with -nordff to make sure\n"); - log(" that no registers are merged into $mem read ports.\n"); + log(" that no registers are merged into $mem read ports. '_m' functions\n"); + log(" will be generated for accessing the arrays that are used to represent\n"); + log(" memories.\n"); log("\n"); log(" -tpl \n"); log(" use the given template file. the line containing only the token '%%%%'\n"); diff --git a/passes/memory/memory_collect.cc b/passes/memory/memory_collect.cc index 134b5e8e1..91b5759eb 100644 --- a/passes/memory/memory_collect.cc +++ b/passes/memory/memory_collect.cc @@ -23,7 +23,7 @@ USING_YOSYS_NAMESPACE PRIVATE_NAMESPACE_BEGIN -bool memcells_cmp(RTLIL::Cell *a, RTLIL::Cell *b) +bool memcells_cmp(Cell *a, Cell *b) { if (a->type == "$memrd" && b->type == "$memrd") return a->name < b->name; @@ -32,7 +32,7 @@ bool memcells_cmp(RTLIL::Cell *a, RTLIL::Cell *b) return a->parameters.at("\\PRIORITY").as_int() < b->parameters.at("\\PRIORITY").as_int(); } -void handle_memory(RTLIL::Module *module, RTLIL::Memory *memory) +Cell *handle_memory(Module *module, RTLIL::Memory *memory) { log("Collecting $memrd, $memwr and $meminit for memory `%s' in module `%s':\n", memory->name.c_str(), module->name.c_str()); @@ -43,25 +43,25 @@ void handle_memory(RTLIL::Module *module, RTLIL::Memory *memory) SigMap sigmap(module); int wr_ports = 0; - RTLIL::SigSpec sig_wr_clk; - RTLIL::SigSpec sig_wr_clk_enable; - RTLIL::SigSpec sig_wr_clk_polarity; - RTLIL::SigSpec sig_wr_addr; - RTLIL::SigSpec sig_wr_data; - RTLIL::SigSpec sig_wr_en; + SigSpec sig_wr_clk; + SigSpec sig_wr_clk_enable; + SigSpec sig_wr_clk_polarity; + SigSpec sig_wr_addr; + SigSpec sig_wr_data; + SigSpec sig_wr_en; int rd_ports = 0; - RTLIL::SigSpec sig_rd_clk; - RTLIL::SigSpec sig_rd_clk_enable; - RTLIL::SigSpec sig_rd_clk_polarity; - RTLIL::SigSpec sig_rd_transparent; - RTLIL::SigSpec sig_rd_addr; - RTLIL::SigSpec sig_rd_data; + SigSpec sig_rd_clk; + SigSpec sig_rd_clk_enable; + SigSpec sig_rd_clk_polarity; + SigSpec sig_rd_transparent; + SigSpec sig_rd_addr; + SigSpec sig_rd_data; - std::vector memcells; + std::vector memcells; for (auto &cell_it : module->cells_) { - RTLIL::Cell *cell = cell_it.second; + Cell *cell = cell_it.second; if (cell->type.in("$memrd", "$memwr", "$meminit") && memory->name == cell->parameters["\\MEMID"].decode_string()) { addr_bits = std::max(addr_bits, cell->getParam("\\ABITS").as_int()); memcells.push_back(cell); @@ -70,7 +70,7 @@ void handle_memory(RTLIL::Module *module, RTLIL::Memory *memory) if (memcells.empty()) { log(" no cells found. removing memory.\n"); - return; + return nullptr; } std::sort(memcells.begin(), memcells.end(), memcells_cmp); @@ -104,8 +104,8 @@ void handle_memory(RTLIL::Module *module, RTLIL::Memory *memory) if (cell->type == "$memwr") { SigSpec clk = sigmap(cell->getPort("\\CLK")); - SigSpec clk_enable = RTLIL::SigSpec(cell->parameters["\\CLK_ENABLE"]); - SigSpec clk_polarity = RTLIL::SigSpec(cell->parameters["\\CLK_POLARITY"]); + SigSpec clk_enable = SigSpec(cell->parameters["\\CLK_ENABLE"]); + SigSpec clk_polarity = SigSpec(cell->parameters["\\CLK_POLARITY"]); SigSpec addr = sigmap(cell->getPort("\\ADDR")); SigSpec data = sigmap(cell->getPort("\\DATA")); SigSpec en = sigmap(cell->getPort("\\EN")); @@ -134,9 +134,9 @@ void handle_memory(RTLIL::Module *module, RTLIL::Memory *memory) if (cell->type == "$memrd") { SigSpec clk = sigmap(cell->getPort("\\CLK")); - SigSpec clk_enable = RTLIL::SigSpec(cell->parameters["\\CLK_ENABLE"]); - SigSpec clk_polarity = RTLIL::SigSpec(cell->parameters["\\CLK_POLARITY"]); - SigSpec transparent = RTLIL::SigSpec(cell->parameters["\\TRANSPARENT"]); + SigSpec clk_enable = SigSpec(cell->parameters["\\CLK_ENABLE"]); + SigSpec clk_polarity = SigSpec(cell->parameters["\\CLK_POLARITY"]); + SigSpec transparent = SigSpec(cell->parameters["\\TRANSPARENT"]); SigSpec addr = sigmap(cell->getPort("\\ADDR")); SigSpec data = sigmap(cell->getPort("\\DATA")); @@ -162,12 +162,12 @@ void handle_memory(RTLIL::Module *module, RTLIL::Memory *memory) std::stringstream sstr; sstr << "$mem$" << memory->name.str() << "$" << (autoidx++); - RTLIL::Cell *mem = module->addCell(sstr.str(), "$mem"); - mem->parameters["\\MEMID"] = RTLIL::Const(memory->name.str()); - mem->parameters["\\WIDTH"] = RTLIL::Const(memory->width); - mem->parameters["\\OFFSET"] = RTLIL::Const(memory->start_offset); - mem->parameters["\\SIZE"] = RTLIL::Const(memory->size); - mem->parameters["\\ABITS"] = RTLIL::Const(addr_bits); + Cell *mem = module->addCell(sstr.str(), "$mem"); + mem->parameters["\\MEMID"] = Const(memory->name.str()); + mem->parameters["\\WIDTH"] = Const(memory->width); + mem->parameters["\\OFFSET"] = Const(memory->start_offset); + mem->parameters["\\SIZE"] = Const(memory->size); + mem->parameters["\\ABITS"] = Const(addr_bits); while (GetSize(init_data) > 1 && init_data.bits.back() == State::Sx && init_data.bits[GetSize(init_data)-2] == State::Sx) init_data.bits.pop_back(); @@ -180,9 +180,9 @@ void handle_memory(RTLIL::Module *module, RTLIL::Memory *memory) log_assert(sig_wr_data.size() == wr_ports * memory->width); log_assert(sig_wr_en.size() == wr_ports * memory->width); - mem->parameters["\\WR_PORTS"] = RTLIL::Const(wr_ports); - mem->parameters["\\WR_CLK_ENABLE"] = wr_ports ? sig_wr_clk_enable.as_const() : RTLIL::Const(0, 1); - mem->parameters["\\WR_CLK_POLARITY"] = wr_ports ? sig_wr_clk_polarity.as_const() : RTLIL::Const(0, 1); + mem->parameters["\\WR_PORTS"] = Const(wr_ports); + mem->parameters["\\WR_CLK_ENABLE"] = wr_ports ? sig_wr_clk_enable.as_const() : Const(0, 1); + mem->parameters["\\WR_CLK_POLARITY"] = wr_ports ? sig_wr_clk_polarity.as_const() : Const(0, 1); mem->setPort("\\WR_CLK", sig_wr_clk); mem->setPort("\\WR_ADDR", sig_wr_addr); @@ -195,10 +195,10 @@ void handle_memory(RTLIL::Module *module, RTLIL::Memory *memory) log_assert(sig_rd_addr.size() == rd_ports * addr_bits); log_assert(sig_rd_data.size() == rd_ports * memory->width); - mem->parameters["\\RD_PORTS"] = RTLIL::Const(rd_ports); - mem->parameters["\\RD_CLK_ENABLE"] = rd_ports ? sig_rd_clk_enable.as_const() : RTLIL::Const(0, 1); - mem->parameters["\\RD_CLK_POLARITY"] = rd_ports ? sig_rd_clk_polarity.as_const() : RTLIL::Const(0, 1); - mem->parameters["\\RD_TRANSPARENT"] = rd_ports ? sig_rd_transparent.as_const() : RTLIL::Const(0, 1); + mem->parameters["\\RD_PORTS"] = Const(rd_ports); + mem->parameters["\\RD_CLK_ENABLE"] = rd_ports ? sig_rd_clk_enable.as_const() : Const(0, 1); + mem->parameters["\\RD_CLK_POLARITY"] = rd_ports ? sig_rd_clk_polarity.as_const() : Const(0, 1); + mem->parameters["\\RD_TRANSPARENT"] = rd_ports ? sig_rd_transparent.as_const() : Const(0, 1); mem->setPort("\\RD_CLK", sig_rd_clk); mem->setPort("\\RD_ADDR", sig_rd_addr); @@ -206,19 +206,24 @@ void handle_memory(RTLIL::Module *module, RTLIL::Memory *memory) for (auto c : memcells) module->remove(c); + + return mem; } -static void handle_module(RTLIL::Design *design, RTLIL::Module *module) +static void handle_module(Design *design, Module *module) { - std::vector delme; + std::vector> finqueue; + for (auto &mem_it : module->memories) if (design->selected(module, mem_it.second)) { - handle_memory(module, mem_it.second); - delme.push_back(mem_it.first); + Cell *c = handle_memory(module, mem_it.second); + finqueue.push_back(pair(c, mem_it.first)); } - for (auto &it : delme) { - delete module->memories.at(it); - module->memories.erase(it); + for (auto &it : finqueue) { + delete module->memories.at(it.second); + module->memories.erase(it.second); + if (it.first) + module->rename(it.first, it.second); } } -- 2.30.2