4 files changed, 106 insertions, 0 deletions
diff --git a/tests/various/chformal_coverenable.ys b/tests/various/chformal_coverenable.ys
new file mode 100644
index 000000000..52b3ee6bf
--- /dev/null
+++ b/tests/various/chformal_coverenable.ys
@@ -0,0 +1,25 @@
+read_verilog -formal <<EOT
+module top(input a, b, c, d);
+
+    always @* begin
+        if (a) assert (b == c);
+        if (!a) assert (b != c);
+        if (b) assume (c);
+        if (c) cover (d);
+    end
+
+endmodule
+EOT
+
+prep -top top
+
+select -assert-count 1 t:$cover
+
+chformal -cover -coverenable
+select -assert-count 2 t:$cover
+
+chformal -assert -coverenable
+select -assert-count 4 t:$cover
+
+chformal -assume -coverenable
+select -assert-count 5 t:$cover
diff --git a/tests/various/equiv_make_make_assert.ys b/tests/various/equiv_make_make_assert.ys
new file mode 100644
index 000000000..1c2efa723
--- /dev/null
+++ b/tests/various/equiv_make_make_assert.ys
@@ -0,0 +1,32 @@
+read_verilog <<EOT
+module gold(
+	input wire [7:0] a,
+	input wire [7:0] b,
+	output wire [7:0] c
+);
+
+wire [7:0] b_neg;
+assign b_neg = -b;
+assign c = a + b_neg;
+endmodule
+
+module gate(
+	input wire [7:0] a,
+	input wire [7:0] b,
+	output wire [7:0] c
+);
+
+wire [7:0] b_neg;
+assign b_neg = ~b + 1;
+assign c = a + b_neg;
+endmodule
+
+EOT
+
+equiv_make -make_assert gold gate miter
+
+select -assert-count 0 t:$equiv
+select -assert-count 2 t:$assert
+
+prep -top miter
+sat -prove-asserts -verify
diff --git a/tests/various/muxcover.ys b/tests/various/muxcover.ys
index 67e9625e6..37a90dcb0 100644
--- a/tests/various/muxcover.ys
+++ b/tests/various/muxcover.ys
@@ -508,3 +508,43 @@ design -import gate -as gate
 
 miter -equiv -flatten -make_assert -make_outputs -ignore_gold_x gold gate miter
 sat -verify -prove-asserts -show-ports miter
+
+## implement a mux6 as a mux8 :: https://github.com/YosysHQ/yosys/issues/3591
+
+design -reset
+read_verilog << EOF
+module test (A, S, Y);
+        parameter INPUTS = 6;
+
+        input [INPUTS-1:0] A;
+        input [$clog2(INPUTS)-1:0] S;
+
+        wire [15:0] AA = {{(16-INPUTS){1'b0}}, A};
+        wire [3:0] SS = {{(4-$clog2(INPUTS)){1'b0}}, S};
+
+        output Y = SS[3] ? (SS[2] ? SS[1] ? (SS[0] ? AA[15] : AA[14])
+                                          : (SS[0] ? AA[13] : AA[12])
+                                  : SS[1] ? (SS[0] ? AA[11] : AA[10])
+                                          : (SS[0] ? AA[9] : AA[8]))
+                         : (SS[2] ? SS[1] ? (SS[0] ? AA[7] : AA[6])
+                                          : (SS[0] ? AA[5] : AA[4])
+                                  : SS[1] ? (SS[0] ? AA[3] : AA[2])
+                                          : (SS[0] ? AA[1] : AA[0]));
+endmodule
+EOF
+
+prep
+design -save gold
+simplemap t:\$mux
+muxcover
+opt_clean -purge
+select -assert-count 1 t:$_MUX8_
+select -assert-none t:$_MUX8_ %% t:* %D
+techmap -map +/simcells.v t:$_MUX8_
+design -stash gate
+
+design -import gold -as gold
+design -import gate -as gate
+
+miter -equiv -flatten -make_assert -make_outputs -ignore_gold_x gold gate miter
+sat -verify -prove-asserts -show-ports miter
diff --git a/tests/various/rtlil_z_bits.ys b/tests/various/rtlil_z_bits.ys
new file mode 100644
index 000000000..c38669159
--- /dev/null
+++ b/tests/various/rtlil_z_bits.ys
@@ -0,0 +1,9 @@
+! mkdir -p temp
+read_rtlil <<EOT
+module \test
+  wire output 1 \a
+  connect \a 1'z
+end
+EOT
+write_rtlil temp/rtlil_z_bits.il
+! grep -F -q "connect \\a 1'z" temp/rtlil_z_bits.il