diff --git a/backends/verilog/verilog_backend.cc b/backends/verilog/verilog_backend.cc
index 73ffcbf3e..d5f83aefc 100644
--- a/backends/verilog/verilog_backend.cc
+++ b/backends/verilog/verilog_backend.cc
@@ -456,21 +456,22 @@ void dump_wire(std::ostream &f, std::string indent, RTLIL::Wire *wire)
 		if (wire->attributes.count(ID::single_bit_vector))
 			range = stringf(" [%d:%d]", wire->start_offset, wire->start_offset);
 	}
+	std::string sign = wire->is_signed ? " signed" : "";
 	if (wire->port_input && !wire->port_output)
-		f << stringf("%s" "input%s %s;\n", indent, range, id(wire->name));
+		f << stringf("%s" "input%s%s %s;\n", indent, sign, range, id(wire->name));
 	if (!wire->port_input && wire->port_output)
-		f << stringf("%s" "output%s %s;\n", indent, range, id(wire->name));
+		f << stringf("%s" "output%s%s %s;\n", indent, sign, range, id(wire->name));
 	if (wire->port_input && wire->port_output)
-		f << stringf("%s" "inout%s %s;\n", indent, range, id(wire->name));
+		f << stringf("%s" "inout%s%s %s;\n", indent, sign, range, id(wire->name));
 	if (reg_wires.count(wire->name)) {
-		f << stringf("%s" "reg%s %s", indent, range, id(wire->name));
+		f << stringf("%s" "reg%s%s %s", indent, sign, range, id(wire->name));
 		if (wire->attributes.count(ID::init)) {
 			f << stringf(" = ");
 			dump_const(f, wire->attributes.at(ID::init));
 		}
 		f << stringf(";\n");
 	} else
-		f << stringf("%s" "wire%s %s;\n", indent, range, id(wire->name));
+		f << stringf("%s" "wire%s%s %s;\n", indent, sign, range, id(wire->name));
 #endif
 }
 
diff --git a/frontends/ast/simplify.cc b/frontends/ast/simplify.cc
index f314ff3d5..ffe8f859c 100644
--- a/frontends/ast/simplify.cc
+++ b/frontends/ast/simplify.cc
@@ -2591,21 +2591,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();
@@ -2680,6 +2685,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
diff --git a/tests/verilog/issue4402.ys b/tests/verilog/issue4402.ys
new file mode 100644
index 000000000..f5ddca7d2
--- /dev/null
+++ b/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
diff --git a/tests/verilog/issue4402_sim.sh b/tests/verilog/issue4402_sim.sh
new file mode 100755
index 000000000..470650613
--- /dev/null
+++ b/tests/verilog/issue4402_sim.sh
@@ -0,0 +1,55 @@
+#!/usr/bin/env bash
+# Simulation regression for issue #4402.
+# Confirms pre- and post-synthesis outputs match for a module with a signed input port.
+# Requires iverilog/vvp in PATH. Skips if not found.
+set -e
+
+if ! command -v iverilog > /dev/null 2>&1; then
+    echo "SKIP: iverilog not found"
+    exit 0
+fi
+
+SCRIPT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"
+YOSYS="${YOSYS:-$SCRIPT_DIR/../../yosys}"
+TMPDIR="$(mktemp -d)"
+trap 'rm -rf "$TMPDIR"' EXIT
+
+cat > "$TMPDIR/top.v" << 'EOF'
+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
+EOF
+
+# Synthesize
+"$YOSYS" -q -p "
+read_verilog $TMPDIR/top.v
+hierarchy -top top
+proc
+write_verilog $TMPDIR/top_syn.v
+"
+
+# Simulate original
+iverilog -o "$TMPDIR/sim_orig" "$SCRIPT_DIR/issue4402_tb.v" "$TMPDIR/top.v" 2>/dev/null
+# Simulate synthesized
+iverilog -o "$TMPDIR/sim_syn"  "$SCRIPT_DIR/issue4402_tb.v" "$TMPDIR/top_syn.v" 2>/dev/null
+
+ORIG=$(vvp "$TMPDIR/sim_orig" 2>/dev/null | grep "y =")
+SYN=$(vvp  "$TMPDIR/sim_syn"  2>/dev/null | grep "y =")
+
+echo "Original:    $ORIG"
+echo "Synthesized: $SYN"
+
+if [ "$ORIG" != "$SYN" ]; then
+    echo "FAIL: pre/post-synthesis outputs differ"
+    exit 1
+fi
+echo "PASS"
diff --git a/tests/verilog/issue4402_tb.v b/tests/verilog/issue4402_tb.v
new file mode 100644
index 000000000..4faee54b9
--- /dev/null
+++ b/tests/verilog/issue4402_tb.v
@@ -0,0 +1,20 @@
+`timescale 1ns / 1ps
+module testbench;
+  reg clk;
+  reg signed [5:0] wire0;
+  wire y;
+
+  top uut (.y(y), .clk(clk), .wire0(wire0));
+
+  initial begin
+    clk = 0;
+    wire0 = 6'b111101;
+    forever #5 clk = ~clk;
+  end
+
+  initial begin
+    #100;
+    $display("y = %d", y);
+    $finish;
+  end
+endmodule
diff --git a/tests/verilog/issue5745.ys b/tests/verilog/issue5745.ys
new file mode 100644
index 000000000..1e16b8373
--- /dev/null
+++ b/tests/verilog/issue5745.ys
@@ -0,0 +1,18 @@
+# Issue #5745: chparam values are unsigned when using read_verilog frontend
+#
+# When chparam overrides a parameter value, the signed attribute is lost,
+# causing signed comparisons to silently use unsigned logic.
+#
+# m = -32 (signed 9-bit), p2 = 11. Correct signed semantics: -32 < 11, so k = 1.
+# Bug: chparam strips the signed attribute from p2. The $lt cell gets A_SIGNED=0,
+# B_SIGNED=0, so the comparison treats m as unsigned (480 > 11), giving k = 0.
+
+read_verilog <<EOT
+module mod #(parameter p2=11) (output k);
+  wire signed [8:0] m = -32;
+  assign k = m < p2;
+endmodule
+EOT
+chparam -set p2 11
+hierarchy -top mod
+sat -prove k 1 -verify