From b75fa62e9b2a9f4410084fb1c80ceb23ed9d9c48 Mon Sep 17 00:00:00 2001
From: Jannis Harder <me@jix.one>
Date: Tue, 24 May 2022 17:18:53 +0200
Subject: [PATCH] verilog: fix $past's signedness
---
CHANGELOG | 3 +++
frontends/ast/genrtlil.cc | 2 +-
frontends/ast/simplify.cc | 1 +
tests/verilog/past_signedness.ys | 35 ++++++++++++++++++++++++++++++++
4 files changed, 40 insertions(+), 1 deletion(-)
create mode 100644 tests/verilog/past_signedness.ys
diff --git a/CHANGELOG b/CHANGELOG
index ff7ce49a2..d64d592d2 100644
--- 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 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