8 files changed, 147 insertions, 0 deletions
diff --git a/tests/various/aiger_dff.ys b/tests/various/aiger_dff.ys
new file mode 100644
index 000000000..057f3d774
--- /dev/null
+++ b/tests/various/aiger_dff.ys
@@ -0,0 +1,7 @@
+read_verilog -icells <<EOT
+module top(input clk, d, output q);
+\$_DFF_N_ dffn(.C(clk), .D(d), .Q(q));
+endmodule
+EOT
+write_aiger -zinit -ywmap aiger_dff.out /dev/null
+!grep -qF negedge aiger_dff.out
diff --git a/tests/various/bug3462.ys b/tests/various/bug3462.ys
new file mode 100644
index 000000000..c85dc9470
--- /dev/null
+++ b/tests/various/bug3462.ys
@@ -0,0 +1,12 @@
+read_verilog <<EOT
+module top();
+    wire array[0:0];
+    wire out;
+    sub #(.d(1)) inst(
+        .in(array[0]),
+        .out(out)
+    );
+endmodule
+EOT
+
+hierarchy -top top -libdir .
diff --git a/tests/various/cellarray_array_connections.ys b/tests/various/cellarray_array_connections.ys
new file mode 100644
index 000000000..ef36a9a45
--- /dev/null
+++ b/tests/various/cellarray_array_connections.ys
@@ -0,0 +1,45 @@
+# Regression test for #3467
+read_verilog <<EOT
+
+module bit_buf (
+    input wire bit_in,
+    output wire bit_out
+);
+    assign bit_out = bit_in;
+endmodule
+
+module top (
+	input wire [3:0] data_in,
+	output wire [3:0] data_out
+);
+
+    wire [3:0] data [0:4];
+
+    assign data[0] = data_in;
+    assign data_out = data[4];
+
+	genvar i;
+	generate
+		for (i=0; i<=3; i=i+1) begin
+			bit_buf bit_buf_instance[3:0] (
+				.bit_in(data[i]),
+				.bit_out(data[i + 1])
+			);
+		end
+	endgenerate
+endmodule
+
+module top2 (
+	input wire [3:0] data_in,
+	output wire [3:0] data_out
+);
+    assign data_out = data_in;
+endmodule
+
+EOT
+
+hierarchy
+proc
+
+miter -equiv -make_assert -flatten top top2 miter
+sat -prove-asserts -verify miter
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/rename_scramble_name.ys b/tests/various/rename_scramble_name.ys
new file mode 100644
index 000000000..9a36d0922
--- /dev/null
+++ b/tests/various/rename_scramble_name.ys
@@ -0,0 +1,31 @@
+read_verilog <<EOF
+module top();
+    wire a, b, c;
+endmodule
+EOF
+
+proc
+hierarchy -top top
+rename -seed 2 -scramble-name w:*
+select -assert-none w:a w:b w:c
+select -assert-count 3 w:$_*_
+select -assert-none w:$_*_ %% %n
+design -reset
+
+read_verilog <<EOF
+module foo(input a, b, output c);
+    assign c = a + b;
+endmodule
+
+module top();
+    wire a, b, c;
+    foo bar(.a(a), .b(b), .c(c));
+endmodule
+EOF
+
+proc
+hierarchy -top top
+rename -seed 2 -scramble-name c:bar
+select -assert-none c:bar
+select -assert-count 1 c:$_*_
+select -assert-none c:$_*_ w:* foo/c:$add$<<EOF:2$1 %% %n
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
diff --git a/tests/various/smtlib2_module-expected.smt2 b/tests/various/smtlib2_module-expected.smt2
index ace858ca8..494e7cda0 100644
--- a/tests/various/smtlib2_module-expected.smt2
+++ b/tests/various/smtlib2_module-expected.smt2
@@ -4,11 +4,14 @@
 (declare-fun |smtlib2_is| (|smtlib2_s|) Bool)
 (declare-fun |smtlib2#0| (|smtlib2_s|) (_ BitVec 8)) ; \a
 ; yosys-smt2-input a 8
+; yosys-smt2-witness {"offset": 0, "path": ["\\a"], "smtname": "a", "smtoffset": 0, "type": "input", "width": 8}
 (define-fun |smtlib2_n a| ((state |smtlib2_s|)) (_ BitVec 8) (|smtlib2#0| state))
 (declare-fun |smtlib2#1| (|smtlib2_s|) (_ BitVec 8)) ; \b
 ; yosys-smt2-input b 8
+; yosys-smt2-witness {"offset": 0, "path": ["\\b"], "smtname": "b", "smtoffset": 0, "type": "input", "width": 8}
 (define-fun |smtlib2_n b| ((state |smtlib2_s|)) (_ BitVec 8) (|smtlib2#1| state))
 ; yosys-smt2-output add 8
+; yosys-smt2-witness {"offset": 0, "path": ["\\add"], "smtname": "add", "smtoffset": 0, "type": "blackbox", "width": 8}
 (define-fun |smtlib2_n add| ((state |smtlib2_s|)) (_ BitVec 8) (let (
 (|a| (|smtlib2_n a| state))
 (|b| (|smtlib2_n b| state))
@@ -16,6 +19,7 @@
 (bvadd a b)
 ))
 ; yosys-smt2-output eq 1
+; yosys-smt2-witness {"offset": 0, "path": ["\\eq"], "smtname": "eq", "smtoffset": 0, "type": "blackbox", "width": 1}
 (define-fun |smtlib2_n eq| ((state |smtlib2_s|)) Bool (let (
 (|a| (|smtlib2_n a| state))
 (|b| (|smtlib2_n b| state))
@@ -23,6 +27,7 @@
 (= a b)
 ))
 ; yosys-smt2-output sub 8
+; yosys-smt2-witness {"offset": 0, "path": ["\\sub"], "smtname": "sub", "smtoffset": 0, "type": "blackbox", "width": 8}
 (define-fun |smtlib2_n sub| ((state |smtlib2_s|)) (_ BitVec 8) (let (
 (|a| (|smtlib2_n a| state))
 (|b| (|smtlib2_n b| state))
@@ -38,13 +43,16 @@
 (declare-sort |uut_s| 0)
 (declare-fun |uut_is| (|uut_s|) Bool)
 ; yosys-smt2-cell smtlib2 s
+; yosys-smt2-witness {"path": ["\\s"], "smtname": "s", "type": "cell"}
 (declare-fun |uut#0| (|uut_s|) (_ BitVec 8)) ; \add
 (declare-fun |uut#1| (|uut_s|) Bool) ; \eq
 (declare-fun |uut#2| (|uut_s|) (_ BitVec 8)) ; \sub
 (declare-fun |uut_h s| (|uut_s|) |smtlib2_s|)
 ; yosys-smt2-anyconst uut#3 8 smtlib2_module.v:14.17-14.26
+; yosys-smt2-witness {"offset": 0, "path": ["\\a"], "smtname": 3, "smtoffset": 0, "type": "init", "width": 8}
 (declare-fun |uut#3| (|uut_s|) (_ BitVec 8)) ; \a
 ; yosys-smt2-anyconst uut#4 8 smtlib2_module.v:14.32-14.41
+; yosys-smt2-witness {"offset": 0, "path": ["\\b"], "smtname": 4, "smtoffset": 0, "type": "init", "width": 8}
 (declare-fun |uut#4| (|uut_s|) (_ BitVec 8)) ; \b
 (define-fun |uut#5| ((state |uut_s|)) (_ BitVec 8) (bvadd (|uut#3| state) (|uut#4| state))) ; \add2
 (define-fun |uut#6| ((state |uut_s|)) Bool (= (|uut#0| state) (|uut#5| state))) ; $0$formal$smtlib2_module.v:28$1_CHECK[0:0]$9
diff --git a/tests/various/sub.v b/tests/various/sub.v
new file mode 100644
index 000000000..63422ca5c
--- /dev/null
+++ b/tests/various/sub.v
@@ -0,0 +1,3 @@
+module sub #(parameter d=1) (input in, output out);
+    assign out = in;
+endmodule