Merge pull request #3299 from YosysHQ/mmicko/sim_memory

sim pass: support for memories

4 files changed, 59 insertions, 3 deletions

diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc
index 73e88c049..7de5deadd 100644
--- a/backends/btor/btor.cc
+++ b/backends/btor/btor.cc
@@ -1220,6 +1220,8 @@ struct BtorWorker
 
 			int this_nid = next_nid++;
 			btorf("%d uext %d %d %d%s\n", this_nid, sid, nid, 0, getinfo(wire).c_str());
+			if (info_clocks.count(nid))
+				info_clocks[this_nid] |= info_clocks[nid];
 
 			btorf_pop(stringf("wire %s", log_id(wire)));
 			continue;
diff --git a/kernel/fstdata.cc b/kernel/fstdata.cc
index 2bec58bcf..fea8ee3c3 100644
--- 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,36 @@ 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_warning("Error parsing memory address in : %s\n", clean_name.c_str());
+					} else {
+						memory_to_handle[var.scope+"."+mem_cell][mem_addr] = var.id;
+						name_to_handle[stringf("%s.%s[%d]",var.scope.c_str(),mem_cell.c_str(),mem_addr)] = h->u.var.handle;
+						continue;
+					}
+				}
+				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_warning("Error parsing memory address in : %s\n", clean_name.c_str());
+					} else {
+						memory_to_handle[var.scope+"."+mem_cell][mem_addr] = var.id;
+						name_to_handle[stringf("%s.%s[%d]",var.scope.c_str(),mem_cell.c_str(),mem_addr)] = h->u.var.handle;
+						continue;
+					}
+				}
 				name_to_handle[var.scope+"."+clean_name] = h->u.var.handle;
 				break;
 			}
diff --git a/kernel/fstdata.h b/kernel/fstdata.h
index d8dca5fb0..f5cf1d48d 100644
--- 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 7b52b85cd..d085fab2d 100644
--- 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,10 @@ 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;
+				if (shared->fst)
+					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 +340,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 +803,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;