diff options
| -rw-r--r-- | CHANGELOG | 3 | ||||
| -rw-r--r-- | backends/aiger/aiger.cc | 3 | ||||
| -rw-r--r-- | frontends/verilog/const2ast.cc | 12 | ||||
| -rw-r--r-- | tests/various/signext.ys | 33 |
4 files changed, 43 insertions, 8 deletions
@@ -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 diff --git a/backends/aiger/aiger.cc b/backends/aiger/aiger.cc index d685c5638..6863b40fa 100644 --- a/backends/aiger/aiger.cc +++ b/backends/aiger/aiger.cc @@ -89,7 +89,8 @@ struct AigerWriter aig_map[bit] = mkgate(a0, a1); } else if (alias_map.count(bit)) { - aig_map[bit] = bit2aig(alias_map.at(bit)); + int a = bit2aig(alias_map.at(bit)); + aig_map[bit] = a; } if (bit == State::Sx || bit == State::Sz) diff --git a/frontends/verilog/const2ast.cc b/frontends/verilog/const2ast.cc index 57d366dbf..3a3634d34 100644 --- a/frontends/verilog/const2ast.cc +++ b/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; } diff --git a/tests/various/signext.ys b/tests/various/signext.ys new file mode 100644 index 000000000..0c8d671e7 --- /dev/null +++ b/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 |