Make sure to apply correct signedness to loop vars.

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

tests/verilog/issue4402.ys

@@ -0,0 +1,32 @@
+# Issue #4402: read_verilog doesn't respect signed keyword
+#
+# write_verilog was not emitting the signed keyword for port declarations.
+# Uses the original reproduction module from the issue (var2/var3 given
+# initial values of 0, which were uninitialized/assumed-zero in the report).
+#
+# Pre-synthesis simulation:  wire0=1'b1 (signed -1), -1<=0 true -> y=0
+# Post-synthesis (unfixed):  wire0 loses signed, 1<=0 false -> y=1  (BUG)
+# Post-synthesis (fixed):    wire0 retains signed, -1<=0 true -> y=0
+
+! mkdir -p temp
+
+read_verilog <<EOT
+module top (y, clk, wire0);
+  output wire y;
+  input wire clk;
+  input wire signed wire0;
+  reg reg1;
+  reg var2 = 0;
+  reg var3 = 0;
+  assign y = reg1;
+  always @(posedge clk) begin
+    reg1 = ($signed(wire0 <= 0) ? $unsigned(-var3) : (^~$signed(var2)));
+  end
+endmodule
+EOT
+hierarchy -top top
+proc
+write_verilog temp/issue4402_syn.v
+
+# Port declaration must include the signed keyword.
+! grep -q "input signed wire0" temp/issue4402_syn.v