From: Marcelina Kościelnicka <mwk@0x04.net>
Date: Sun, 18 Oct 2020 01:09:45 +0000 (+0200)
Subject: smt2: Use Mem helper.
X-Git-Tag: working-ls180~226
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f272c8b407b656aedaa48a362f1e844278be3b16;p=yosys.git

smt2: Use Mem helper.
---

diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index 0b4e20ac6..a185fdd74 100644
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -22,6 +22,7 @@
 #include "kernel/sigtools.h"
 #include "kernel/celltypes.h"
 #include "kernel/log.h"
+#include "kernel/mem.h"
 #include <string>
 
 USING_YOSYS_NAMESPACE
@@ -40,12 +41,15 @@ struct Smt2Worker
 	std::map<RTLIL::SigBit, RTLIL::Cell*> bit_driver;
 	std::set<RTLIL::Cell*> exported_cells, hiercells, hiercells_queue;
 	pool<Cell*> recursive_cells, registers;
+	std::vector<Mem> memories;
+	dict<Cell*, Mem*> mem_cells;
+	std::set<Mem*> memory_queue;
 
 	pool<SigBit> clock_posedge, clock_negedge;
 	vector<string> ex_state_eq, ex_input_eq;
 
 	std::map<RTLIL::SigBit, std::pair<int, int>> fcache;
-	std::map<Cell*, int> memarrays;
+	std::map<Mem*, int> memarrays;
 	std::map<int, int> bvsizes;
 	dict<IdString, char*> ids;
 
@@ -116,12 +120,73 @@ struct Smt2Worker
 
 		makebits(stringf("%s_is", get_id(module)));
 
