17 files changed, 586 insertions, 12 deletions
diff --git a/tests/arch/ecp5/mux.ys b/tests/arch/ecp5/mux.ys
index 22866832d..92463aa32 100644
--- a/tests/arch/ecp5/mux.ys
+++ b/tests/arch/ecp5/mux.ys
@@ -39,8 +39,8 @@ proc
 equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 # equivalency check
 design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
 cd mux16 # Constrain all select calls below inside the top module
-select -assert-count 12 t:L6MUX21
-select -assert-count 34 t:LUT4
-select -assert-count 17 t:PFUMX
+select -assert-count 8 t:L6MUX21
+select -assert-count 26 t:LUT4
+select -assert-count 12 t:PFUMX
 
 select -assert-none t:LUT4 t:L6MUX21 t:PFUMX %% t:* %D
diff --git a/tests/arch/ecp5/opt_lut_ins.ys b/tests/arch/ecp5/opt_lut_ins.ys
new file mode 100644
index 000000000..2bc546912
--- /dev/null
+++ b/tests/arch/ecp5/opt_lut_ins.ys
@@ -0,0 +1,32 @@
+read_ilang << EOF
+
+module \top
+
+  wire input 1 \A
+  wire input 2 \B
+  wire input 3 \C
+  wire input 4 \D
+
+  wire output 5 \Z
+
+  cell \LUT4 $0
+    parameter \INIT 16'1111110011000000
+    connect \A \A
+    connect \B \B
+    connect \C \C
+    connect \D \D
+    connect \Z \Z
+  end
+end
+
+EOF
+
+read_verilog -lib +/ecp5/cells_sim.v
+
+equiv_opt -assert -map +/ecp5/cells_sim.v opt_lut_ins -tech ecp5
+
+design -load postopt
+
+select -assert-count 1 top/t:LUT4
+select -assert-count 0 top/w:A %co top/t:LUT4 %i
+select -assert-count 1 top/w:B %co top/t:LUT4 %i
diff --git a/tests/arch/efinix/mux.ys b/tests/arch/efinix/mux.ys
index a5ab80d8b..67006b6f2 100644
--- a/tests/arch/efinix/mux.ys
+++ b/tests/arch/efinix/mux.ys
@@ -16,7 +16,7 @@ proc
 equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix # equivalency check
 design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
 cd mux4 # Constrain all select calls below inside the top module
-select -assert-count 2 t:EFX_LUT4
+#select -assert-count 2 t:EFX_LUT4
 
 select -assert-none t:EFX_LUT4 %% t:* %D
 
@@ -26,7 +26,7 @@ proc
 equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix # equivalency check
 design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
 cd mux8 # Constrain all select calls below inside the top module
-select -assert-count 5 t:EFX_LUT4
+#select -assert-count 5 t:EFX_LUT4
 
 select -assert-none t:EFX_LUT4 %% t:* %D
 
diff --git a/tests/arch/gowin/mux.ys b/tests/arch/gowin/mux.ys
index afad29a89..33b092284 100644
--- a/tests/arch/gowin/mux.ys
+++ b/tests/arch/gowin/mux.ys
@@ -18,13 +18,13 @@ proc
 equiv_opt -assert -map +/gowin/cells_sim.v synth_gowin # equivalency check
 design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
 cd mux4 # Constrain all select calls below inside the top module
-select -assert-count 4 t:LUT4
+select -assert-count 4 t:LUT*
 select -assert-count 2 t:MUX2_LUT5
 select -assert-count 1 t:MUX2_LUT6
 select -assert-count 6 t:IBUF
 select -assert-count 1 t:OBUF
 
-select -assert-none t:LUT4 t:MUX2_LUT6 t:MUX2_LUT5 t:IBUF t:OBUF %% t:* %D
+select -assert-none t:LUT* t:MUX2_LUT6 t:MUX2_LUT5 t:IBUF t:OBUF %% t:* %D
 
 design -load read
 hierarchy -top mux8
