From: Clifford Wolf <clifford@clifford.at>
Date: Thu, 28 Feb 2019 20:15:58 +0000 (-0800)
Subject: Fix smt2 code generation for partially initialized memowy words, fixes #831
X-Git-Tag: yosys-0.9~294^2
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f570aa5e1d3ac201089da2198f8e5084185fd92f;p=yosys.git

Fix smt2 code generation for partially initialized memowy words, fixes #831

Signed-off-by: Clifford Wolf <clifford@clifford.at>
---

diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index 418f8d766..7f3cc94ca 100644
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -1103,20 +1103,27 @@ struct Smt2Worker
 							break;
 
 						Const initword = init_data.extract(i*width, width, State::Sx);
+						Const initmask = initword;
 						bool gen_init_constr = false;
 
-						for (auto bit : initword.bits)
-							if (bit == State::S0 || bit == State::S1)
+						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("(= (select (|%s#%d#0| state) #b%s) #b%s) ; %s[%d]",
+								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(),
-										initword.as_string().c_str(), get_id(cell), i));
+										initmask.as_string().c_str(), initword.as_string().c_str(), get_id(cell), i));
 						}
 					}
 				}