verilog: fix $past's signedness

diff --git a/CHANGELOG b/CHANGELOG
index ff7ce49a25ae6c9df6dc70d14b1a6cf7435661d3..d64d592d292fb5dfca9720315cdf9cb17089a803 100644 (file)
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -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 020b4e5e893dadd39e24d07b498b7c4b66e0de35..6ef7da7a953e9fe94661cdcee1efc9d83a34d83c 100644 (file)
--- 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 4d7c4f5221429aa977a425ddf2fd9a43d8199e6a..c2adcafd0e05a6a0333aa3511cc430d6c3ca8b64 100644 (file)
--- 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 (file)
index 0000000..91f3232
--- /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