Merge pull request #1116 from YosysHQ/eddie/fix1115

Sign extend unsized 'bx and 'bz values

CHANGELOG

@@ -19,6 +19,7 @@ Yosys 0.8 .. Yosys 0.8-dev
     - Added "read_aiger" frontend
     - Extended "muxcover -mux{4,8,16}=<cost>"
     - "synth_xilinx" to now infer hard shift registers, using new "shregmap -tech xilinx"
+    - Fixed sign extension of unsized constants with 'bx and 'bz MSB
 
 
 Yosys 0.7 .. Yosys 0.8
@@ -32,7 +33,7 @@ Yosys 0.7 .. Yosys 0.8
     - Added "write_verilog -decimal"
     - Added "scc -set_attr"
     - Added "verilog_defines" command
-    - Remeber defines from one read_verilog to next
+    - Remember defines from one read_verilog to next
     - Added support for hierarchical defparam
     - Added FIRRTL back-end
     - Improved ABC default scripts

frontends/verilog/const2ast.cc

@@ -204,7 +204,7 @@ AstNode *VERILOG_FRONTEND::const2ast(std::string code, char case_type, bool warn
 	{
 		std::vector<RTLIL::State> data;
 		bool is_signed = false;
-		bool is_unsized = false;
+		bool is_unsized = len_in_bits < 0;
 		if (*(endptr+1) == 's') {
 			is_signed = true;
 			endptr++;
@@ -213,25 +213,25 @@ AstNode *VERILOG_FRONTEND::const2ast(std::string code, char case_type, bool warn
 		{
 		case 'b':
 		case 'B':
-			my_strtobin(data, endptr+2, len_in_bits, 2, case_type, false);
+			my_strtobin(data, endptr+2, len_in_bits, 2, case_type, is_unsized);
 			break;
 		case 'o':
 		case 'O':
-			my_strtobin(data, endptr+2, len_in_bits, 8, case_type, false);
+			my_strtobin(data, endptr+2, len_in_bits, 8, case_type, is_unsized);
 			break;
 		case 'd':
 		case 'D':
-			my_strtobin(data, endptr+2, len_in_bits, 10, case_type, false);
+			my_strtobin(data, endptr+2, len_in_bits, 10, case_type, is_unsized);
 			break;
 		case 'h':
 		case 'H':
-			my_strtobin(data, endptr+2, len_in_bits, 16, case_type, false);
+			my_strtobin(data, endptr+2, len_in_bits, 16, case_type, is_unsized);
 			break;
 		default:
 			char next_char = char(tolower(*(endptr+1)));
 			if (next_char == '0' || next_char == '1' || next_char == 'x' || next_char == 'z') {
-				my_strtobin(data, endptr+1, 1, 2, case_type, true);
 				is_unsized = true;
+				my_strtobin(data, endptr+1, 1, 2, case_type, is_unsized);
 			} else {
 				return NULL;
 			}

tests/various/signext.ys

@@ -0,0 +1,33 @@
+
+read_verilog -formal <<EOT
+module gate(input clk, output [32:0] o, p, q, r, s, t, u);
+assign o = 'bx;
+assign p = 1'bx;
+assign q = 'bz;
+assign r = 1'bz;
+assign s = 1'b0;
+assign t = 'b1;
+assign u = -'sb1;
+endmodule
+EOT
+
+proc
+
+## Equivalence checking
+
+read_verilog -formal <<EOT
+module gold(input clk, output [32:0] o, p, q, r, s, t, u);
+assign o = {33{1'bx}};
+assign p = {{32{1'b0}}, 1'bx};
+assign q = {33{1'bz}};
+assign r = {{32{1'b0}}, 1'bz};
+assign s = {33{1'b0}};
+assign t = {{32{1'b0}}, 1'b1};
+assign u = {33{1'b1}};
+endmodule
+EOT
+
+proc
+
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -verify -prove-asserts -show-ports -enable_undef miter