+		dict<IdString, Mem*> mem_dict;
+		memories = Mem::get_all_memories(module);
+		for (auto &mem : memories)
+		{
+			mem_dict[mem.memid] = &mem;
+			for (auto &port : mem.wr_ports)
+			{
+				if (port.clk_enable) {
+					SigSpec clk = sigmap(port.clk);
+					for (int i = 0; i < GetSize(clk); i++)
+					{
+						if (clk[i].wire == nullptr)
+							continue;
+						if (port.clk_polarity)
+							clock_posedge.insert(clk[i]);
+						else
+							clock_negedge.insert(clk[i]);
+					}
+				}
+				for (auto bit : sigmap(port.en))
+					noclock.insert(bit);
+				for (auto bit : sigmap(port.addr))
+					noclock.insert(bit);
+				for (auto bit : sigmap(port.data))
+					noclock.insert(bit);
+			}
+			for (auto &port : mem.rd_ports)
+			{
+				if (port.clk_enable) {
+					SigSpec clk = sigmap(port.clk);
+					for (int i = 0; i < GetSize(clk); i++)
+					{
+						if (clk[i].wire == nullptr)
+							continue;
+						if (port.clk_polarity)
+							clock_posedge.insert(clk[i]);
+						else
+							clock_negedge.insert(clk[i]);
+					}
+				}
+				for (auto bit : sigmap(port.en))
+					noclock.insert(bit);
+				for (auto bit : sigmap(port.addr))
+					noclock.insert(bit);
+				for (auto bit : sigmap(port.data))
+					noclock.insert(bit);
+				Cell *driver = port.cell ? port.cell : mem.cell;
+				for (auto bit : sigmap(port.data)) {
+					if (bit_driver.count(bit))
+						log_error("Found multiple drivers for %s.\n", log_signal(bit));
+					bit_driver[bit] = driver;
+				}
+			}
+		}
+
 		for (auto cell : module->cells())
 		for (auto &conn : cell->connections())
 		{
 			if (GetSize(conn.second) == 0)
 				continue;
 
+			// Handled above.
+			if (cell->type.in(ID($mem), ID($memrd), ID($memwr), ID($meminit))) {
+				mem_cells[cell] = mem_dict[cell->parameters.at(ID::MEMID).decode_string()];
+				continue;
+			}
+
 			bool is_input = ct.cell_input(cell->type, conn.first);
 			bool is_output = ct.cell_output(cell->type, conn.first);
 
@@ -135,24 +200,6 @@ struct Smt2Worker
 				log_error("Unsupported or unknown directionality on port %s of cell %s.%s (%s).\n",
 						log_id(conn.first), log_id(module), log_id(cell), log_id(cell->type));
 
-			if (cell->type.in(ID($mem)) && conn.first.in(ID::RD_CLK, ID::WR_CLK))
-			{
-				SigSpec clk = sigmap(conn.second);
-				for (int i = 0; i < GetSize(clk); i++)
-				{
-					if (clk[i].wire == nullptr)
-						continue;
-
-					if (cell->getParam(conn.first == ID::RD_CLK ? ID::RD_CLK_ENABLE : ID::WR_CLK_ENABLE)[i] != State::S1)
-						continue;
-
-					if (cell->getParam(conn.first == ID::RD_CLK ? ID::RD_CLK_POLARITY : ID::WR_CLK_POLARITY)[i] == State::S1)
-						clock_posedge.insert(clk[i]);
-					else
-						clock_negedge.insert(clk[i]);
-				}
-			}
-			else
 			if (cell->type.in(ID($dff), ID($_DFF_P_), ID($_DFF_N_)) && conn.first.in(ID::CLK, ID::C))
 			{
 				bool posedge = (cell->type == ID($_DFF_N_)) || (cell->type == ID($dff) && cell->getParam(ID::CLK_POLARITY).as_bool());
@@ -647,27 +694,35 @@ struct Smt2Worker
 			// FIXME: $slice $concat
 		}
 
-		if (memmode && cell->type == ID($mem))
+		if (memmode && cell->type.in(ID($mem), ID($memrd), ID($memwr), ID($meminit)))
 		{
+			Mem *mem = mem_cells[cell];
+
+			if (memarrays.count(mem)) {
+				recursive_cells.erase(cell);
+				return;
+			}
+
 			int arrayid = idcounter++;
-			memarrays[cell] = arrayid;
-
-			int abits = cell->getParam(ID::ABITS).as_int();
-			int width = cell->getParam(ID::WIDTH).as_int();
-			int rd_ports = cell->getParam(ID::RD_PORTS).as_int();
-			int wr_ports = cell->getParam(ID::WR_PORTS).as_int();
-
-			bool async_read = false;
-			if (!cell->getParam(ID::WR_CLK_ENABLE).is_fully_ones()) {
-				if (!cell->getParam(ID::WR_CLK_ENABLE).is_fully_zero())
-					log_error("Memory %s.%s has mixed clocked/nonclocked write ports. This is not supported by \"write_smt2\".\n", log_id(cell), log_id(module));
-				async_read = true;
+			memarrays[mem] = arrayid;
+
+			int abits = ceil_log2(mem->size);
+
+			bool has_sync_wr = false;
+			bool has_async_wr = false;
+			for (auto &port : mem->wr_ports) {
+				if (port.clk_enable)
+					has_sync_wr = true;
+				else
+					has_async_wr = true;
 			}
+			if (has_async_wr && has_sync_wr)
+				log_error("Memory %s.%s has mixed clocked/nonclocked write ports. This is not supported by \"write_smt2\".\n", log_id(cell), log_id(module));
 
-			decls.push_back(stringf("; yosys-smt2-memory %s %d %d %d %d %s\n", get_id(cell), abits, width, rd_ports, wr_ports, async_read ? "async" : "sync"));
+			decls.push_back(stringf("; yosys-smt2-memory %s %d %d %d %d %s\n", get_id(mem->memid), abits, mem->width, GetSize(mem->rd_ports), GetSize(mem->wr_ports), has_async_wr ? "async" : "sync"));
 
 			string memstate;
-			if (async_read) {
+			if (has_async_wr) {
 				memstate = stringf("%s#%d#final", get_id(module), arrayid);
 			} else {
 				memstate = stringf("%s#%d#0", get_id(module), arrayid);
@@ -675,80 +730,79 @@ struct Smt2Worker
 
 			if (statebv)
 			{
-				int mem_size = cell->getParam(ID::SIZE).as_int();
-				int mem_offset = cell->getParam(ID::OFFSET).as_int();
-
-				makebits(memstate, width*mem_size, get_id(cell));
+				makebits(memstate, mem->width*mem->size, get_id(mem->memid));
 				decls.push_back(stringf("(define-fun |%s_m %s| ((state |%s_s|)) (_ BitVec %d) (|%s| state))\n",
-						get_id(module), get_id(cell), get_id(module), width*mem_size, memstate.c_str()));
+						get_id(module), get_id(mem->memid), get_id(module), mem->width*mem->size, memstate.c_str()));
 
-				for (int i = 0; i < rd_ports; i++)
+				for (int i = 0; i < GetSize(mem->rd_ports); i++)
 				{
-					SigSpec addr_sig = cell->getPort(ID::RD_ADDR).extract(abits*i, abits);
-					SigSpec data_sig = cell->getPort(ID::RD_DATA).extract(width*i, width);
+					auto &port = mem->rd_ports[i];
+					SigSpec addr_sig = port.addr;
+					addr_sig.extend_u0(abits);
 					std::string addr = get_bv(addr_sig);
 
-					if (cell->getParam(ID::RD_CLK_ENABLE).extract(i).as_bool())
+					if (port.clk_enable)
 						log_error("Read port %d (%s) of memory %s.%s is clocked. This is not supported by \"write_smt2\"! "
-								"Call \"memory\" with -nordff to avoid this error.\n", i, log_signal(data_sig), log_id(cell), log_id(module));
+								"Call \"memory\" with -nordff to avoid this error.\n", i, log_signal(port.data), log_id(mem->memid), log_id(module));
 
 					decls.push_back(stringf("(define-fun |%s_m:R%dA %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
-							get_id(module), i, get_id(cell), get_id(module), abits, addr.c_str(), log_signal(addr_sig)));
+							get_id(module), i, get_id(mem->memid), get_id(module), abits, addr.c_str(), log_signal(addr_sig)));
 
 					std::string read_expr = "#b";
-					for (int k = 0; k < width; k++)
+					for (int k = 0; k < mem->width; k++)
 						read_expr += "0";
 
-					for (int k = 0; k < mem_size; k++)
+					for (int k = 0; k < mem->size; k++)
 						read_expr = stringf("(ite (= (|%s_m:R%dA %s| state) #b%s) ((_ extract %d %d) (|%s| state))\n  %s)",
-								get_id(module), i, get_id(cell), Const(k+mem_offset, abits).as_string().c_str(),
-								width*(k+1)-1, width*k, memstate.c_str(), read_expr.c_str());
+								get_id(module), i, get_id(mem->memid), Const(k+mem->start_offset, abits).as_string().c_str(),
+								mem->width*(k+1)-1, mem->width*k, memstate.c_str(), read_expr.c_str());
 
 					decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) (_ BitVec %d)\n  %s) ; %s\n",