@@ -35,7 +35,7 @@ cd mux8 # Constrain all select calls below inside the top module
 select -assert-count 11 t:IBUF
 select -assert-count 1 t:OBUF
 
-select -assert-none t:LUT4 t:MUX2_LUT6 t:MUX2_LUT5 t:IBUF t:OBUF %% t:* %D
+select -assert-none t:LUT* t:MUX2_LUT6 t:MUX2_LUT5 t:IBUF t:OBUF %% t:* %D
 
 design -load read
 hierarchy -top mux16
@@ -46,4 +46,4 @@ cd mux16 # Constrain all select calls below inside the top module
 select -assert-count 20 t:IBUF
 select -assert-count 1 t:OBUF
 
-select -assert-none t:LUT4 t:MUX2_LUT6 t:MUX2_LUT5 t:MUX2_LUT6 t:MUX2_LUT7 t:MUX2_LUT8 t:IBUF t:OBUF %% t:* %D
+select -assert-none t:GND t:VCC t:LUT* t:MUX2_LUT6 t:MUX2_LUT5 t:MUX2_LUT6 t:MUX2_LUT7 t:MUX2_LUT8 t:IBUF t:OBUF %% t:* %D
diff --git a/tests/arch/xilinx/add_sub.ys b/tests/arch/xilinx/add_sub.ys
index 70cfe81a3..6be9a73a3 100644
--- a/tests/arch/xilinx/add_sub.ys
+++ b/tests/arch/xilinx/add_sub.ys
@@ -1,11 +1,23 @@
 read_verilog ../common/add_sub.v
 hierarchy -top top
 proc
+design -save orig
+
 equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check
 design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
 cd top # Constrain all select calls below inside the top module
 stat
-select -assert-count 16 t:LUT2
+select -assert-count 8 t:LUT2
 select -assert-count 2 t:CARRY4
 select -assert-none t:LUT2 t:CARRY4 %% t:* %D
 
+design -load orig
+
+equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -family xc3s -noiopad # equivalency check
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd top # Constrain all select calls below inside the top module
+stat
+select -assert-count 8 t:LUT2
+select -assert-count 6 t:MUXCY
+select -assert-count 8 t:XORCY
+select -assert-none t:LUT2 t:MUXCY t:XORCY %% t:* %D
diff --git a/tests/arch/xilinx/dffs.ys b/tests/arch/xilinx/dffs.ys
index dc764b033..deaf16bd6 100644
--- a/tests/arch/xilinx/dffs.ys
+++ b/tests/arch/xilinx/dffs.ys
@@ -8,7 +8,6 @@ design -load postopt # load the post-opt design (otherwise equiv_opt loads the p
 cd dff # Constrain all select calls below inside the top module
 select -assert-count 1 t:BUFG
 select -assert-count 1 t:FDRE
-
 select -assert-none t:BUFG t:FDRE %% t:* %D
 
 
@@ -20,6 +19,27 @@ design -load postopt # load the post-opt design (otherwise equiv_opt loads the p
 cd dffe # Constrain all select calls below inside the top module
 select -assert-count 1 t:BUFG
 select -assert-count 1 t:FDRE
+select -assert-none t:BUFG t:FDRE %% t:* %D
+
+
+design -load read
+hierarchy -top dff
+proc
+equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -abc9 -dff -noiopad # equivalency check
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd dff # Constrain all select calls below inside the top module
+select -assert-count 1 t:BUFG
+select -assert-count 1 t:FDRE
+select -assert-none t:BUFG t:FDRE %% t:* %D
+
 
+design -load read
+hierarchy -top dffe
+proc
+equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -abc9 -dff -noiopad # equivalency check
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd dffe # Constrain all select calls below inside the top module
+select -assert-count 1 t:BUFG
+select -assert-count 1 t:FDRE
 select -assert-none t:BUFG t:FDRE %% t:* %D
 
