From 70291f0e4954a81dfae5a236ecafda9abc43e5f7 Mon Sep 17 00:00:00 2001
From: George Rennie <georgerennie@gmail.com>
Date: Fri, 30 May 2025 14:25:35 +0100
Subject: [PATCH 1/5] read_verilog: fix -1 constant used to correct post
 increment/decrement

---
 frontends/verilog/verilog_parser.y | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/frontends/verilog/verilog_parser.y b/frontends/verilog/verilog_parser.y
index 9d0956c8e..fa624d471 100644
--- a/frontends/verilog/verilog_parser.y
+++ b/frontends/verilog/verilog_parser.y
@@ -336,7 +336,8 @@ static AstNode *addIncOrDecExpr(AstNode *lhs, dict<IdString, AstNode*> *attr, AS
 	log_assert(stmt->type == AST_ASSIGN_EQ);
 	AstNode *expr = stmt->children[0]->clone();
 	if (undo) {
-		AstNode *minus_one = AstNode::mkconst_int(-1, true, 1);
+		AstNode *one = AstNode::mkconst_int(1, false, 1);
+		AstNode *minus_one = new AstNode(AST_NEG, one);
 		expr = new AstNode(op, expr, minus_one);
 	}
 	SET_AST_NODE_LOC(expr, begin, end);

From 3790be114f770b336b9aa815236504f8173870bd Mon Sep 17 00:00:00 2001
From: George Rennie <georgerennie@gmail.com>
Date: Fri, 30 May 2025 14:36:05 +0100
Subject: [PATCH 2/5] tests: add tests for verilog pre/post increment/decrement
 in expressions

---
 tests/verilog/incdec.ys | 68 +++++++++++++++++++++++++++++++++++++++++
 1 file changed, 68 insertions(+)
 create mode 100644 tests/verilog/incdec.ys

diff --git a/tests/verilog/incdec.ys b/tests/verilog/incdec.ys
new file mode 100644
index 000000000..9133061a5
--- /dev/null
+++ b/tests/verilog/incdec.ys
@@ -0,0 +1,68 @@
+# From https://github.com/YosysHQ/yosys/issues/5151
+read_verilog -sv <<EOT
+module expr_postsub_comb (
+    input logic [7:0] in_val_m2,
+    input logic [7:0] sub_val_m2,
+    output logic [7:0] out_diff_m2,
+    output logic [7:0] var_out_m2
+);
+    logic [7:0] var_m2;
+    always_comb begin
+      var_m2 = in_val_m2;
+      out_diff_m2 = (var_m2--) - sub_val_m2;
+      var_out_m2 = var_m2;
+    end
+
+    always_comb assert(out_diff_m2 == in_val_m2 - sub_val_m2);
+endmodule
+EOT
+
+prep
+chformal -lower
+sat -prove-asserts -verify
+
+design -reset
+
+read_verilog -sv <<EOT
+module top(
+	input logic [7:0] a,
+	output logic [7:0] pre_inc,
+	output logic [7:0] pre_dec,
+	output logic [7:0] post_inc,
+	output logic [7:0] post_dec
+);
+
+logic [7:0] a_pre_inc, a_pre_dec, a_post_inc, a_post_dec;
+always_comb begin
+	a_pre_inc = a;
+	a_pre_dec = a;
+	a_post_inc = a;
+	a_post_dec = a;
+
+	pre_inc = ++a_pre_inc;
+	pre_dec = --a_pre_dec;
+	post_inc = a_post_inc++;
+	post_dec = a_post_dec--;
+end
+
+wire [7:0] a_inc = a + 1;
+wire [7:0] a_dec = a - 1;
+
+always_comb begin
+	assert(a_pre_inc == a_inc);
+	assert(a_pre_dec == a_dec);
+	assert(a_post_inc == a_inc);
+	assert(a_post_dec == a_dec);
+
+	assert(pre_inc == a_inc);
+	assert(pre_dec == a_dec);
+	assert(post_inc == a);
+	assert(post_dec == a);
+end
+
+endmodule
+EOT
+
+prep
+chformal -lower
+sat -prove-asserts -verify

From 45e8ff476edacc4f3a2bd18a90ae0dbf09b9c182 Mon Sep 17 00:00:00 2001
From: George Rennie <georgerennie@gmail.com>
Date: Sat, 31 May 2025 01:08:15 +0100
Subject: [PATCH 3/5] read_verilog: copy inout ports in and out of
 functions/tasks

---
 frontends/ast/simplify.cc | 20 ++++++++++++++------
 1 file changed, 14 insertions(+), 6 deletions(-)

diff --git a/frontends/ast/simplify.cc b/frontends/ast/simplify.cc
index 55087c772..1f9944e2e 100644
--- a/frontends/ast/simplify.cc
+++ b/frontends/ast/simplify.cc
@@ -4099,16 +4099,24 @@ skip_dynamic_range_lvalue_expansion:;
 						delete arg;
 						continue;
 					}
+
 					AstNode *wire_id = new AstNode(AST_IDENTIFIER);
 					wire_id->str = wire->str;
