From: Clifford Wolf <clifford@clifford.at>
Date: Wed, 2 Oct 2019 10:48:04 +0000 (+0200)
Subject: Fix btor back-end to use "state" instead of "input" for undef init bits
X-Git-Tag: working-ls180~1025^2
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a84a2d74c779b8023c0bbfc02fa4576d8c4cecca;p=yosys.git

Fix btor back-end to use "state" instead of "input" for undef init bits

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

diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc
index f617b7ec2..9e316a055 100644
--- a/backends/btor/btor.cc
+++ b/backends/btor/btor.cc
@@ -569,7 +569,7 @@ struct BtorWorker
 			int nid_init_val = -1;
 
 			if (!initval.is_fully_undef())
-				nid_init_val = get_sig_nid(initval);
+				nid_init_val = get_sig_nid(initval, -1, false, true);
 
 			int sid = get_bv_sid(GetSize(sig_q));
 			int nid = next_nid++;
@@ -681,7 +681,7 @@ struct BtorWorker
 				{
 					if (verbose)
 						btorf("; initval = %s\n", log_signal(firstword));
-					nid_init_val = get_sig_nid(firstword);
+					nid_init_val = get_sig_nid(firstword, -1, false, true);
 				}
 				else
 				{
@@ -693,8 +693,8 @@ struct BtorWorker
 						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 nid_thisword = get_sig_nid(thisword, -1, false, true);
+						int nid_thisaddr = get_sig_nid(thisaddr, -1, false, true);
 						int last_nid_init_val = nid_init_val;
 						nid_init_val = next_nid++;
 						if (verbose)
@@ -792,7 +792,7 @@ struct BtorWorker
 		cell_recursion_guard.erase(cell);
 	}
 
-	int get_sig_nid(SigSpec sig, int to_width = -1, bool is_signed = false)
+	int get_sig_nid(SigSpec sig, int to_width = -1, bool is_signed = false, bool is_init = false)
 	{
 		int nid = -1;
 		sigmap.apply(sig);
@@ -823,7 +823,10 @@ struct BtorWorker
 				int sid = get_bv_sid(GetSize(sig));
 
 				int nid_input = next_nid++;
-				btorf("%d input %d\n", nid_input, sid);
+				if (is_init)
+					btorf("%d state %d\n", nid_input, sid);
+				else
+					btorf("%d input %d\n", nid_input, sid);
 
 				int nid_masked_input;
 				if (sig_mask_undef.is_fully_ones()) {