diff --git a/tests/arch/xilinx/fsm.ys b/tests/arch/xilinx/fsm.ys
index a464fcfdb..fec4c6082 100644
--- a/tests/arch/xilinx/fsm.ys
+++ b/tests/arch/xilinx/fsm.ys
@@ -3,6 +3,8 @@ hierarchy -top fsm
 proc
 flatten
 
+design -save orig
+
 equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad
 miter -equiv -make_assert -flatten gold gate miter
 sat -verify -prove-asserts -show-public -set-at 1 in_reset 1 -seq 20 -prove-skip 1 miter
@@ -17,3 +19,20 @@ select -assert-count 1 t:LUT2
 select -assert-count 3 t:LUT5
 select -assert-count 1 t:LUT6
 select -assert-none t:BUFG t:FDRE t:FDSE t:LUT2 t:LUT5 t:LUT6 %% t:* %D
+
+design -load orig
+
+equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -family xc3se -noiopad
+miter -equiv -make_assert -flatten gold gate miter
+sat -verify -prove-asserts -show-public -set-at 1 in_reset 1 -seq 20 -prove-skip 1 miter
+
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd fsm # Constrain all select calls below inside the top module
+stat
+select -assert-count 1 t:BUFG
+select -assert-count 6 t:FDRE
+select -assert-count 1 t:LUT1
+select -assert-count 3 t:LUT3
+select -assert-count 6 t:LUT4
+select -assert-count 6 t:MUXF5
+select -assert-none t:BUFG t:FDRE t:LUT1 t:LUT3 t:LUT4 t:MUXF5 %% t:* %D
diff --git a/tests/arch/xilinx/lutram.ys b/tests/arch/xilinx/lutram.ys
index 3f127a77e..cc7354501 100644
--- a/tests/arch/xilinx/lutram.ys
+++ b/tests/arch/xilinx/lutram.ys
@@ -135,3 +135,23 @@ select -assert-count 1 t:BUFG
 select -assert-count 6 t:FDRE
 select -assert-count 2 t:RAM64M
 select -assert-none t:BUFG t:FDRE t:RAM64M %% t:* %D