-					AstNode *assign = child->is_input ?
-							new AstNode(AST_ASSIGN_EQ, wire_id, arg) :
-							new AstNode(AST_ASSIGN_EQ, arg, wire_id);
-					assign->children[0]->was_checked = true;
-					if (child->is_input)
+
+					if (child->is_input) {
+						AstNode *assign = new AstNode(AST_ASSIGN_EQ, wire_id->clone(), arg->clone());
+						assign->children[0]->was_checked = true;
 						new_stmts.push_back(assign);
-					else
+					}
+
+					if (child->is_output) {
+						AstNode *assign = new AstNode(AST_ASSIGN_EQ, arg->clone(), wire_id->clone());
+						assign->children[0]->was_checked = true;
 						output_assignments.push_back(assign);
+					}
+
+					delete arg;
+					delete wire_id;
 				}
 			}
 

From 97f51bb4b73ad32036c0d4273487221afabcacb6 Mon Sep 17 00:00:00 2001
From: George Rennie <georgerennie@gmail.com>
Date: Sat, 31 May 2025 01:21:06 +0100
Subject: [PATCH 4/5] tests: add tests for task/function argument input/output
 copying

---
 tests/verilog/func_task_arg_copying.ys | 132 +++++++++++++++++++++++++
 1 file changed, 132 insertions(+)
 create mode 100644 tests/verilog/func_task_arg_copying.ys

diff --git a/tests/verilog/func_task_arg_copying.ys b/tests/verilog/func_task_arg_copying.ys
new file mode 100644
index 000000000..e87c2781b
--- /dev/null
+++ b/tests/verilog/func_task_arg_copying.ys
@@ -0,0 +1,132 @@
+# https://github.com/YosysHQ/yosys/issues/5157
+read_verilog -sv <<EOT
+module stmt_if_task (
+    output logic [7:0] out_val_m6,
+    input logic [7:0] in_val_m6,
+    input bit condition_m6
+);
+    logic [7:0] var_m6;
+    task automatic update_conditional_m6(input bit cond, inout logic [7:0] val);
+        if (cond) begin
+            val++;
+        end else begin
+            --val;
+        end
+    endtask
+    always_comb begin
+        var_m6 = in_val_m6;
+        update_conditional_m6(condition_m6, var_m6);
+        out_val_m6 = var_m6;
+    end
+
+    wire [7:0] m6_inc = in_val_m6 + 1;
+    wire [7:0] m6_dec = in_val_m6 - 1;
+    always_comb assert(out_val_m6 == (condition_m6 ? m6_inc : m6_dec));
+endmodule
+EOT
+
+prep
+chformal -lower
+sat -prove-asserts -verify
+
+design -reset
+
+read_verilog -sv <<EOT
+module top (
+	output logic [7:0] out
+);
+	task automatic set_to_5(inout logic [7:0] val);
+		val = 5;
+	endtask
+
+	always_comb begin
+		out = 0;
+		set_to_5(out);
+	end
+
+	always_comb assert(out == 5);
+endmodule
+EOT
+
+prep
+chformal -lower
+sat -prove-asserts -verify
+
+design -reset
+
+read_verilog -sv <<EOT
+module top (
+	output logic [7:0] a,
+	output logic [7:0] b,
+	output logic [7:0] c
+);
+	task automatic modify(
+		input logic [7:0] t_in,
+		output logic [7:0] t_out,
+		inout logic [7:0] t_inout
+	);
+		assert(t_in == 5);
+		t_in = 6;
+		t_out = 7;
+		assert(t_inout == 8);
+		t_inout = 9;
+	endtask
+
+	always_comb begin
+		a = 5;
+		b = 4;
+		c = 8;
+
+		modify(a, b, c);
+
+		assert(a == 5);
+		assert(b == 7);
+		assert(c == 9);
+	end
+endmodule
+EOT
+
+prep
+chformal -lower
+sat -prove-asserts -verify
+
+design -reset
+
+read_verilog -sv <<EOT
+module top (
+	output logic [7:0] a,
+	output logic [7:0] b,
+	output logic [7:0] c
+);
+	function logic [7:0] modify(
+		input logic [7:0] t_in,
+		output logic [7:0] t_out,
+		inout logic [7:0] t_inout
+	);
+		assert(t_in == 5);
+		t_in = 6;
+		t_out = 7;
+		assert(t_inout == 8);
+		t_inout = 9;
+		modify = 10;
+	endfunction
+
+	logic [7:0] result;
+	always_comb begin
+		a = 5;
+		b = 4;
+		c = 8;
+
+		result = modify(a, b, c);
+
+		assert(a == 5);
+		assert(b == 7);
+		assert(c == 9);
+		assert(result == 10);
+	end
+endmodule
+EOT
+
+prep
+chformal -lower
+sat -prove-asserts -verify

From c37b7b3bf4d347f67636cc8978e38fbc49e09173 Mon Sep 17 00:00:00 2001
From: "Emil J. Tywoniak" <emil@tywoniak.eu>
Date: Wed, 4 Jun 2025 10:32:03 +0200
Subject: [PATCH 5/5] simplify: fix single_bit_vector memory leak

---
 frontends/ast/simplify.cc | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/frontends/ast/simplify.cc b/frontends/ast/simplify.cc
index 749767743..ef5e49519 100644
--- a/frontends/ast/simplify.cc
+++ b/frontends/ast/simplify.cc
@@ -2087,7 +2087,7 @@ bool AstNode::simplify(bool const_fold, int stage, int width_hint, bool sign_hin
 					std::swap(range_left, range_right);
 					range_swapped = force_upto;
 				}
-				if (range_left == range_right)
+				if (range_left == range_right && !attributes.count(ID::single_bit_vector))
 					set_attribute(ID::single_bit_vector, mkconst_int(1, false));
 			}
 		} else {