Start restoring memory state from VCD/FST

diff --git a/kernel/fstdata.cc b/kernel/fstdata.cc
index 2bec58bcf555d195964fb3b868373df0b894a08c..1bf43bfdda688c7bd5c643e184a1b96cc287a3ae 100644 (file)
--- a/kernel/fstdata.cc
+++ b/kernel/fstdata.cc
@@ -85,6 +85,13 @@ fstHandle FstData::getHandle(std::string name) {
                return 0;
 };
 
+dict<int,fstHandle> FstData::getMemoryHandles(std::string name) { 
+       if (memory_to_handle.find(name) != memory_to_handle.end())
+               return memory_to_handle[name];
+       else 
+               return dict<int,fstHandle>();
+};
+
 static std::string remove_spaces(std::string str)
 {
        str.erase(std::remove(str.begin(), str.end(), ' '), str.end());
@@ -126,7 +133,30 @@ void FstData::extractVarNames()
                                }
                                if (clean_name[0]=='\\')
                                        clean_name = clean_name.substr(1);
-
+                               size_t pos = clean_name.find_last_of("<");
+                               if (pos != std::string::npos) {
+                                       std::string mem_cell = clean_name.substr(0, pos);
+                                       std::string addr = clean_name.substr(pos+1);
+                                       addr.pop_back(); // remove closing bracket
+                                       char *endptr;
+                                       int mem_addr = strtol(addr.c_str(), &endptr, 16);
+                                       if (*endptr) {
+                                               log_error("Error parsing memory address in : %s\n", clean_name.c_str());
+                                       }
+                                       memory_to_handle[var.scope+"."+mem_cell][mem_addr] = var.id;
+                               }
+                               pos = clean_name.find_last_of("[");
+                               if (pos != std::string::npos) {
+                                       std::string mem_cell = clean_name.substr(0, pos);
+                                       std::string addr = clean_name.substr(pos+1);
+                                       addr.pop_back(); // remove closing bracket
+                                       char *endptr;
+                                       int mem_addr = strtol(addr.c_str(), &endptr, 10);
+                                       if (*endptr) {
+                                               log_error("Error parsing memory address in : %s\n", clean_name.c_str());
+                                       }
+                                       memory_to_handle[var.scope+"."+mem_cell][mem_addr] = var.id;
+                               }
                                name_to_handle[var.scope+"."+clean_name] = h->u.var.handle;
                                break;
                        }

diff --git a/kernel/fstdata.h b/kernel/fstdata.h
index d8dca5fb0a33362f7f599c82121a1771ca91199b..f5cf1d48d8e189e35f115bf624a7c4d6bcfe2a1a 100644 (file)
--- a/kernel/fstdata.h
+++ b/kernel/fstdata.h
@@ -54,6 +54,7 @@ class FstData
 
        std::string valueOf(fstHandle signal);
        fstHandle getHandle(std::string name);
+       dict<int,fstHandle> getMemoryHandles(std::string name);
        double getTimescale() { return timescale; }
        const char *getTimescaleString() { return timescale_str.c_str(); }
 private:
@@ -63,6 +64,7 @@ private:
        std::vector<FstVar> vars;
        std::map<fstHandle, FstVar> handle_to_var;
        std::map<std::string, fstHandle> name_to_handle;
+       std::map<std::string, dict<int, fstHandle>> memory_to_handle;
        std::map<fstHandle, std::string> last_data;
        uint64_t last_time;
        std::map<fstHandle, std::string> past_data;

diff --git a/passes/sat/sim.cc b/passes/sat/sim.cc
index 7b52b85cd3078861fea923859e89e5a813db85a0..654378d09ec234ae84c043830905ad4c37b6f49d 100644 (file)
--- a/passes/sat/sim.cc
+++ b/passes/sat/sim.cc
@@ -157,6 +157,7 @@ struct SimInstance
 
        dict<Wire*, pair<int, Const>> signal_database;
        dict<Wire*, fstHandle> fst_handles;
+       dict<IdString, dict<int,fstHandle>> fst_memories;
 
        SimInstance(SimShared *shared, std::string scope, Module *module, Cell *instance = nullptr, SimInstance *parent = nullptr) :
                        shared(shared), scope(scope), module(module), instance(instance), parent(parent), sigmap(module)
@@ -243,7 +244,9 @@ struct SimInstance
 
                        if (cell->is_mem_cell())
                        {
-                               mem_cells[cell] = cell->parameters.at(ID::MEMID).decode_string();
+                               std::string name = cell->parameters.at(ID::MEMID).decode_string();
+                               mem_cells[cell] = name;
+                               fst_memories[name] = shared->fst->getMemoryHandles(scope + "." + RTLIL::unescape_id(name));
                        }
                        if (cell->type.in(ID($assert), ID($cover), ID($assume))) {
                                formal_database.insert(cell);
@@ -336,7 +339,7 @@ struct SimInstance
 
                int offset = (addr.as_int() - state.mem->start_offset) * state.mem->width;
                for (int i = 0; i < GetSize(data); i++)
-                       if (0 <= i+offset && i+offset < GetSize(data))
+                       if (0 <= i+offset && i+offset < state.mem->size * state.mem->width)
                                state.data.bits[i+offset] = data.bits[i];
        }
 
@@ -799,6 +802,18 @@ struct SimInstance
                                did_something |= true;
                        }
                }
+               for (auto cell : module->cells())
+               {
+                       if (cell->is_mem_cell()) {
+                               std::string memid = cell->parameters.at(ID::MEMID).decode_string();
+                               for (auto &data : fst_memories[memid]) 
+                               {
+                                       std::string v = shared->fst->valueOf(data.second);
+                                       set_memory_state(memid, Const(data.first), Const::from_string(v));
+                               }
+                       }
+               }
+
                for (auto child : children)
                        did_something |= child.second->setInitState();
                return did_something;