8 files changed, 94 insertions, 37 deletions
diff --git a/tests/various/const_arg_loop.v b/tests/various/const_arg_loop.sv
index 358fb439a..f28d06e68 100644
--- a/tests/various/const_arg_loop.v
+++ b/tests/various/const_arg_loop.sv
@@ -20,11 +20,11 @@ module top;
 	endfunction
 
 	function automatic [31:0] operation2;
-		input [4:0] var;
+		input [4:0] inp;
 		input integer num;
 		begin
-			var[0] = var[0] ^ 1;
-			operation2 = num * var;
+			inp[0] = inp[0] ^ 1;
+			operation2 = num * inp;
 		end
 	endfunction
 
@@ -79,15 +79,14 @@ module top;
 	wire [31:0] x5;
 	assign x5 = operation5(64);
 
-// `define VERIFY
-`ifdef VERIFY
-    assert property (a == 2);
-    assert property (A == 3);
-    assert property (x1 == 16);
-    assert property (x1b == 16);
-    assert property (x2 == 4);
-    assert property (x3 == 16);
-    assert property (x4 == a << 1);
-    assert property (x5 == 64);
-`endif
+	always_comb begin
+		assert(a == 2);
+		assert(A == 3);
+		assert(x1 == 16);
+		assert(x1b == 16);
+		assert(x2 == 4);
+		assert(x3 == 16);
+		assert(x4 == a << 1);
+		assert(x5 == 64);
+	end
 endmodule
diff --git a/tests/various/const_arg_loop.ys b/tests/various/const_arg_loop.ys
index b039bda10..392532213 100644
--- a/tests/various/const_arg_loop.ys
+++ b/tests/various/const_arg_loop.ys
@@ -1 +1,6 @@
-read_verilog const_arg_loop.v
+read_verilog -sv const_arg_loop.sv
+hierarchy
+proc
+opt -full
+select -module top
+sat -verify -seq 1 -tempinduct -prove-asserts -show-all
diff --git a/tests/various/const_func.v b/tests/various/const_func.sv
index 541e63b19..af65f5c73 100644
--- a/tests/various/const_func.v
+++ b/tests/various/const_func.sv
@@ -62,26 +62,25 @@ module top(out);
     localparam signed Y = $floor(W / X);
     localparam signed Z = negate($floor(W / X));
 
-// `define VERIFY
-`ifdef VERIFY
-    assert property (a1 == 0);
-    assert property (a2 == 0);
-    assert property (a3 == "BAR");
-    assert property (a4 == 0);
-    assert property (b1 == "FOO");
-    assert property (b2 == "FOO");
-    assert property (b3 == 0);
-    assert property (b4 == "HI");
-    assert property (c1 == 1);
-    assert property (c2 == 1);
-    assert property (c3 == 0);
-    assert property (c4 == 0);
-    assert property (d1 == 0);
-    assert property (d2 == 0);
-    assert property (d3 == 1);
-    assert property (d4 == 1);
+    always_comb begin
+        assert(a1 == 0);
+        assert(a2 == 0);
+        assert(a3 == "BAR");
+        assert(a4 == 0);
+        assert(b1 == "FOO");
+        assert(b2 == "FOO");
+        assert(b3 == 0);
+        assert(b4 == "HI");
+        assert(c1 == 1);
+        assert(c2 == 1);
+        assert(c3 == 0);
+        assert(c4 == 0);
+        assert(d1 == 0);
+        assert(d2 == 0);
+        assert(d3 == 1);
+        assert(d4 == 1);
 
-    assert property (Y == 3);
-    assert property (Z == ~3);
-`endif
+        assert(Y == 3);
+        assert(Z == ~3);
+    end
 endmodule
diff --git a/tests/various/const_func.ys b/tests/various/const_func.ys
index 5e3c04105..2f60acfe6 100644
--- a/tests/various/const_func.ys
+++ b/tests/various/const_func.ys
@@ -1 +1,7 @@
-read_verilog const_func.v
+read_verilog -sv const_func.sv
+hierarchy
+proc
+flatten
+opt -full
+select -module top
+sat -verify -seq 1 -tempinduct -prove-asserts -show-all
diff --git a/tests/verilog/func_arg_mismatch_1.ys b/tests/verilog/func_arg_mismatch_1.ys
new file mode 100644
index 000000000..a0e82db0c
--- /dev/null
+++ b/tests/verilog/func_arg_mismatch_1.ys
@@ -0,0 +1,12 @@
+logger -expect error "Incompatible re-declaration of wire" 1
+read_verilog -sv <<EOT
+module top;
+    function automatic integer f;
+        input [0:0] inp;
+        integer inp;
+        f = inp;
+    endfunction
+    integer x, y;
+    initial x = f(y);
+endmodule
+EOT
diff --git a/tests/verilog/func_arg_mismatch_2.ys b/tests/verilog/func_arg_mismatch_2.ys
new file mode 100644
index 000000000..c2c29c1fb
--- /dev/null
+++ b/tests/verilog/func_arg_mismatch_2.ys
@@ -0,0 +1,12 @@
+logger -expect error "Incompatible re-declaration of constant function wire" 1
+read_verilog -sv <<EOT
+module top;
+    function automatic integer f;
+        input [0:0] inp;
+        integer inp;
+        f = inp;
+    endfunction
+    integer x;
+    initial x = f(0);
+endmodule
+EOT
diff --git a/tests/verilog/func_arg_mismatch_3.ys b/tests/verilog/func_arg_mismatch_3.ys
new file mode 100644
index 000000000..892824c09
--- /dev/null
+++ b/tests/verilog/func_arg_mismatch_3.ys
@@ -0,0 +1,12 @@
+logger -expect error "Incompatible re-declaration of wire" 1
+read_verilog -sv <<EOT
+module top;
+    function automatic integer f;
+        input [1:0] inp;
+        integer inp;
+        f = inp;
+    endfunction
+    integer x, y;
+    initial x = f(y);
+endmodule
+EOT
diff --git a/tests/verilog/func_arg_mismatch_4.ys b/tests/verilog/func_arg_mismatch_4.ys
new file mode 100644
index 000000000..87ec1c299
--- /dev/null
+++ b/tests/verilog/func_arg_mismatch_4.ys
@@ -0,0 +1,12 @@
+logger -expect error "Incompatible re-declaration of constant function wire" 1
+read_verilog -sv <<EOT
+module top;
+    function automatic integer f;
+        input [1:0] inp;
+        integer inp;
+        f = inp;
+    endfunction
+    integer x;
+    initial x = f(0);
+endmodule
+EOT