Merge pull request #893 from YosysHQ/clifford/btormeminit

Memory init support in write_btor

3 files changed, 63 insertions, 3 deletions

diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc
index 53359bd7b..55c494996 100644
--- a/backends/btor/btor.cc
+++ b/backends/btor/btor.cc
@@ -615,6 +615,7 @@ struct BtorWorker
 		{
 			int abits = cell->getParam("\\ABITS").as_int();
 			int width = cell->getParam("\\WIDTH").as_int();
+			int nwords = cell->getParam("\\SIZE").as_int();
 			int rdports = cell->getParam("\\RD_PORTS").as_int();
 			int wrports = cell->getParam("\\WR_PORTS").as_int();
 
@@ -641,6 +642,52 @@ struct BtorWorker
 			int data_sid = get_bv_sid(width);
 			int bool_sid = get_bv_sid(1);
 			int sid = get_mem_sid(abits, width);
+
+			Const initdata = cell->getParam("\\INIT");
+			initdata.exts(nwords*width);
+			int nid_init_val = -1;
+
+			if (!initdata.is_fully_undef())
+			{
+				bool constword = true;
+				Const firstword = initdata.extract(0, width);
+
+				for (int i = 1; i < nwords; i++) {
+					Const thisword = initdata.extract(i*width, width);
+					if (thisword != firstword) {
+						constword = false;
+						break;
+					}
+				}
+
+				if (constword)
+				{
+					if (verbose)
+						btorf("; initval = %s\n", log_signal(firstword));
+					nid_init_val = get_sig_nid(firstword);
+				}
+				else
+				{
+					int 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);
+						if (thisword.is_fully_undef())
+							continue;
+						Const thisaddr(i, abits);
+						int nid_thisword = get_sig_nid(thisword);
+						int nid_thisaddr = get_sig_nid(thisaddr);
+						int last_nid_init_val = nid_init_val;
+						nid_init_val = next_nid++;
+						if (verbose)
+							btorf("; initval[%d] = %s\n", i, log_signal(thisword));
+						btorf("%d write %d %d %d %d\n", nid_init_val, sid, last_nid_init_val, nid_thisaddr, nid_thisword);
+					}
+				}
+			}
+
+
 			int nid = next_nid++;
 			int nid_head = nid;
 
@@ -649,6 +696,12 @@ struct BtorWorker
 			else
 				btorf("%d state %d %s\n", nid, sid, log_id(cell));
 
+			if (nid_init_val >= 0)
+			{
+				int nid_init = next_nid++;
+				btorf("%d init %d %d %d\n", nid_init, sid, nid, nid_init_val);
+			}
+
 			if (asyncwr)
 			{
 				for (int port = 0; port < wrports; port++)
@@ -932,9 +985,8 @@ struct BtorWorker
 
 			btorf_push(stringf("output %s", log_id(wire)));
 
-			int sid = get_bv_sid(GetSize(wire));
 			int nid = get_sig_nid(wire);
-			btorf("%d output %d %d %s\n", next_nid++, sid, nid, log_id(wire));
+			btorf("%d output %d %s\n", next_nid++, nid, log_id(wire));
 
 			btorf_pop(stringf("output %s", log_id(wire)));
 		}
diff --git a/kernel/rtlil.cc b/kernel/rtlil.cc
index d0fa88890..b3214579d 100644
--- a/kernel/rtlil.cc
+++ b/kernel/rtlil.cc
@@ -3237,7 +3237,7 @@ void RTLIL::SigSpec::extend_u0(int width, bool is_signed)
 		remove(width, width_ - width);
 
 	if (width_ < width) {
-		RTLIL::SigBit padding = width_ > 0 ? (*this)[width_ - 1] : RTLIL::State::S0;
+		RTLIL::SigBit padding = width_ > 0 ? (*this)[width_ - 1] : RTLIL::State::Sx;
 		if (!is_signed)
 			padding = RTLIL::State::S0;
 		while (width_ < width)
diff --git a/kernel/rtlil.h b/kernel/rtlil.h
index 01323d112..52496e702 100644
--- a/kernel/rtlil.h
+++ b/kernel/rtlil.h
@@ -546,6 +546,14 @@ struct RTLIL::Const
 		return ret;
 	}
 
+	void extu(int width) {
+		bits.resize(width, RTLIL::State::S0);
+	}
+
+	void exts(int width) {
+		bits.resize(width, bits.empty() ? RTLIL::State::Sx : bits.back());
+	}
+
 	inline unsigned int hash() const {
 		unsigned int h = mkhash_init;
 		for (auto b : bits)