Add "sim" support for memories

diff --git a/passes/sat/sim.cc b/passes/sat/sim.cc
index ae9a862a4e372c852eaaa98456be29204b859ebf..a80d89a81c154f0989010781b99f9f3fbd1f7922 100644 (file)
--- a/passes/sat/sim.cc
+++ b/passes/sat/sim.cc
@@ -47,6 +47,7 @@ struct SimInstance
        dict<SigBit, pool<Wire*>> upd_outports;
 
        pool<SigBit> dirty_bits;
+       pool<Cell*> dirty_cells;
        pool<SimInstance*, hash_ptr_ops> dirty_children;
 
        struct ff_state_t
@@ -122,6 +123,27 @@ struct SimInstance
                                ff_database[cell] = ff;
                        }
 
+                       if (cell->type == "$mem")
+                       {
+                               mem_state_t mem;
+
+                               mem.past_wr_clk = Const(State::Sx, GetSize(cell->getPort("\\WR_CLK")));
+                               mem.past_wr_en = Const(State::Sx, GetSize(cell->getPort("\\WR_EN")));
+                               mem.past_wr_addr = Const(State::Sx, GetSize(cell->getPort("\\WR_ADDR")));
+                               mem.past_wr_data = Const(State::Sx, GetSize(cell->getPort("\\WR_DATA")));
+
+                               mem.data = cell->getParam("\\INIT");
+                               int sz = cell->getParam("\\SIZE").as_int() * cell->getParam("\\WIDTH").as_int();
+
+                               if (GetSize(mem.data) > sz)
+                                       mem.data.bits.resize(sz);
+
+                               while (GetSize(mem.data) < sz)
+                                       mem.data.bits.push_back(State::Sx);
+
+                               mem_database[cell] = mem;
+                       }
+
                        if (cell->type.in("$assert", "$cover", "$assume")) {
                                formal_database.insert(cell);
                        }
@@ -193,6 +215,40 @@ struct SimInstance
                if (formal_database.count(cell))
                        return;
 
+               if (mem_database.count(cell))
+               {
+                       mem_state_t &mem = mem_database.at(cell);
+
+                       int num_rd_ports = cell->getParam("\\RD_PORTS").as_int();
+
+                       int size = cell->getParam("\\SIZE").as_int();
+                       int offset = cell->getParam("\\OFFSET").as_int();
+                       int abits = cell->getParam("\\ABITS").as_int();
+                       int width = cell->getParam("\\WIDTH").as_int();
+
+                       if (cell->getParam("\\RD_CLK_ENABLE").as_bool())
+                               log_error("Memory %s.%s has clocked read ports. Run 'memory' with -nordff.\n", log_id(module), log_id(cell));
+
+                       SigSpec rd_addr_sig = cell->getPort("\\RD_ADDR");
+                       SigSpec rd_data_sig = cell->getPort("\\RD_DATA");
+
+                       for (int port_idx = 0; port_idx < num_rd_ports; port_idx++)
+                       {
+                               Const addr = get_state(rd_addr_sig.extract(port_idx*abits, abits));
+                               Const data = Const(State::Sx, width);
+
+                               if (addr.is_fully_def()) {
+                                       int index = addr.as_int() - offset;
+                                       if (index >= 0 && index < size)
+                                               data = mem.data.extract(index*width, width);
+                               }
+
+                               set_state(rd_data_sig.extract(port_idx*width, width), data);
+                       }
+
+                       return;
+               }
+
                if (children.count(cell))
                {
                        auto child = children.at(cell);
@@ -249,8 +305,6 @@ struct SimInstance
                        return;
                }
 
-               // FIXME
-
                log_error("Unsupported cell type: %s (%s.%s)\n", log_id(cell->type), log_id(module), log_id(cell));
        }
 
@@ -259,6 +313,8 @@ struct SimInstance
                pool<Cell*> queue_cells;
                pool<Wire*> queue_outports;
 
