From e75ca29b19e230bc829a369c7de9cbadb629f5a7 Mon Sep 17 00:00:00 2001
From: Eddie Hung <eddie@fpgeh.com>
Date: Wed, 11 Dec 2019 11:26:54 -0800
Subject: [PATCH 1/4] Add test: 'Warning: ignoring initial value on
 non-register: \o'

---
 tests/sat/initval.ys | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/tests/sat/initval.ys b/tests/sat/initval.ys
index 2079d2f34..337aa9343 100644
--- a/tests/sat/initval.ys
+++ b/tests/sat/initval.ys
@@ -2,3 +2,13 @@ read_verilog -sv initval.v
 proc;;
 
 sat -seq 10 -prove-asserts
+
+design -reset
+read_verilog -icells <<EOT
+module top(input clk, i, output o, p);
+(* init = 1'bx *)
+wire p = o;
+$_DFF_P_ dff (.C(clk), .D(i), .Q(o));
+endmodule
+EOT
+sat -seq 1

From 9a892199f72bb08f78c868fe8ab5b8a63cf25f37 Mon Sep 17 00:00:00 2001
From: Eddie Hung <eddie@fpgeh.com>
Date: Wed, 11 Dec 2019 11:27:10 -0800
Subject: [PATCH 2/4] Suppress warning message for init[i] = 1'bx

---
 passes/sat/sat.cc | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc
index 430bba1e8..436ac1b01 100644
--- a/passes/sat/sat.cc
+++ b/passes/sat/sat.cc
@@ -269,7 +269,8 @@ struct SatHelper
 				for (int i = 0; i < lhs.size(); i++) {
 					RTLIL::SigSpec bit = lhs.extract(i, 1);
 					if (rhs[i] == State::Sx || !satgen.initial_state.check_all(bit)) {
-						removed_bits.append(bit);
+						if (rhs[i] != State::Sx)
+							removed_bits.append(bit);
 						lhs.remove(i, 1);
 						rhs.remove(i, 1);
 						i--;

From 61a1f3f49b7bd0478b92c0933c487af5803c53f9 Mon Sep 17 00:00:00 2001
From: Eddie Hung <eddie@fpgeh.com>
Date: Wed, 11 Dec 2019 23:48:09 -0800
Subject: [PATCH 3/4] Make testcase clearer with \o having its own init

---
 tests/sat/initval.ys | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/tests/sat/initval.ys b/tests/sat/initval.ys
index 337aa9343..6cb68a8d3 100644
--- a/tests/sat/initval.ys
+++ b/tests/sat/initval.ys
@@ -6,6 +6,8 @@ sat -seq 10 -prove-asserts
 design -reset
 read_verilog -icells <<EOT
 module top(input clk, i, output o, p);
+(* init = 1'b0 *)
+wire o;
 (* init = 1'bx *)
 wire p = o;
 $_DFF_P_ dff (.C(clk), .D(i), .Q(o));

From 4a805108776f563bcd7550d1331a73a50512fbe2 Mon Sep 17 00:00:00 2001
From: Eddie Hung <eddie@fpgeh.com>
Date: Wed, 11 Dec 2019 23:52:05 -0800
Subject: [PATCH 4/4] Even more obvious testcase

---
 tests/sat/initval.ys | 11 +++++------
 1 file changed, 5 insertions(+), 6 deletions(-)

diff --git a/tests/sat/initval.ys b/tests/sat/initval.ys
index 6cb68a8d3..1436724b0 100644
--- a/tests/sat/initval.ys
+++ b/tests/sat/initval.ys
@@ -5,12 +5,11 @@ sat -seq 10 -prove-asserts
 
 design -reset
 read_verilog -icells <<EOT
-module top(input clk, i, output o, p);
-(* init = 1'b0 *)
-wire o;
-(* init = 1'bx *)
-wire p = o;
-$_DFF_P_ dff (.C(clk), .D(i), .Q(o));
+module top(input clk, i, output [1:0] o);
+(* init = 2'bx0 *)
+wire [1:0] o;
+assign o[1] = o[0];
+$_DFF_P_ dff (.C(clk), .D(i), .Q(o[0]));
 endmodule
 EOT
 sat -seq 1