btor: Use Mem helper.
authorMarcelina Kościelnicka <mwk@0x04.net>
Sun, 18 Oct 2020 01:28:36 +0000 (03:28 +0200)
committerMarcelina Kościelnicka <mwk@0x04.net>
Wed, 21 Oct 2020 15:51:20 +0000 (17:51 +0200)
backends/btor/btor.cc

index 5abab8978c3e40be3ebf616b503c5ef641ef9822..639c6f12950ad6cb1853ead8c38185736bea5b5d 100644 (file)
@@ -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)));
                        }
                }