diff options
| -rw-r--r-- | CHANGELOG | 3 | ||||
| -rw-r--r-- | frontends/ast/genrtlil.cc | 2 | ||||
| -rw-r--r-- | frontends/ast/simplify.cc | 1 | ||||
| -rw-r--r-- | tests/verilog/past_signedness.ys | 35 |
4 files changed, 40 insertions, 1 deletions
@@ -4,6 +4,9 @@ List of major changes and improvements between releases Yosys 0.17 .. Yosys 0.17-dev -------------------------- + * Formal Verification + - Fixed the signedness of $past's return value to be the same as the + argument's instead of always unsigned. * Verilog - Fixed an issue where simplifying case statements by removing unreachable diff --git a/frontends/ast/genrtlil.cc b/frontends/ast/genrtlil.cc index 020b4e5e8..6ef7da7a9 100644 --- a/frontends/ast/genrtlil.cc +++ b/frontends/ast/genrtlil.cc @@ -1084,7 +1084,7 @@ void AstNode::detectSignWidthWorker(int &width_hint, bool &sign_hint, bool *foun sub_sign_hint = true; children.at(0)->detectSignWidthWorker(sub_width_hint, sub_sign_hint); width_hint = max(width_hint, sub_width_hint); - sign_hint = false; + sign_hint &= sub_sign_hint; } break; } diff --git a/frontends/ast/simplify.cc b/frontends/ast/simplify.cc index 4d7c4f522..c2adcafd0 100644 --- a/frontends/ast/simplify.cc +++ b/frontends/ast/simplify.cc @@ -3230,6 +3230,7 @@ skip_dynamic_range_lvalue_expansion:; reg->str = stringf("$past$%s:%d$%d$%d", filename.c_str(), location.first_line, myidx, i); reg->is_reg = true; + reg->is_signed = sign_hint; current_ast_mod->children.push_back(reg); diff --git a/tests/verilog/past_signedness.ys b/tests/verilog/past_signedness.ys new file mode 100644 index 000000000..91f32328b --- /dev/null +++ b/tests/verilog/past_signedness.ys @@ -0,0 +1,35 @@ +logger -expect-no-warnings + +read_verilog -formal <<EOT +module top(input clk); + reg signed [3:0] value = -1; + reg ready = 0; + + always @(posedge clk) begin + if (ready) + assert ($past(value) == -1); + ready <= 1; + end +endmodule +EOT + +prep -top top +sim -n 3 -clock clk + +design -reset + +read_verilog -formal <<EOT +module top(input clk); + reg signed [3:0] value = -1; + reg ready = 0; + + always @(posedge clk) begin + if (ready) + assert ($past(value + 4'b0000) == 15); + ready <= 1; + end +endmodule +EOT + +prep -top top +sim -n 3 -clock clk |