-							get_id(module), idcounter, get_id(module), width, read_expr.c_str(), log_signal(data_sig)));
+							get_id(module), idcounter, get_id(module), mem->width, read_expr.c_str(), log_signal(port.data)));
 
 					decls.push_back(stringf("(define-fun |%s_m:R%dD %s| ((state |%s_s|)) (_ BitVec %d) (|%s#%d| state))\n",
-							get_id(module), i, get_id(cell), get_id(module), width, get_id(module), idcounter));
+							get_id(module), i, get_id(mem->memid), get_id(module), mem->width, get_id(module), idcounter));
 
-					register_bv(data_sig, idcounter++);
+					register_bv(port.data, idcounter++);
 				}
 			}
 			else
 			{
 				if (statedt)
 					dtmembers.push_back(stringf("  (|%s| (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n",
-							memstate.c_str(), abits, width, get_id(cell)));
+							memstate.c_str(), abits, mem->width, get_id(mem->memid)));
 				else
 					decls.push_back(stringf("(declare-fun |%s| (|%s_s|) (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n",
-							memstate.c_str(), get_id(module), abits, width, get_id(cell)));
+							memstate.c_str(), get_id(module), abits, mem->width, get_id(mem->memid)));
 
 				decls.push_back(stringf("(define-fun |%s_m %s| ((state |%s_s|)) (Array (_ BitVec %d) (_ BitVec %d)) (|%s| state))\n",
-						get_id(module), get_id(cell), get_id(module), abits, width, memstate.c_str()));
+						get_id(module), get_id(mem->memid), get_id(module), abits, mem->width, memstate.c_str()));
 
