From 14dbf70074e393daaeca111ad8751e0a79b5ddd6 Mon Sep 17 00:00:00 2001
From: Gus Smith <guscomps@gmail.com>
Date: Mon, 20 Apr 2026 18:56:04 -0700
Subject: [PATCH] Make sure to apply correct signedness to loop vars

---
 frontends/ast/simplify.cc              | 28 ++++++++-----
 tests/verilog/for_loop_signed_index.ys | 56 ++++++++++++++++++++++++++
 2 files changed, 73 insertions(+), 11 deletions(-)
 create mode 100644 tests/verilog/for_loop_signed_index.ys

diff --git a/frontends/ast/simplify.cc b/frontends/ast/simplify.cc
index 48a4291d2..e876cf48c 100644
--- a/frontends/ast/simplify.cc
+++ b/frontends/ast/simplify.cc
@@ -2619,21 +2619,26 @@ bool AstNode::simplify(bool const_fold, int stage, int width_hint, bool sign_hin
 			input_error("Right hand side of 1st expression of %s for-loop is not constant!\n", loop_type_str);
 
 		auto resolved = current_scope.at(init_ast->children[0]->str);
-		if (resolved->range_valid) {
-			int const_size = varbuf->range_left - varbuf->range_right;
-			int resolved_size = resolved->range_left - resolved->range_right;
-			if (const_size < resolved_size) {
-				for (int i = const_size; i < resolved_size; i++)
-					varbuf->bits.push_back(resolved->is_signed ? varbuf->bits.back() : State::S0);
-				varbuf->range_left = resolved->range_left;
-				varbuf->range_right = resolved->range_right;
-				varbuf->range_swapped = resolved->range_swapped;
-				varbuf->range_valid = resolved->range_valid;
+		auto apply_loop_var_type = [&resolved](std::unique_ptr<AstNode> &value) {
+			if (resolved->range_valid) {
+				int const_size = value->range_left - value->range_right;
+				int resolved_size = resolved->range_left - resolved->range_right;
+				if (const_size < resolved_size) {
+					for (int i = const_size; i < resolved_size; i++)
+						value->bits.push_back(resolved->is_signed ? value->bits.back() : State::S0);
+					value->range_left = resolved->range_left;
+					value->range_right = resolved->range_right;
+					value->range_swapped = resolved->range_swapped;
+					value->range_valid = resolved->range_valid;
+				}
 			}
-		}
+			value->is_signed = resolved->is_signed;
+		};
+		apply_loop_var_type(varbuf);
 
 		varbuf = std::make_unique<AstNode>(location, AST_LOCALPARAM, std::move(varbuf));
 		varbuf->str = init_ast->children[0]->str;
+		varbuf->is_signed = resolved->is_signed;
 
 		AstNode *backup_scope_varbuf = current_scope[varbuf->str];
 		current_scope[varbuf->str] = varbuf.get();
@@ -2708,6 +2713,7 @@ bool AstNode::simplify(bool const_fold, int stage, int width_hint, bool sign_hin
 			if (buf->type != AST_CONSTANT)
 				input_error("Right hand side of 3rd expression of %s for-loop is not constant (%s)!\n", loop_type_str, type2str(buf->type));
 
+			apply_loop_var_type(buf);
 			varbuf->children[0] = std::move(buf);
 		}
 
diff --git a/tests/verilog/for_loop_signed_index.ys b/tests/verilog/for_loop_signed_index.ys
new file mode 100644
index 000000000..87e6b14cb
--- /dev/null
+++ b/tests/verilog/for_loop_signed_index.ys
@@ -0,0 +1,56 @@
+# Regression test: when procedural for-loops are unrolled, the constant
+# replacement for the loop variable must keep the variable's declared
+# signedness.
+
+read_verilog <<EOT
+module signed_index(input signed a, output reg y);
+  reg signed i;
+
+  always @*
+    for (i = 1'h0; i < 1'h1; i = i + 1'h1)
+      y = a <= i;
+endmodule
+
+EOT
+
+hierarchy -top signed_index
+proc
+sat -set a 1 -prove y 1 -verify
+
+design -reset
+
+# This loop runs more than once. The final assignment to y happens after the
+# step expression has recomputed i, so it fails unless the stepped value is
+# retagged with the loop variable's signedness too.
+read_verilog <<EOT
+module signed_index_after_step(input signed a, output reg y);
+  reg signed [1:0] i;
+
+  always @* begin
+    y = 1'b0;
+    for (i = -2'sd1; i < 2'sd1; i = i + 1'h1)
+      y = a <= i;
+  end
+endmodule
+EOT
+
+hierarchy -top signed_index_after_step
+proc
+sat -set a 1 -prove y 1 -verify
+
+design -reset
+
+# Control: `a` signed but `i` unsigned, so comparison should be unsigned.
+read_verilog <<EOT
+module unsigned_index(input signed a, output reg y);
+  reg i;
+
+  always @*
+    for (i = 1'h0; i < 1'h1; i = i + 1'h1)
+      y = a <= i;
+endmodule
+EOT
+
+hierarchy -top unsigned_index
+proc
+sat -set a 1 -prove y 0 -verify