From: Clifford Wolf <clifford@clifford.at>
Date: Thu, 1 Dec 2016 11:00:00 +0000 (+0100)
Subject: Added support for partially initialized regs to smt2 back-end
X-Git-Tag: yosys-0.8~568
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=52c243cf05c331ef2c1ce01416e85f2fb8a70a33;p=yosys.git

Added support for partially initialized regs to smt2 back-end
---

diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index 43479eb55..e0daae728 100644
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -639,12 +639,24 @@ struct Smt2Worker
 			if (wire->attributes.count("\\init")) {
 				RTLIL::SigSpec sig = sigmap(wire);
 				Const val = wire->attributes.at("\\init");
-				val.bits.resize(GetSize(sig));
+				val.bits.resize(GetSize(sig), State::Sx);
 				if (bvmode && GetSize(sig) > 1) {
-					init_list.push_back(stringf("(= %s #b%s) ; %s", get_bv(sig).c_str(), val.as_string().c_str(), get_id(wire)));
+					Const mask(State::S1, GetSize(sig));
+					bool use_mask = false;
+					for (int i = 0; i < GetSize(sig); i++)
+						if (val[i] != State::S0 && val[i] != State::S1) {
+							val[i] = State::S0;
+							mask[i] = State::S0;
+							use_mask = true;
+						}
+					if (use_mask)
+						init_list.push_back(stringf("(= (bvand %s #b%s) #b%s) ; %s", get_bv(sig).c_str(), mask.as_string().c_str(), val.as_string().c_str(), get_id(wire)));
+					else
+						init_list.push_back(stringf("(= %s #b%s) ; %s", get_bv(sig).c_str(), val.as_string().c_str(), get_id(wire)));
 				} else {
 					for (int i = 0; i < GetSize(sig); i++)
-						init_list.push_back(stringf("(= %s %s) ; %s", get_bool(sig[i]).c_str(), val.bits[i] == State::S1 ? "true" : "false", get_id(wire)));
+						if (val[i] == State::S0 || val[i] == State::S1)
+							init_list.push_back(stringf("(= %s %s) ; %s", get_bool(sig[i]).c_str(), val[i] == State::S1 ? "true" : "false", get_id(wire)));
 				}
 			}