-				for (int i = 0; i < rd_ports; i++)
+				for (int i = 0; i < GetSize(mem->rd_ports); i++)
 				{
-					SigSpec addr_sig = cell->getPort(ID::RD_ADDR).extract(abits*i, abits);
-					SigSpec data_sig = cell->getPort(ID::RD_DATA).extract(width*i, width);
+					auto &port = mem->rd_ports[i];
+					SigSpec addr_sig = port.addr;
+					addr_sig.extend_u0(abits);
 					std::string addr = get_bv(addr_sig);
 
-					if (cell->getParam(ID::RD_CLK_ENABLE).extract(i).as_bool())
+					if (port.clk_enable)
 						log_error("Read port %d (%s) of memory %s.%s is clocked. This is not supported by \"write_smt2\"! "
-								"Call \"memory\" with -nordff to avoid this error.\n", i, log_signal(data_sig), log_id(cell), log_id(module));
+								"Call \"memory\" with -nordff to avoid this error.\n", i, log_signal(port.data), log_id(mem->memid), log_id(module));
 
 					decls.push_back(stringf("(define-fun |%s_m:R%dA %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
-							get_id(module), i, get_id(cell), get_id(module), abits, addr.c_str(), log_signal(addr_sig)));
+							get_id(module), i, get_id(mem->memid), get_id(module), abits, addr.c_str(), log_signal(addr_sig)));
 
 					decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) (_ BitVec %d) (select (|%s| state) (|%s_m:R%dA %s| state))) ; %s\n",
-							get_id(module), idcounter, get_id(module), width, memstate.c_str(), get_id(module), i, get_id(cell), log_signal(data_sig)));
+							get_id(module), idcounter, get_id(module), mem->width, memstate.c_str(), get_id(module), i, get_id(mem->memid), log_signal(port.data)));
 
 					decls.push_back(stringf("(define-fun |%s_m:R%dD %s| ((state |%s_s|)) (_ BitVec %d) (|%s#%d| state))\n",
-							get_id(module), i, get_id(cell), get_id(module), width, get_id(module), idcounter));
+							get_id(module), i, get_id(mem->memid), get_id(module), mem->width, get_id(module), idcounter));
 
-					register_bv(data_sig, idcounter++);
+					register_bv(port.data, idcounter++);
 				}
 			}
 
-			registers.insert(cell);
+			memory_queue.insert(mem);
 			recursive_cells.erase(cell);
 			return;
 		}
@@ -977,7 +1031,7 @@ struct Smt2Worker
 			}
 		}
 
-		for (int iter = 1; !registers.empty(); iter++)
+		for (int iter = 1; !registers.empty() || !memory_queue.empty(); iter++)
 		{
 			pool<Cell*> this_regs;
 			this_regs.swap(registers);
@@ -1010,152 +1064,156 @@ struct Smt2Worker
 					if (cell->type == ID($anyconst))
 						ex_state_eq.push_back(stringf("(= %s %s)", get_bv(cell->getPort(ID::Y)).c_str(), get_bv(cell->getPort(ID::Y), "other_state").c_str()));
 				}
+			}
 
