From 0221f3e1c5b427678c5679027ee47ec7c0b8321d Mon Sep 17 00:00:00 2001
From: Eddie Hung <eddie@fpgeh.com>
Date: Thu, 20 Jun 2019 10:04:42 -0700
Subject: [PATCH 1/3] Fix sign extension when sign is 1'bx

---
 kernel/rtlil.cc | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/kernel/rtlil.cc b/kernel/rtlil.cc
index a09f4a0d1..95a24c93f 100644
--- a/kernel/rtlil.cc
+++ b/kernel/rtlil.cc
@@ -3437,7 +3437,7 @@ void RTLIL::SigSpec::extend_u0(int width, bool is_signed)
 
 	if (width_ < width) {
 		RTLIL::SigBit padding = width_ > 0 ? (*this)[width_ - 1] : RTLIL::State::Sx;
-		if (!is_signed)
+		if (padding != RTLIL::State::Sx && !is_signed)
 			padding = RTLIL::State::S0;
 		while (width_ < width)
 			append(padding);

From b98276fa61be7a1c589d6dac661d31982cfab16b Mon Sep 17 00:00:00 2001
From: Eddie Hung <eddie@fpgeh.com>
Date: Thu, 20 Jun 2019 10:10:43 -0700
Subject: [PATCH 2/3] Add test

---
 tests/various/signext.ys | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)
 create mode 100644 tests/various/signext.ys

diff --git a/tests/various/signext.ys b/tests/various/signext.ys
new file mode 100644
index 000000000..26dab13a6
--- /dev/null
+++ b/tests/various/signext.ys
@@ -0,0 +1,24 @@
+
+read_verilog -formal <<EOT
+module gate(input clk, output [1:0] o);
+assign o = 1'bx;
+endmodule
+EOT
+
+
+## Example usage for "pmuxtree" and "muxcover"
+
+proc
+
+## Equivalence checking
+
+read_verilog -formal <<EOT
+module gold(input clk, output [1:0] o);
+assign o = 2'bxx;
+endmodule
+EOT
+
+proc
+
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -verify -prove-asserts -show-ports -enable_undef miter

From b77322034c9234a8c24c6f53ed028fe29737b6b4 Mon Sep 17 00:00:00 2001
From: Eddie Hung <eddie@fpgeh.com>
Date: Thu, 20 Jun 2019 10:15:04 -0700
Subject: [PATCH 3/3] Remove leftover comment

---
 tests/various/signext.ys | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/tests/various/signext.ys b/tests/various/signext.ys
index 26dab13a6..ae44a0e06 100644
--- a/tests/various/signext.ys
+++ b/tests/various/signext.ys
@@ -5,9 +5,6 @@ assign o = 1'bx;
 endmodule
 EOT
 
-
-## Example usage for "pmuxtree" and "muxcover"
-
 proc
 
 ## Equivalence checking