+
+
+design -reset
+read_verilog ../common/lutram.v
+hierarchy -top lutram_1w1r -chparam A_WIDTH 4
+proc
+memory -nomap
+equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -family xc3s -noiopad
+memory
+opt -full
+
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -verify -prove-asserts -seq 3 -set-init-zero -show-inputs -show-outputs miter
+
+design -load postopt
+cd lutram_1w1r
+select -assert-count 1 t:BUFG
+select -assert-count 8 t:FDRE
+select -assert-count 8 t:RAM16X1D
+select -assert-none t:BUFG t:FDRE t:RAM16X1D %% t:* %D
diff --git a/tests/arch/xilinx/mux_lut4.ys b/tests/arch/xilinx/mux_lut4.ys
new file mode 100644
index 000000000..3e3256993
--- /dev/null
+++ b/tests/arch/xilinx/mux_lut4.ys
@@ -0,0 +1,51 @@
+read_verilog ../common/mux.v
+design -save read
+
+hierarchy -top mux2
+proc
+equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -family xc3se -noiopad # equivalency check
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd mux2 # Constrain all select calls below inside the top module
+select -assert-count 1 t:LUT3
+
+select -assert-none t:LUT3 %% t:* %D
+
+
+design -load read
+hierarchy -top mux4
+proc
+equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -family xc3se -noiopad # equivalency check
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd mux4 # Constrain all select calls below inside the top module
+select -assert-count 4 t:LUT1
+select -assert-count 2 t:MUXF5
+select -assert-count 1 t:MUXF6
+
+select -assert-none t:LUT1 t:MUXF5 t:MUXF6 %% t:* %D
+
+
+design -load read
+hierarchy -top mux8
+proc
+equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -family xc3se -noiopad # equivalency check
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd mux8 # Constrain all select calls below inside the top module
+select -assert-count 4 t:LUT1
+select -assert-count 3 t:LUT4
+select -assert-count 2 t:MUXF5
+select -assert-count 1 t:MUXF6
+
+select -assert-none t:LUT1 t:LUT4 t:MUXF5 t:MUXF6 %% t:* %D
+
+
+design -load read
+hierarchy -top mux16
+proc
+equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -family xc3se -noiopad # equivalency check
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd mux16 # Constrain all select calls below inside the top module
+select -assert-max 32 t:LUT*
+select -assert-max 8 t:MUXF6
+select -assert-max 4 t:MUXF7
+
+select -assert-none t:LUT* t:MUXF5 t:MUXF6 t:MUXF7 %% t:* %D
diff --git a/tests/arch/xilinx/opt_lut_ins.ys b/tests/arch/xilinx/opt_lut_ins.ys
new file mode 100644
index 000000000..a01d02179
--- /dev/null
+++ b/tests/arch/xilinx/opt_lut_ins.ys
@@ -0,0 +1,25 @@
+read_ilang << EOF
+
+module \top
+
+  wire width 4 input 1 \A
+
+  wire output 2 \O
+
+  cell \LUT4 $0
+    parameter \INIT 16'1111110011000000
+    connect \I0 \A [0]
+    connect \I1 \A [1]
+    connect \I2 \A [2]
+    connect \I3 \A [3]
+    connect \O \O
+  end
+end
+
+EOF
+
+equiv_opt -assert -map +/xilinx/cells_sim.v opt_lut_ins -tech xilinx
+
+design -load postopt
+
+select -assert-count 1 t:LUT3
diff --git a/tests/opt/opt_lut_ins.ys b/tests/opt/opt_lut_ins.ys
new file mode 100644
index 000000000..82460b164
--- /dev/null
+++ b/tests/opt/opt_lut_ins.ys
@@ -0,0 +1,23 @@
+read_ilang << EOF
+
+module \top
+
+  wire width 4 input 1 \A
+
+  wire output 2 \Y
+
+  cell $lut \lut
+    parameter \LUT 16'1111110011000000
+    parameter \WIDTH 4
+    connect \A \A
+    connect \Y \Y
+  end
+end
+
+EOF
+
+equiv_opt -assert opt_lut_ins
+
+design -load postopt
+
+select -assert-count 1 t:$lut r:WIDTH=3 %i
diff --git a/tests/opt/opt_merge_init.ys b/tests/opt/opt_merge_init.ys
new file mode 100644
index 000000000..a29c29df6
--- /dev/null
+++ b/tests/opt/opt_merge_init.ys
@@ -0,0 +1,49 @@
+read_verilog -icells <<EOT
+module top(input clk, i, (* init = 1'b0 *) output o, p);
+  \$dff  #(
+    .CLK_POLARITY(1'h1),
+    .WIDTH(32'd1)
+  ) ffo  (
+    .CLK(clk),
+    .D(i),
+    .Q(o)
+  );
+  \$dff  #(
+    .CLK_POLARITY(1'h1),
+    .WIDTH(32'd1)
+  ) ffp  (
+    .CLK(clk),
+    .D(i),
+    .Q(p)
+  );
+endmodule
+EOT
+
+opt_merge
+select -assert-count 1 a:init=1'0
+
+
+design -reset
+read_verilog -icells <<EOT
+module top(input clk, i, (* init = 2'b11 *) output [1:0] o);
+  \$dff  #(
+    .CLK_POLARITY(1'h1),
+    .WIDTH(32'd1)
+  ) ff1  (
+    .CLK(clk),
+    .D(i),
+    .Q(o[1])
+  );
+  \$dff  #(
+    .CLK_POLARITY(1'h1),
+    .WIDTH(32'd1)
+  ) ff0  (
+    .CLK(clk),
+    .D(i),
+    .Q(o[0])
+  );
+endmodule
+EOT
+
+opt_merge
+select -assert-count 1 a:init=2'bx1
diff --git a/tests/sat/clk2fflogic.ys b/tests/sat/clk2fflogic.ys
new file mode 100644
index 000000000..6d6d9e490
--- /dev/null
+++ b/tests/sat/clk2fflogic.ys
@@ -0,0 +1,66 @@
+read_verilog -icells <<EOT
+module top(input clk, d, s, r, output reg [17:0] q);
+always @(posedge clk or posedge s) if ( s) q[ 0] <= 1'b1; else q[ 0] <= d;
+always @(posedge clk or negedge s) if (!s) q[ 1] <= 1'b1; else q[ 1] <= d;
+always @(posedge clk or posedge r) if ( r) q[ 2] <= 1'b0; else q[ 2] <= d;
+always @(posedge clk or negedge r) if (!r) q[ 3] <= 1'b0; else q[ 3] <= d;
+always @(negedge clk or posedge s) if ( s) q[ 4] <= 1'b1; else q[ 4] <= d;
+always @(negedge clk or negedge s) if (!s) q[ 5] <= 1'b1; else q[ 5] <= d;
+always @(negedge clk or posedge r) if ( r) q[ 6] <= 1'b0; else q[ 6] <= d;
+always @(negedge clk or negedge r) if (!r) q[ 7] <= 1'b0; else q[ 7] <= d;
+
+// Seems like proc_dlatch always sets {SET,CLR}_POLARITY to true
+always @(posedge clk or posedge s or posedge r) if ( r) q[ 8] <= 1'b0; else if ( s) q[ 8] <= 1'b1; else q[ 8] <= d;
+//always @(posedge clk or posedge s or negedge r) if (!r) q[ 9] <= 1'b0; else if ( s) q[ 9] <= 1'b1; else q[ 9] <= d;
+//always @(posedge clk or negedge s or posedge r) if ( r) q[10] <= 1'b0; else if (!s) q[10] <= 1'b1; else q[10] <= d;
+//always @(posedge clk or negedge s or negedge r) if (!r) q[11] <= 1'b0; else if (!s) q[11] <= 1'b1; else q[11] <= d;
+$dffsr  #(.CLK_POLARITY(1'h1), .CLR_POLARITY(1'h0), .SET_POLARITY(1'h1), .WIDTH(32'd1)) ppn (.CLK(clk), .CLR(r), .D(d), .Q(q[ 9]), .SET(s));
+$dffsr  #(.CLK_POLARITY(1'h1), .CLR_POLARITY(1'h1), .SET_POLARITY(1'h0), .WIDTH(32'd1)) pnp (.CLK(clk), .CLR(r), .D(d), .Q(q[10]), .SET(s));
+$dffsr  #(.CLK_POLARITY(1'h1), .CLR_POLARITY(1'h0), .SET_POLARITY(1'h0), .WIDTH(32'd1)) pnn (.CLK(clk), .CLR(r), .D(d), .Q(q[11]), .SET(s));
+
+always @(negedge clk or posedge s or posedge r) if ( r) q[12] <= 1'b0; else if ( s) q[12] <= 1'b1; else q[12] <= d;
+//always @(negedge clk or posedge s or negedge r) if (!r) q[13] <= 1'b0; else if ( s) q[13] <= 1'b1; else q[13] <= d;
+//always @(negedge clk or negedge s or posedge r) if ( r) q[14] <= 1'b0; else if (!s) q[14] <= 1'b1; else q[14] <= d;
+//always @(negedge clk or negedge s or negedge r) if (!r) q[15] <= 1'b0; else if (!s) q[15] <= 1'b1; else q[15] <= d;
+$dffsr  #(.CLK_POLARITY(1'h0), .CLR_POLARITY(1'h0), .SET_POLARITY(1'h1), .WIDTH(32'd1)) npn (.CLK(clk), .CLR(r), .D(d), .Q(q[13]), .SET(s));
+$dffsr  #(.CLK_POLARITY(1'h0), .CLR_POLARITY(1'h1), .SET_POLARITY(1'h0), .WIDTH(32'd1)) nnp (.CLK(clk), .CLR(r), .D(d), .Q(q[14]), .SET(s));
+$dffsr  #(.CLK_POLARITY(1'h0), .CLR_POLARITY(1'h0), .SET_POLARITY(1'h0), .WIDTH(32'd1)) nnn (.CLK(clk), .CLR(r), .D(d), .Q(q[15]), .SET(s));
+
+always @(posedge clk) q[16] <= d;
+always @(negedge clk) q[17] <= d;
+endmodule
+EOT
+proc
+select -assert-count 8 t:$adff
+select -assert-count 8 t:$dffsr
+select -assert-count 2 t:$dff
+design -save gold
+
+simplemap
+select -assert-count 1 t:$_DFF_NN0_
+select -assert-count 1 t:$_DFF_NN1_
+select -assert-count 1 t:$_DFF_NP0_
+select -assert-count 1 t:$_DFF_NP1_
+select -assert-count 1 t:$_DFF_PN0_
+select -assert-count 1 t:$_DFF_PN1_
+select -assert-count 1 t:$_DFF_PP0_
+select -assert-count 1 t:$_DFF_PP1_
+stat
+select -assert-count 1 t:$_DFFSR_NNN_
+select -assert-count 1 t:$_DFFSR_NNP_
+select -assert-count 1 t:$_DFFSR_NPN_
+select -assert-count 1 t:$_DFFSR_NPP_
+select -assert-count 1 t:$_DFFSR_PNN_
+select -assert-count 1 t:$_DFFSR_PNP_
+select -assert-count 1 t:$_DFFSR_PPN_
+select -assert-count 1 t:$_DFFSR_PPP_
+select -assert-count 1 t:$_DFF_N_
+select -assert-count 1 t:$_DFF_P_
+design -stash gate
+
+design -import gold -as gold
+design -import gate -as gate
+clk2fflogic
+
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -verify -prove-asserts -show-ports -set-init-undef -seq 10 miter
diff --git a/tests/techmap/run-test.sh b/tests/techmap/run-test.sh
index 96489ff15..c16f204d9 100755
--- a/tests/techmap/run-test.sh
+++ b/tests/techmap/run-test.sh
@@ -6,7 +6,7 @@ for x in *.ys; do
 	echo "all:: run-$x"
 	echo "run-$x:"
 	echo "	@echo 'Running $x..'"
-	echo "	@../../yosys -ql ${x%.ys}.log $x"
+	echo "	@../../yosys -ql ${x%.ys}.log -e 'select out of bounds' $x"
 done
 for s in *.sh; do
 	if [ "$s" != "run-test.sh" ]; then
diff --git a/tests/techmap/shiftx2mux.ys b/tests/techmap/shiftx2mux.ys
new file mode 100644
index 000000000..eb29680f6
--- /dev/null
+++ b/tests/techmap/shiftx2mux.ys
@@ -0,0 +1,121 @@
+read_verilog <<EOT
+module sc1 (i1 ,
+            i2 ,
+            i3 ,
+            i4 ,
+            i5 ,
+            i6 ,
+            i7 ,
+            i8 ,
+            i9 ,
+            i10,
+            i11,
+            i12,
+            i13,
+            i14,
+            i15,
+            binary_out,
+            encoder_in,
+            enable
+);
+
+input [3:0]   i1 ;
+input [3:0]   i2 ;
+input [3:0]   i3 ;
+input [3:0]   i4 ;
+input [3:0]   i5 ;
+input [3:0]   i6 ;
+input [3:0]   i7 ;
+input [3:0]   i8 ;
+input [3:0]   i9 ;
+input [3:0]   i10 ;
+input [3:0]   i11 ;
+input [3:0]   i12 ;
+input [3:0]   i13 ;
+input [3:0]   i14 ;
+input [3:0]   i15 ;
+
+output reg [3:0] binary_out  ;
+
+input [3:0] encoder_in ;
+input  enable ;
+
+
+
+always @ (*)
+begin
+	binary_out = 0;
+	if (enable) begin
+		case (encoder_in)
+			4'h1 : binary_out = i1;
+			4'h2 : binary_out = i2;
+			4'h3 : binary_out = i3;
+			4'h4 : binary_out = i4;
+			4'h5 : binary_out = i5;
+			4'h6 : binary_out = i6;
+			4'h7 : binary_out = i7;
+			4'h8 : binary_out = i8;
+			4'h9 : binary_out = i9;
+			4'ha : binary_out = i10;
+			4'hb : binary_out = i11;/*
+			4'hc : binary_out = i12;
+			4'hd : binary_out = i13;
+			4'he : binary_out = i14;
+			4'hf : binary_out = i15;*/
+	       endcase
+       end
+end
+endmodule
+EOT
+
+proc
+pmux2shiftx
+design -save gold
+
+
+design -load gold
+techmap -D NO_LSB_FIRST_SHIFT_SHIFTX
+abc -lut 6
+select -assert-min 17 t:$lut
+
+
+design -load gold
+techmap
+abc -lut 6
+select -assert-count 16 t:$lut
+
+design -stash gate
+design -import gold -as gold
+design -import gate -as gate
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -verify -prove-asserts -show-ports miter
+
+
+design -load gold
+techmap -D NO_LSB_FIRST_SHIFT_SHIFTX
+abc9 -lut 6
+select -assert-min 17 t:$lut
+
+
+design -load gold
+techmap
+abc9 -lut 6
+select -assert-count 16 t:$lut
+
+design -stash gate
+design -import gold -as gold
+design -import gate -as gate
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -verify -prove-asserts -show-ports miter
+
+
+design -reset
+read_verilog <<EOT
+module top(input [6:0] A, input [1:0] B, output [1:0] Y);
+wire [7:0] AA = {1'bx, A};
+assign Y = AA[B*2 +: 2];
+endmodule
+EOT
+opt
+wreduce
+equiv_opt techmap
diff --git a/tests/various/sformatf.ys b/tests/various/sformatf.ys
new file mode 100644
index 000000000..66d6b0dbe
--- /dev/null
+++ b/tests/various/sformatf.ys
@@ -0,0 +1,12 @@
+read_verilog <<EOT
+
+module top;
+	localparam a = $sformatf("0x%x", 8'h5A);
+	localparam b = $sformatf("%d", 4'b011);
+	generate
+		if (a != "0x5a") $error("a incorrect!");
+		if (b != "3") $error("b incorrect!");
+	endgenerate
+endmodule
+
+EOT
diff --git a/tests/various/sv_implicit_ports.sh b/tests/various/sv_implicit_ports.sh
new file mode 100755
index 000000000..9a01447f7
--- /dev/null
+++ b/tests/various/sv_implicit_ports.sh
@@ -0,0 +1,124 @@
+#!/bin/bash
+
+trap 'echo "ERROR in sv_implicit_ports.sh" >&2; exit 1' ERR
+
+# Simple case
+../../yosys -f "verilog -sv" -qp "prep -flatten -top top; select -assert-count 1 t:\$add" - <<EOT
+module add(input [7:0] a, input [7:0] b, output [7:0] q);
+	assign q = a + b;
+endmodule
+
+module top(input [7:0] a, output [7:0] q);
+	wire [7:0] b = 8'd42;
+	add add_i(.*);
+endmodule
+EOT
+
+# Generate block
+../../yosys -f "verilog -sv" -qp "prep -flatten -top top; select -assert-count 1 t:\$add" - <<EOT
+module add(input [7:0] a, input [7:0] b, output [7:0] q);
+assign q = a + b;
+endmodule
+
+module top(input [7:0] a, output [7:0] q);
+	generate
+	if (1) begin:ablock
+		wire [7:0] b = 8'd42;
+		add add_i(.*);
+	end
+	endgenerate
+endmodule
+EOT
+
+# Missing wire
+((../../yosys -f "verilog -sv" -qp "hierarchy -top top" - || true) <<EOT
+module add(input [7:0] a, input [7:0] b, output [7:0] q);
+	assign q = a + b;
+endmodule
+
+module top(input [7:0] a, output [7:0] q);
+	add add_i(.*);
+endmodule
+EOT
+) 2>&1 | grep -F "ERROR: No matching wire for implicit port connection \`b' of cell top.add_i (add)." > /dev/null
+
+# Incorrectly sized wire
+((../../yosys -f "verilog -sv" -qp "hierarchy -top top" - || true) <<EOT
+module add(input [7:0] a, input [7:0] b, output [7:0] q);
+	assign q = a + b;
+endmodule
+
+module top(input [7:0] a, output [7:0] q);
+	wire [6:0] b = 6'd42;
+	add add_i(.*);
+endmodule
+EOT
+) 2>&1 | grep -F "ERROR: Width mismatch between wire (7 bits) and port (8 bits) for implicit port connection \`b' of cell top.add_i (add)." > /dev/null
+
+# Defaults
+../../yosys -f "verilog -sv" -qp "prep -flatten -top top; select -assert-count 1 t:\$add" - <<EOT
+module add(input [7:0] a = 8'd00, input [7:0] b = 8'd01, output [7:0] q);
+assign q = a + b;
+endmodule
+
+module top(input [7:0] a, output [7:0] q);
+	add add_i(.*);
+endmodule
+EOT
+
+# Parameterised module
+../../yosys -f "verilog -sv" -qp "prep -flatten -top top; select -assert-count 1 t:\$add" - <<EOT
+module add #(parameter N=3) (input [N-1:0] a = 8'd00, input [N-1:0] b = 8'd01, output [N-1:0] q);
+assign q = a + b;
+endmodule
+
+module top(input [7:0] a, output [7:0] q);
+	add #(.N(8)) add_i(.*);
+endmodule
+EOT
+
+# Parameterised blackbox module
+../../yosys -f "verilog -sv" -qp "prep -flatten -top top; select -assert-count 1 t:add" - <<EOT
+(* blackbox *)
+module add #(parameter N=3) (input [N-1:0] a, b, output [N-1:0] q);
+endmodule
+
+module top(input [7:0] a, b, output [7:0] q);
+	add #(.N(8)) add_i(.*);
+endmodule
+EOT
+
+# Parameterised blackbox module - incorrect width
+((../../yosys -f "verilog -sv" -qp "prep -flatten -top top; select -assert-count 1 t:add" - || true) <<EOT
+(* blackbox *)
+module add #(parameter N=3) (input [N-1:0] a, b, output [N-1:0] q);
+endmodule
+
+module top(input [7:0] a, b, output [7:0] q);
+	add #(.N(6)) add_i(.*);
+endmodule
+EOT
+) 2>&1 | grep -F "ERROR: Width mismatch between wire (8 bits) and port (6 bits) for implicit port connection \`q' of cell top.add_i (add)." > /dev/null
+
+# Mixed implicit and explicit 1
+../../yosys -f "verilog -sv" -qp "prep -flatten -top top; select -assert-count 1 t:\$add" - <<EOT
+module add(input [7:0] a, input [7:0] b, output [7:0] q);
+	assign q = a + b;
+endmodule
+
+module top(input [7:0] a, output [7:0] q);
+	add add_i(.b(8'd42), .*);
+endmodule
+EOT
+
+# Mixed implicit and explicit 2
+(../../yosys -f "verilog -sv" -qp "prep -flatten -top top; select -assert-count 1 t:\$add" - <<EOT
+module add(input [7:0] a, input [7:0] b, output [7:0] q);
+	assign q = a + b;
+endmodule
+
+module top(input [7:0] a, input [9:0] b, output [7:0] q);
+	add add_i(.b, .*);
+endmodule
+EOT
+) 2>&1 | grep -F "Warning: Resizing cell port top.add_i.b from 10 bits to 8 bits." > /dev/null