4 files changed, 36 insertions, 143 deletions
diff --git a/tests/various/const_func.v b/tests/various/const_func.v
index 76cdc385d..541e63b19 100644
--- a/tests/various/const_func.v
+++ b/tests/various/const_func.v
@@ -53,6 +53,15 @@ module top(out);
         c1, c2, c3, c4,
         d1, d2, d3, d4};
 
+    function signed [31:0] negate;
+        input integer inp;
+        negate = ~inp;
+    endfunction
+    parameter W = 10;
+    parameter X = 3;
+    localparam signed Y = $floor(W / X);
+    localparam signed Z = negate($floor(W / X));
+
 // `define VERIFY
 `ifdef VERIFY
     assert property (a1 == 0);
@@ -71,5 +80,8 @@ module top(out);
     assert property (d2 == 0);
     assert property (d3 == 1);
     assert property (d4 == 1);
+
+    assert property (Y == 3);
+    assert property (Z == ~3);
 `endif
 endmodule
diff --git a/tests/various/const_func_block_var.v b/tests/various/const_func_block_var.v
new file mode 100644
index 000000000..98e83aa5b
--- /dev/null
+++ b/tests/various/const_func_block_var.v
@@ -0,0 +1,23 @@
+module top(out);
+	function integer operation;
+		input integer num;
+		begin
+			operation = 0;
+			begin : op_i
+				integer i;
+				for (i = 0; i < 2; i = i + 1)
+				begin : op_j
+					integer j;
+					for (j = i; j < i * 2; j = j + 1)
+						num = num + 1;
+				end
+				num = num * 2;
+			end
+			operation = num;
+		end
+	endfunction
+
+	localparam res = operation(4);
+	output wire [31:0] out;
+	assign out = res;
+endmodule
diff --git a/tests/various/const_func_block_var.ys b/tests/various/const_func_block_var.ys
new file mode 100644
index 000000000..7c2e85c64
--- /dev/null
+++ b/tests/various/const_func_block_var.ys
@@ -0,0 +1 @@
+read_verilog const_func_block_var.v
diff --git a/tests/various/peepopt.ys b/tests/various/peepopt.ys
index ee5ad8a1a..45e936a21 100644
--- a/tests/various/peepopt.ys
+++ b/tests/various/peepopt.ys
@@ -68,146 +68,3 @@ equiv_opt -assert peepopt
 design -load postopt
 clean
 select -assert-count 0 t:*
-
-####################
-
-design -reset
-read_verilog <<EOT
-module peepopt_dffmuxext_unsigned(input clk, ce, input [1:0] i, output reg [3:0] o);
-    always @(posedge clk) if (ce) o <= i;
-endmodule
-EOT
-
-proc
-equiv_opt -assert peepopt
-design -load postopt
-clean
-select -assert-count 1 t:$dff r:WIDTH=2 %i
-select -assert-count 1 t:$mux r:WIDTH=2 %i
-select -assert-count 0 t:$dff t:$mux %% t:* %D
-
-####################
-
-design -reset
-read_verilog <<EOT
-module peepopt_dffmuxext_signed(input clk, ce, input signed [1:0] i, output reg signed [3:0] o);
-    always @(posedge clk) if (ce) o <= i;
-endmodule
-EOT
-
-proc
-equiv_opt -assert peepopt
-design -load postopt
-clean
-select -assert-count 1 t:$dff r:WIDTH=2 %i
-select -assert-count 1 t:$mux r:WIDTH=2 %i
-select -assert-count 0 t:$dff t:$mux %% t:* %D
-
-###################
-
-design -reset
-read_verilog <<EOT
-module peepopt_dffmuxext_const(input clk, ce, input [1:0] i, output reg [5:0] o);
-    always @(posedge clk) if (ce) o <= {1'b0, i[1], 2'b1x, i[0], 1'bz};
-endmodule
-EOT
-
-proc
-equiv_opt -assert peepopt
-design -load postopt
-select -assert-count 1 t:$dff r:WIDTH=2 %i
-select -assert-count 1 t:$mux r:WIDTH=2 %i
-select -assert-count 0 t:$dff t:$mux %% t:* %D
-
-###################
-
-design -reset
-read_verilog <<EOT
-module peepopt_dffmuxext_const_init(input clk, ce, input [1:0] i, (* init=6'b0x00x1 *) output reg [5:0] o);
-    always @(posedge clk) if (ce) o <= {1'b0, i[1], 2'b1x, i[0], 1'bz};
-endmodule
-EOT
-
-proc
-equiv_opt -assert peepopt
-design -load postopt
-select -assert-count 1 t:$dff r:WIDTH=4 %i
-select -assert-count 1 t:$mux r:WIDTH=4 %i
-select -assert-count 0 t:$dff t:$mux %% t:* %D
-
-####################
-
-design -reset
-read_verilog <<EOT
-module peepopt_dffmuxext_unsigned_rst(input clk, ce, rst, input [1:0] i, output reg [3:0] o);
-    always @(posedge clk) if (rst) o <= 0; else if (ce) o <= i;
-endmodule
-EOT
-
-proc
-equiv_opt -assert peepopt
-design -load postopt
-wreduce
-select -assert-count 1 t:$dff r:WIDTH=2 %i
-select -assert-count 2 t:$mux
-select -assert-count 2 t:$mux r:WIDTH=2 %i
-select -assert-count 0 t:$dff t:$mux %% t:* %D
-
-####################
-
-design -reset
-read_verilog <<EOT
-module peepopt_dffmuxext_signed_rst(input clk, ce, rstn, input signed [1:0] i, output reg signed [3:0] o);
-    always @(posedge clk) begin
-        if (ce) o <= i;
-        if (!rstn) o <= 4'b1111;
-    end
-endmodule
-EOT
-
-proc
-equiv_opt -assert peepopt
-design -load postopt
-wreduce
-select -assert-count 1 t:$dff r:WIDTH=2 %i
-select -assert-count 2 t:$mux
-select -assert-count 2 t:$mux r:WIDTH=2 %i
-select -assert-count 0 t:$logic_not t:$dff t:$mux %% t:* %D
-
-####################
-
-design -reset
-read_verilog <<EOT
-module peepopt_dffmuxext_signed_rst_init(input clk, ce, rstn, input signed [1:0] i, output reg signed [3:0] o);
-    initial o <= 4'b0010;
-    always @(posedge clk) begin
-        if (ce) o <= i;
-        if (!rstn) o <= 4'b1111;
-    end
-endmodule
-EOT
-
-proc
-# NB: equiv_opt uses equiv_induct which covers
-#     only the induction half of temporal induction
-#     --- missing the base-case half
-#     This makes it akin to `sat -tempinduct-inductonly`
-#     instead of `sat -tempinduct-baseonly` or
-#     `sat -tempinduct` which is necessary for this
-#     testcase
-#equiv_opt -assert peepopt
-
-design -save gold
-peepopt
-wreduce
-design -stash gate
-design -import gold -as gold
-design -import gate -as gate
-miter -equiv -flatten -make_assert -make_outputs gold gate miter
-sat -tempinduct -verify -prove-asserts -show-ports miter
-
-design -load gate
-select -assert-count 1 t:$dff r:WIDTH=4 %i
-select -assert-count 2 t:$mux
-select -assert-count 2 t:$mux r:WIDTH=4 %i
-select -assert-count 0 t:$logic_not t:$dff t:$mux %% t:* %D