-				if (cell->type == ID($mem))
-				{
-					int arrayid = memarrays.at(cell);
+			std::set<Mem*> this_mems;
+			this_mems.swap(memory_queue);
+
+			for (auto mem : this_mems)
+			{
+				int arrayid = memarrays.at(mem);
+
+				int abits = ceil_log2(mem->size);;
 
-					int abits = cell->getParam(ID::ABITS).as_int();
-					int width = cell->getParam(ID::WIDTH).as_int();
-					int wr_ports = cell->getParam(ID::WR_PORTS).as_int();
+				bool has_sync_wr = false;
+				bool has_async_wr = false;
+				for (auto &port : mem->wr_ports) {
+					if (port.clk_enable)
+						has_sync_wr = true;
+					else
+						has_async_wr = true;
+				}
 
-					bool async_read = false;
-					string initial_memstate, final_memstate;
+				string initial_memstate, final_memstate;
 
-					if (!cell->getParam(ID::WR_CLK_ENABLE).is_fully_ones()) {
-						log_assert(cell->getParam(ID::WR_CLK_ENABLE).is_fully_zero());
-						async_read = true;
-						initial_memstate = stringf("%s#%d#0", get_id(module), arrayid);
-						final_memstate = stringf("%s#%d#final", get_id(module), arrayid);
+				if (has_async_wr) {
+					log_assert(!has_sync_wr);
+					initial_memstate = stringf("%s#%d#0", get_id(module), arrayid);
+					final_memstate = stringf("%s#%d#final", get_id(module), arrayid);
+				}
+
+				if (statebv)
+				{
+					if (has_async_wr) {
+						makebits(final_memstate, mem->width*mem->size, get_id(mem->memid));
 					}
 
-					if (statebv)
+					for (int i = 0; i < GetSize(mem->wr_ports); i++)
 					{
-						int mem_size = cell->getParam(ID::SIZE).as_int();
-						int mem_offset = cell->getParam(ID::OFFSET).as_int();
-
-						if (async_read) {
-							makebits(final_memstate, width*mem_size, get_id(cell));
+						auto &port = mem->wr_ports[i];
+						SigSpec addr_sig = port.addr;
+						addr_sig.extend_u0(abits);
+
+						std::string addr = get_bv(addr_sig);
+						std::string data = get_bv(port.data);
+						std::string mask = get_bv(port.en);
+
+						decls.push_back(stringf("(define-fun |%s_m:W%dA %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
+								get_id(module), i, get_id(mem->memid), get_id(module), abits, addr.c_str(), log_signal(addr_sig)));
+						addr = stringf("(|%s_m:W%dA %s| state)", get_id(module), i, get_id(mem->memid));
+
+						decls.push_back(stringf("(define-fun |%s_m:W%dD %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
+								get_id(module), i, get_id(mem->memid), get_id(module), mem->width, data.c_str(), log_signal(port.data)));
+						data = stringf("(|%s_m:W%dD %s| state)", get_id(module), i, get_id(mem->memid));
+
+						decls.push_back(stringf("(define-fun |%s_m:W%dM %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
+								get_id(module), i, get_id(mem->memid), get_id(module), mem->width, mask.c_str(), log_signal(port.en)));
+						mask = stringf("(|%s_m:W%dM %s| state)", get_id(module), i, get_id(mem->memid));
+
+						std::string data_expr;
+
+						for (int k = mem->size-1; k >= 0; k--) {
+							std::string new_data = stringf("(bvor (bvand %s %s) (bvand ((_ extract %d %d) (|%s#%d#%d| state)) (bvnot %s)))",
+									data.c_str(), mask.c_str(), mem->width*(k+1)-1, mem->width*k, get_id(module), arrayid, i, mask.c_str());
+							data_expr += stringf("\n  (ite (= %s #b%s) %s ((_ extract %d %d) (|%s#%d#%d| state)))",
+									addr.c_str(), Const(k+mem->start_offset, abits).as_string().c_str(), new_data.c_str(),
+									mem->width*(k+1)-1, mem->width*k, get_id(module), arrayid, i);
 						}
 
-						for (int i = 0; i < wr_ports; i++)
-						{
-							SigSpec addr_sig = cell->getPort(ID::WR_ADDR).extract(abits*i, abits);
-							SigSpec data_sig = cell->getPort(ID::WR_DATA).extract(width*i, width);
-							SigSpec mask_sig = cell->getPort(ID::WR_EN).extract(width*i, width);
+						decls.push_back(stringf("(define-fun |%s#%d#%d| ((state |%s_s|)) (_ BitVec %d) (concat%s)) ; %s\n",
+								get_id(module), arrayid, i+1, get_id(module), mem->width*mem->size, data_expr.c_str(), get_id(mem->memid)));
+					}
+				}
+				else
+				{
+					if (has_async_wr) {
+						if (statedt)
+							dtmembers.push_back(stringf("  (|%s| (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n",
+									initial_memstate.c_str(), abits, mem->width, get_id(mem->memid)));
+						else
+							decls.push_back(stringf("(declare-fun |%s| (|%s_s|) (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n",
+									initial_memstate.c_str(), get_id(module), abits, mem->width, get_id(mem->memid)));
+					}
 
-							std::string addr = get_bv(addr_sig);
-							std::string data = get_bv(data_sig);
-							std::string mask = get_bv(mask_sig);
+					for (int i = 0; i < GetSize(mem->wr_ports); i++)
+					{
+						auto &port = mem->wr_ports[i];
+						SigSpec addr_sig = port.addr;
+						addr_sig.extend_u0(abits);
 
-							decls.push_back(stringf("(define-fun |%s_m:W%dA %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
-									get_id(module), i, get_id(cell), get_id(module), abits, addr.c_str(), log_signal(addr_sig)));
-							addr = stringf("(|%s_m:W%dA %s| state)", get_id(module), i, get_id(cell));
+						std::string addr = get_bv(addr_sig);
+						std::string data = get_bv(port.data);
+						std::string mask = get_bv(port.en);
 
-							decls.push_back(stringf("(define-fun |%s_m:W%dD %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
-									get_id(module), i, get_id(cell), get_id(module), width, data.c_str(), log_signal(data_sig)));
-							data = stringf("(|%s_m:W%dD %s| state)", get_id(module), i, get_id(cell));
+						decls.push_back(stringf("(define-fun |%s_m:W%dA %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
+								get_id(module), i, get_id(mem->memid), get_id(module), abits, addr.c_str(), log_signal(addr_sig)));
+						addr = stringf("(|%s_m:W%dA %s| state)", get_id(module), i, get_id(mem->memid));
 
-							decls.push_back(stringf("(define-fun |%s_m:W%dM %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
-									get_id(module), i, get_id(cell), get_id(module), width, mask.c_str(), log_signal(mask_sig)));
-							mask = stringf("(|%s_m:W%dM %s| state)", get_id(module), i, get_id(cell));
+						decls.push_back(stringf("(define-fun |%s_m:W%dD %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
+								get_id(module), i, get_id(mem->memid), get_id(module), mem->width, data.c_str(), log_signal(port.data)));
+						data = stringf("(|%s_m:W%dD %s| state)", get_id(module), i, get_id(mem->memid));
 
-							std::string data_expr;
+						decls.push_back(stringf("(define-fun |%s_m:W%dM %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
+								get_id(module), i, get_id(mem->memid), get_id(module), mem->width, mask.c_str(), log_signal(port.en)));
+						mask = stringf("(|%s_m:W%dM %s| state)", get_id(module), i, get_id(mem->memid));
 
-							for (int k = mem_size-1; k >= 0; k--) {
-								std::string new_data = stringf("(bvor (bvand %s %s) (bvand ((_ extract %d %d) (|%s#%d#%d| state)) (bvnot %s)))",
-										data.c_str(), mask.c_str(), width*(k+1)-1, width*k, get_id(module), arrayid, i, mask.c_str());
-								data_expr += stringf("\n  (ite (= %s #b%s) %s ((_ extract %d %d) (|%s#%d#%d| state)))",
-										addr.c_str(), Const(k+mem_offset, abits).as_string().c_str(), new_data.c_str(),
-										width*(k+1)-1, width*k, get_id(module), arrayid, i);
-							}
+						data = stringf("(bvor (bvand %s %s) (bvand (select (|%s#%d#%d| state) %s) (bvnot %s)))",
+								data.c_str(), mask.c_str(), get_id(module), arrayid, i, addr.c_str(), mask.c_str());
 
-							decls.push_back(stringf("(define-fun |%s#%d#%d| ((state |%s_s|)) (_ BitVec %d) (concat%s)) ; %s\n",
-									get_id(module), arrayid, i+1, get_id(module), width*mem_size, data_expr.c_str(), get_id(cell)));
-						}
+						decls.push_back(stringf("(define-fun |%s#%d#%d| ((state |%s_s|)) (Array (_ BitVec %d) (_ BitVec %d)) "
+								"(store (|%s#%d#%d| state) %s %s)) ; %s\n",
+								get_id(module), arrayid, i+1, get_id(module), abits, mem->width,
+								get_id(module), arrayid, i, addr.c_str(), data.c_str(), get_id(mem->memid)));
 					}
-					else
-					{
-						if (async_read) {
-							if (statedt)
-								dtmembers.push_back(stringf("  (|%s| (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n",
-										initial_memstate.c_str(), abits, width, get_id(cell)));
-							else
-								decls.push_back(stringf("(declare-fun |%s| (|%s_s|) (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n",
-										initial_memstate.c_str(), get_id(module), abits, width, get_id(cell)));
-						}
-
-						for (int i = 0; i < wr_ports; i++)
-						{
-							SigSpec addr_sig = cell->getPort(ID::WR_ADDR).extract(abits*i, abits);
-							SigSpec data_sig = cell->getPort(ID::WR_DATA).extract(width*i, width);
-							SigSpec mask_sig = cell->getPort(ID::WR_EN).extract(width*i, width);
+				}
 
-							std::string addr = get_bv(addr_sig);
-							std::string data = get_bv(data_sig);
-							std::string mask = get_bv(mask_sig);
+				std::string expr_d = stringf("(|%s#%d#%d| state)", get_id(module), arrayid, GetSize(mem->wr_ports));
+				std::string expr_q = stringf("(|%s#%d#0| next_state)", get_id(module), arrayid);
+				trans.push_back(stringf("  (= %s %s) ; %s\n", expr_d.c_str(), expr_q.c_str(), get_id(mem->memid)));
+				ex_state_eq.push_back(stringf("(= (|%s#%d#0| state) (|%s#%d#0| other_state))", get_id(module), arrayid, get_id(module), arrayid));
 
-							decls.push_back(stringf("(define-fun |%s_m:W%dA %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
-									get_id(module), i, get_id(cell), get_id(module), abits, addr.c_str(), log_signal(addr_sig)));
-							addr = stringf("(|%s_m:W%dA %s| state)", get_id(module), i, get_id(cell));
+				if (has_async_wr)
+					hier.push_back(stringf("  (= %s (|%s| state)) ; %s\n", expr_d.c_str(), final_memstate.c_str(), get_id(mem->memid)));
 
-							decls.push_back(stringf("(define-fun |%s_m:W%dD %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
-									get_id(module), i, get_id(cell), get_id(module), width, data.c_str(), log_signal(data_sig)));
-							data = stringf("(|%s_m:W%dD %s| state)", get_id(module), i, get_id(cell));
+				Const init_data = mem->get_init_data();
 
-							decls.push_back(stringf("(define-fun |%s_m:W%dM %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
-									get_id(module), i, get_id(cell), get_id(module), width, mask.c_str(), log_signal(mask_sig)));
-							mask = stringf("(|%s_m:W%dM %s| state)", get_id(module), i, get_id(cell));
+				for (int i = 0; i < mem->size; i++)
+				{
+					if (i*mem->width >= GetSize(init_data))
+						break;
 
-							data = stringf("(bvor (bvand %s %s) (bvand (select (|%s#%d#%d| state) %s) (bvnot %s)))",
-									data.c_str(), mask.c_str(), get_id(module), arrayid, i, addr.c_str(), mask.c_str());
+					Const initword = init_data.extract(i*mem->width, mem->width, State::Sx);
+					Const initmask = initword;
+					bool gen_init_constr = false;
 
-							decls.push_back(stringf("(define-fun |%s#%d#%d| ((state |%s_s|)) (Array (_ BitVec %d) (_ BitVec %d)) "
-									"(store (|%s#%d#%d| state) %s %s)) ; %s\n",
-									get_id(module), arrayid, i+1, get_id(module), abits, width,
-									get_id(module), arrayid, i, addr.c_str(), data.c_str(), get_id(cell)));
+					for (int k = 0; k < GetSize(initword); k++) {
+						if (initword[k] == State::S0 || initword[k] == State::S1) {
+							gen_init_constr = true;
+							initmask[k] = State::S1;
+						} else {
+							initmask[k] = State::S0;
+							initword[k] = State::S0;
 						}
 					}
 
-					std::string expr_d = stringf("(|%s#%d#%d| state)", get_id(module), arrayid, wr_ports);
-					std::string expr_q = stringf("(|%s#%d#0| next_state)", get_id(module), arrayid);
-					trans.push_back(stringf("  (= %s %s) ; %s\n", expr_d.c_str(), expr_q.c_str(), get_id(cell)));
-					ex_state_eq.push_back(stringf("(= (|%s#%d#0| state) (|%s#%d#0| other_state))", get_id(module), arrayid, get_id(module), arrayid));
-
-					if (async_read)
-						hier.push_back(stringf("  (= %s (|%s| state)) ; %s\n", expr_d.c_str(), final_memstate.c_str(), get_id(cell)));
-
-					Const init_data = cell->getParam(ID::INIT);
-					int memsize = cell->getParam(ID::SIZE).as_int();
-
-					for (int i = 0; i < memsize; i++)
+					if (gen_init_constr)
 					{
-						if (i*width >= GetSize(init_data))
-							break;
-
-						Const initword = init_data.extract(i*width, width, State::Sx);
-						Const initmask = initword;
-						bool gen_init_constr = false;
-
-						for (int k = 0; k < GetSize(initword); k++) {
-							if (initword[k] == State::S0 || initword[k] == State::S1) {
-								gen_init_constr = true;
-								initmask[k] = State::S1;
-							} else {
-								initmask[k] = State::S0;
-								initword[k] = State::S0;
-							}
-						}
-
-						if (gen_init_constr)
-						{
-							if (statebv)
-								/* FIXME */;
-							else
-								init_list.push_back(stringf("(= (bvand (select (|%s#%d#0| state) #b%s) #b%s) #b%s) ; %s[%d]",
-										get_id(module), arrayid, Const(i, abits).as_string().c_str(),
-										initmask.as_string().c_str(), initword.as_string().c_str(), get_id(cell), i));
-						}
+						if (statebv)
+							/* FIXME */;
+						else
+							init_list.push_back(stringf("(= (bvand (select (|%s#%d#0| state) #b%s) #b%s) #b%s) ; %s[%d]",
+									get_id(module), arrayid, Const(i, abits).as_string().c_str(),
+									initmask.as_string().c_str(), initword.as_string().c_str(), get_id(mem->memid), i));
 					}
 				}
 			}
@@ -1586,7 +1644,7 @@ struct Smt2Backend : public Backend {
 
 		for (auto module : sorted_modules)
 		{
-			if (module->get_blackbox_attribute() || module->has_memories_warn() || module->has_processes_warn())
+			if (module->get_blackbox_attribute() || module->has_processes_warn())
 				continue;
 
 			log("Creating SMT-LIBv2 representation of module %s.\n", log_id(module));