+               queue_cells.swap(dirty_cells);
+
                while (1)
                {
                        for (auto bit : dirty_bits)
@@ -324,6 +380,58 @@ struct SimInstance
                        }
                }
 
+               for (auto &it : mem_database)
+               {
+                       Cell *cell = it.first;
+                       mem_state_t &mem = it.second;
+
+                       int num_wr_ports = cell->getParam("\\WR_PORTS").as_int();
+
+                       int size = cell->getParam("\\SIZE").as_int();
+                       int offset = cell->getParam("\\OFFSET").as_int();
+                       int abits = cell->getParam("\\ABITS").as_int();
+                       int width = cell->getParam("\\WIDTH").as_int();
+
+                       Const wr_clk_enable = cell->getParam("\\WR_CLK_ENABLE");
+                       Const wr_clk_polarity = cell->getParam("\\WR_CLK_POLARITY");
+                       Const current_wr_clk  = get_state(cell->getPort("\\WR_CLK"));
+
+                       for (int port_idx = 0; port_idx < num_wr_ports; port_idx++)
+                       {
+                               Const addr, data, enable;
+
+                               if (wr_clk_enable[port_idx] == State::S0)
+                               {
+                                       addr = get_state(cell->getPort("\\WR_ADDR").extract(port_idx*abits, abits));
+                                       data = get_state(cell->getPort("\\WR_DATA").extract(port_idx*width, width));
+                                       enable = get_state(cell->getPort("\\WR_EN").extract(port_idx*width, width));
+                               }
+                               else
+                               {
+                                       if (wr_clk_polarity[port_idx] == State::S1 ?
+                                                       (mem.past_wr_clk[port_idx] == State::S1 || current_wr_clk[port_idx] != State::S1) :
+                                                       (mem.past_wr_clk[port_idx] == State::S0 || current_wr_clk[port_idx] != State::S0))
+                                               continue;
+
+                                       addr = mem.past_wr_addr.extract(port_idx*abits, abits);
+                                       data = mem.past_wr_data.extract(port_idx*width, width);
+                                       enable = mem.past_wr_en.extract(port_idx*width, width);
+                               }
+
+                               if (addr.is_fully_def())
+                               {
+                                       int index = addr.as_int() - offset;
+                                       if (index >= 0 && index < size)
+                                               for (int i = 0; i < width; i++)
+                                                       if (enable[i] == State::S1 && mem.data.bits.at(index*width+i) != data[i]) {
+                                                               mem.data.bits.at(index*width+i) = data[i];
+                                                               dirty_cells.insert(cell);
+                                                               did_something = true;
+                                                       }
+                               }
+                       }
+               }
+
                for (auto it : children)
                        if (it.second->update_ph2()) {
                                dirty_children.insert(it.second);
@@ -346,6 +454,17 @@ struct SimInstance
                        }
                }
 
+               for (auto &it : mem_database)
+               {
+                       Cell *cell = it.first;
+                       mem_state_t &mem = it.second;
+
+                       mem.past_wr_clk  = get_state(cell->getPort("\\WR_CLK"));
+                       mem.past_wr_en   = get_state(cell->getPort("\\WR_EN"));
+                       mem.past_wr_addr = get_state(cell->getPort("\\WR_ADDR"));
+                       mem.past_wr_data = get_state(cell->getPort("\\WR_DATA"));
+               }
+
                for (auto cell : formal_database)
                {
                        string label = log_id(cell);
@@ -396,6 +515,21 @@ struct SimInstance
                        }
                }
 
+               for (auto &it : mem_database)
+               {
+                       Cell *cell = it.first;
+                       mem_state_t &mem = it.second;
+                       Const initval = mem.data;
+
+                       while (GetSize(initval) >= 2) {
+                               if (initval[GetSize(initval)-1] != State::Sx) break;
+                               if (initval[GetSize(initval)-2] != State::Sx) break;
+                               initval.bits.pop_back();
+                       }
+
+                       cell->setParam("\\INIT", initval);
+               }
+
                for (auto it : children)
                        it.second->writeback(wbmods);
        }