aboutsummaryrefslogtreecommitdiffstats
path: root/tests/various
diff options
context:
space:
mode:
Diffstat (limited to 'tests/various')
-rw-r--r--tests/various/.gitignore6
-rw-r--r--tests/various/abc9.v9
-rw-r--r--tests/various/abc9.ys24
-rw-r--r--tests/various/async.sh11
-rw-r--r--tests/various/async.v108
-rw-r--r--tests/various/gzip_verilog.v.gzbin0 -> 82 bytes
-rw-r--r--tests/various/gzip_verilog.ys2
-rw-r--r--tests/various/mem2reg.ys14
-rw-r--r--tests/various/muxcover.ys461
-rw-r--r--tests/various/muxpack.v259
-rw-r--r--tests/various/muxpack.ys268
-rw-r--r--tests/various/opt_rmdff.v50
-rw-r--r--tests/various/opt_rmdff.ys26
-rw-r--r--tests/various/pmgen_reduce.ys21
-rw-r--r--tests/various/pmux2shiftx.v10
-rw-r--r--tests/various/pmux2shiftx.ys21
-rwxr-xr-xtests/various/run-test.sh26
-rw-r--r--tests/various/script.ys20
-rw-r--r--tests/various/shregmap.v48
-rw-r--r--tests/various/shregmap.ys66
-rw-r--r--tests/various/signext.ys33
-rw-r--r--tests/various/specify.v11
-rw-r--r--tests/various/specify.ys2
-rw-r--r--tests/various/wreduce.ys79
-rw-r--r--tests/various/write_gzip.ys16
25 files changed, 1497 insertions, 94 deletions
diff --git a/tests/various/.gitignore b/tests/various/.gitignore
index 397b4a762..4b286fd61 100644
--- a/tests/various/.gitignore
+++ b/tests/various/.gitignore
@@ -1 +1,5 @@
-*.log
+/*.log
+/*.out
+/write_gzip.v
+/write_gzip.v.gz
+/run-test.mk
diff --git a/tests/various/abc9.v b/tests/various/abc9.v
new file mode 100644
index 000000000..a08b613a8
--- /dev/null
+++ b/tests/various/abc9.v
@@ -0,0 +1,9 @@
+module abc9_test027(output reg o);
+initial o = 1'b0;
+always @*
+ o <= ~o;
+endmodule
+
+module abc9_test028(input i, output o);
+unknown u(~i, o);
+endmodule
diff --git a/tests/various/abc9.ys b/tests/various/abc9.ys
new file mode 100644
index 000000000..5c9a4075d
--- /dev/null
+++ b/tests/various/abc9.ys
@@ -0,0 +1,24 @@
+read_verilog abc9.v
+design -save read
+hierarchy -top abc9_test027
+proc
+design -save gold
+
+abc9 -lut 4
+check
+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 read
+hierarchy -top abc9_test028
+proc
+
+abc9 -lut 4
+select -assert-count 1 t:$lut r:LUT=2'b01 r:WIDTH=1 %i %i
+select -assert-count 1 t:unknown
+select -assert-none t:$lut t:unknown %% t: %D
diff --git a/tests/various/async.sh b/tests/various/async.sh
new file mode 100644
index 000000000..7c41d6d94
--- /dev/null
+++ b/tests/various/async.sh
@@ -0,0 +1,11 @@
+#!/bin/bash
+set -ex
+../../yosys -q -o async_syn.v -p 'synth; rename uut syn' async.v
+../../yosys -q -o async_prp.v -p 'prep; rename uut prp' async.v
+../../yosys -q -o async_a2s.v -p 'prep; async2sync; rename uut a2s' async.v
+../../yosys -q -o async_ffl.v -p 'prep; clk2fflogic; rename uut ffl' async.v
+iverilog -o async_sim -DTESTBENCH async.v async_???.v
+vvp -N async_sim > async.out
+tail async.out
+grep PASS async.out
+rm -f async_???.v async_sim async.out async.vcd
diff --git a/tests/various/async.v b/tests/various/async.v
new file mode 100644
index 000000000..c27e30c4b
--- /dev/null
+++ b/tests/various/async.v
@@ -0,0 +1,108 @@
+`define MAXQ 2
+module uut (
+ input clk,
+ input d, r, e,
+ output [`MAXQ:0] q
+);
+ reg q0;
+ always @(posedge clk) begin
+ if (r)
+ q0 <= 0;
+ else if (e)
+ q0 <= d;
+ end
+
+ reg q1;
+ always @(posedge clk, posedge r) begin
+ if (r)
+ q1 <= 0;
+ else if (e)
+ q1 <= d;
+ end
+
+ reg q2;
+ always @(posedge clk, negedge r) begin
+ if (!r)
+ q2 <= 0;
+ else if (!e)
+ q2 <= d;
+ end
+
+ assign q = {q2, q1, q0};
+endmodule
+
+`ifdef TESTBENCH
+module \$ff #(
+ parameter integer WIDTH = 1
+) (
+ input [WIDTH-1:0] D,
+ output reg [WIDTH-1:0] Q
+);
+ wire sysclk = testbench.sysclk;
+ always @(posedge sysclk)
+ Q <= D;
+endmodule
+
+module testbench;
+ reg sysclk;
+ always #5 sysclk = (sysclk === 1'b0);
+
+ reg clk;
+ always @(posedge sysclk) clk = (clk === 1'b0);
+
+ reg d, r, e;
+
+ wire [`MAXQ:0] q_uut;
+ uut uut (.clk(clk), .d(d), .r(r), .e(e), .q(q_uut));
+
+ wire [`MAXQ:0] q_syn;
+ syn syn (.clk(clk), .d(d), .r(r), .e(e), .q(q_syn));
+
+ wire [`MAXQ:0] q_prp;
+ prp prp (.clk(clk), .d(d), .r(r), .e(e), .q(q_prp));
+
+ wire [`MAXQ:0] q_a2s;
+ a2s a2s (.clk(clk), .d(d), .r(r), .e(e), .q(q_a2s));
+
+ wire [`MAXQ:0] q_ffl;
+ ffl ffl (.clk(clk), .d(d), .r(r), .e(e), .q(q_ffl));
+
+ task printq;
+ reg [5*8-1:0] msg;
+ begin
+ msg = "OK";
+ if (q_uut !== q_syn) msg = "SYN";
+ if (q_uut !== q_prp) msg = "PRP";
+ if (q_uut !== q_a2s) msg = "A2S";
+ if (q_uut !== q_ffl) msg = "FFL";
+ $display("%6t %b %b %b %b %b %s", $time, q_uut, q_syn, q_prp, q_a2s, q_ffl, msg);
+ if (msg != "OK") $finish;
+ end
+ endtask
+
+ initial if(0) begin
+ $dumpfile("async.vcd");
+ $dumpvars(0, testbench);
+ end
+
+ initial begin
+ @(posedge clk);
+ d <= 0;
+ r <= 0;
+ e <= 0;
+ @(posedge clk);
+ e <= 1;
+ @(posedge clk);
+ e <= 0;
+ repeat (10000) begin
+ @(posedge clk);
+ printq;
+ d <= $random;
+ r <= $random;
+ e <= $random;
+ end
+ $display("PASS");
+ $finish;
+ end
+endmodule
+`endif
diff --git a/tests/various/gzip_verilog.v.gz b/tests/various/gzip_verilog.v.gz
new file mode 100644
index 000000000..c52a95358
--- /dev/null
+++ b/tests/various/gzip_verilog.v.gz
Binary files differ
diff --git a/tests/various/gzip_verilog.ys b/tests/various/gzip_verilog.ys
new file mode 100644
index 000000000..870317e80
--- /dev/null
+++ b/tests/various/gzip_verilog.ys
@@ -0,0 +1,2 @@
+read_verilog gzip_verilog.v.gz
+select -assert-any top
diff --git a/tests/various/mem2reg.ys b/tests/various/mem2reg.ys
new file mode 100644
index 000000000..85d6267c5
--- /dev/null
+++ b/tests/various/mem2reg.ys
@@ -0,0 +1,14 @@
+read_verilog <<EOT
+module top;
+parameter DATADEPTH=2;
+parameter DATAWIDTH=1;
+(* keep, nomem2reg *) reg [DATAWIDTH-1:0] data1 [DATADEPTH-1:0];
+(* keep, mem2reg *) reg [DATAWIDTH-1:0] data2 [DATADEPTH-1:0];
+endmodule
+EOT
+
+proc
+cd top
+select -assert-count 1 m:data1 a:src=<<EOT:4 %i
+select -assert-count 2 w:data2[*] a:src=<<EOT:5 %i
+select -assert-none a:mem2reg
diff --git a/tests/various/muxcover.ys b/tests/various/muxcover.ys
index 7ac460f13..67e9625e6 100644
--- a/tests/various/muxcover.ys
+++ b/tests/various/muxcover.ys
@@ -13,7 +13,7 @@ read_verilog -formal <<EOT
EOT
-## Examle usage for "pmuxtree" and "muxcover"
+## Example usage for "pmuxtree" and "muxcover"
proc
pmuxtree
@@ -49,3 +49,462 @@ hierarchy -top equiv
equiv_simple -undef
equiv_status -assert
+## Partial matching MUX4
+
+design -reset
+read_verilog -formal <<EOT
+module mux_if_bal_3_1 #(parameter N=3, parameter W=1) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o);
+always @* begin
+ o <= {{W{{1'bx}}}};
+ if (s[0] == 1'b0)
+ if (s[1] == 1'b0)
+ o <= i[0*W+:W];
+ else
+ o <= i[1*W+:W];
+ else
+ if (s[1] == 1'b0)
+ o <= i[2*W+:W];
+end
+endmodule
+EOT
+prep
+design -save gold
+
+techmap
+muxcover -mux4=150
+select -assert-count 0 t:$_MUX_
+select -assert-count 1 t:$_MUX4_
+select -assert-count 0 t:$_MUX8_
+select -assert-count 0 t:$_MUX16_
+techmap -map +/simcells.v t:$_MUX4_
+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
+
+## Partial matching MUX8
+
+design -reset
+read_verilog -formal <<EOT
+module mux_if_bal_5_1 #(parameter N=5, parameter W=1) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o);
+always @* begin
+ o <= {{W{{1'bx}}}};
+ if (s[0] == 1'b0)
+ if (s[1] == 1'b0)
+ if (s[2] == 1'b0)
+ o <= i[0*W+:W];
+ else
+ o <= i[1*W+:W];
+ else
+ if (s[2] == 1'b0)
+ o <= i[2*W+:W];
+ else
+ o <= i[3*W+:W];
+ else
+ if (s[1] == 1'b0)
+ if (s[2] == 1'b0)
+ o <= i[4*W+:W];
+end
+endmodule
+EOT
+prep
+design -save gold
+
+techmap
+muxcover -mux4=150 -mux8=200
+clean
+opt_expr -mux_bool
+select -assert-count 0 t:$_MUX_
+select -assert-count 0 t:$_MUX4_
+select -assert-count 1 t:$_MUX8_
+select -assert-count 0 t:$_MUX16_
+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 gold gate miter
+sat -verify -prove-asserts -show-ports miter
+
+## Partial matching MUX16
+
+design -reset
+read_verilog -formal <<EOT
+module mux_if_bal_9_1 #(parameter N=9, parameter W=1) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o);
+always @* begin
+ o <= {{W{{1'bx}}}};
+ if (s[0] == 1'b0)
+ if (s[1] == 1'b0)
+ if (s[2] == 1'b0)
+ if (s[3] == 1'b0)
+ o <= i[0*W+:W];
+ else
+ o <= i[1*W+:W];
+ else
+ if (s[3] == 1'b0)
+ o <= i[2*W+:W];
+ else
+ o <= i[3*W+:W];
+ else
+ if (s[2] == 1'b0)
+ if (s[3] == 1'b0)
+ o <= i[4*W+:W];
+ else
+ o <= i[5*W+:W];
+ else
+ if (s[3] == 1'b0)
+ o <= i[6*W+:W];
+ else
+ o <= i[7*W+:W];
+ else
+ if (s[1] == 1'b0)
+ if (s[2] == 1'b0)
+ if (s[3] == 1'b0)
+ o <= i[8*W+:W];
+end
+endmodule
+EOT
+prep
+design -save gold
+
+techmap
+muxcover -mux4=150 -mux8=200 -mux16=250
+clean
+opt_expr -mux_bool
+select -assert-count 0 t:$_MUX_
+select -assert-count 0 t:$_MUX4_
+select -assert-count 0 t:$_MUX8_
+select -assert-count 1 t:$_MUX16_
+techmap -map +/simcells.v t:$_MUX16_
+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
+
+## MUX2 in MUX4 :: https://github.com/YosysHQ/yosys/issues/1132
+
+design -reset
+read_verilog -formal <<EOT
+module mux2in4(input [1:0] i, input s, output o);
+ assign o = s ? i[1] : i[0];
+endmodule
+EOT
+prep
+design -save gold
+
+techmap
+muxcover -mux4=99 -nodecode
+clean
+opt_expr -mux_bool
+select -assert-count 0 t:$_MUX_
+select -assert-count 1 t:$_MUX4_
+select -assert-count 0 t:$_MUX8_
+select -assert-count 0 t:$_MUX16_
+techmap -map +/simcells.v t:$_MUX4_
+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
+
+## MUX2 in MUX8 :: https://github.com/YosysHQ/yosys/issues/1132
+
+design -reset
+read_verilog -formal <<EOT
+module mux2in8(input [1:0] i, input s, output o);
+ assign o = s ? i[1] : i[0];
+endmodule
+EOT
+prep
+design -save gold
+
+techmap
+muxcover -mux8=99 -nodecode
+clean
+opt_expr -mux_bool
+select -assert-count 0 t:$_MUX_
+select -assert-count 0 t:$_MUX4_
+select -assert-count 1 t:$_MUX8_
+select -assert-count 0 t:$_MUX16_
+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 gold gate miter
+sat -verify -prove-asserts -show-ports miter
+
+## MUX4 in MUX8 :: https://github.com/YosysHQ/yosys/issues/1132
+
+design -reset
+read_verilog -formal <<EOT
+module mux4in8(input [3:0] i, input [1:0] s, output o);
+ assign o = s[1] ? (s[0] ? i[3] : i[2]) : (s[0] ? i[1] : i[0]);
+endmodule
+EOT
+prep
+design -save gold
+
+techmap
+muxcover -mux8=299 -nodecode
+clean
+opt_expr -mux_bool
+select -assert-count 0 t:$_MUX_
+select -assert-count 0 t:$_MUX4_
+select -assert-count 1 t:$_MUX8_
+select -assert-count 0 t:$_MUX16_
+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 gold gate miter
+sat -verify -prove-asserts -show-ports miter
+
+## MUX2 in MUX16 :: https://github.com/YosysHQ/yosys/issues/1132
+
+design -reset
+read_verilog -formal <<EOT
+module mux2in16(input [1:0] i, input s, output o);
+ assign o = s ? i[1] : i[0];
+endmodule
+EOT
+prep
+design -save gold
+
+techmap
+muxcover -mux16=99 -nodecode
+clean
+opt_expr -mux_bool
+select -assert-count 0 t:$_MUX_
+select -assert-count 0 t:$_MUX4_
+select -assert-count 0 t:$_MUX8_
+select -assert-count 1 t:$_MUX16_
+techmap -map +/simcells.v t:$_MUX16_
+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
+
+## MUX4 in MUX16 :: https://github.com/YosysHQ/yosys/issues/1132
+
+design -reset
+read_verilog -formal <<EOT
+module mux4in16(input [3:0] i, input [1:0] s, output o);
+ assign o = s[1] ? (s[0] ? i[3] : i[2]) : (s[0] ? i[1] : i[0]);
+endmodule
+EOT
+prep
+design -save gold
+
+techmap
+muxcover -mux16=299 -nodecode
+clean
+opt_expr -mux_bool
+select -assert-count 0 t:$_MUX_
+select -assert-count 0 t:$_MUX4_
+select -assert-count 0 t:$_MUX8_
+select -assert-count 1 t:$_MUX16_
+techmap -map +/simcells.v t:$_MUX16_
+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
+
+## MUX8 in MUX16 :: https://github.com/YosysHQ/yosys/issues/1132
+
+design -reset
+read_verilog -formal <<EOT
+module mux4in16(input [7:0] i, input [2:0] s, output o);
+ assign o = s[2] ? s[1] ? (s[0] ? i[3] : i[2]) : (s[0] ? i[1] : i[0])
+ : s[1] ? (s[0] ? i[7] : i[6]) : (s[0] ? i[5] : i[4]);
+endmodule
+EOT
+prep
+design -save gold
+
+techmap
+muxcover -mux16=699 -nodecode
+clean
+opt_expr -mux_bool
+select -assert-count 0 t:$_MUX_
+select -assert-count 0 t:$_MUX4_
+select -assert-count 0 t:$_MUX8_
+select -assert-count 1 t:$_MUX16_
+techmap -map +/simcells.v t:$_MUX16_
+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
+
+## mux_if_bal_5_1 :: https://github.com/YosysHQ/yosys/issues/1132
+
+design -reset
+read_verilog -formal <<EOT
+module mux_if_bal_5_1 #(parameter N=5, parameter W=1) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o);
+always @* begin
+ o <= {{W{{1'bx}}}};
+ if (s[0] == 1'b0)
+ if (s[1] == 1'b0)
+ if (s[2] == 1'b0)
+ o <= i[0*W+:W];
+ else
+ o <= i[1*W+:W];
+ else
+ if (s[2] == 1'b0)
+ o <= i[2*W+:W];
+ else
+ o <= i[3*W+:W];
+ else
+ if (s[1] == 1'b0)
+ if (s[2] == 1'b0)
+ o <= i[4*W+:W];
+end
+endmodule
+EOT
+prep
+design -save gold
+
+wreduce
+opt -full
+techmap
+muxcover -mux8=350
+clean
+opt_expr -mux_bool
+select -assert-count 0 t:$_MUX_
+select -assert-count 0 t:$_MUX4_
+select -assert-count 1 t:$_MUX8_
+select -assert-count 0 t:$_MUX16_
+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
+
+## mux_if_bal_5_1 (nodecode) :: https://github.com/YosysHQ/yosys/issues/1132
+design -load gold
+
+wreduce
+opt -full
+techmap
+muxcover -mux8=350 -nodecode
+clean
+opt_expr -mux_bool
+select -assert-count 0 t:$_MUX_
+select -assert-count 0 t:$_MUX4_
+select -assert-count 1 t:$_MUX8_
+select -assert-count 0 t:$_MUX16_
+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
+
+## mux_if_bal_9_1 :: https://github.com/YosysHQ/yosys/issues/1132
+
+design -reset
+read_verilog -formal <<EOT
+module mux_if_bal_9_1 #(parameter N=9, parameter W=1) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o);
+always @* begin
+ o <= {{W{{1'bx}}}};
+ if (s[3] == 1'b0)
+ if (s[2] == 1'b0)
+ if (s[1] == 1'b0)
+ if (s[0] == 1'b0)
+ o <= i[0*W+:W];
+ else
+ o <= i[1*W+:W];
+ else
+ if (s[0] == 1'b0)
+ o <= i[2*W+:W];
+ else
+ o <= i[3*W+:W];
+ else
+ if (s[1] == 1'b0)
+ if (s[0] == 1'b0)
+ o <= i[4*W+:W];
+ else
+ o <= i[5*W+:W];
+ else
+ if (s[0] == 1'b0)
+ o <= i[6*W+:W];
+ else
+ o <= i[7*W+:W];
+ else
+ if (s[2] == 1'b0)
+ if (s[1] == 1'b0)
+ if (s[0] == 1'b0)
+ o <= i[8*W+:W];
+end
+endmodule
+EOT
+prep
+design -save gold
+
+wreduce
+opt -full
+techmap
+muxcover -mux16=750
+clean
+opt_expr -mux_bool
+select -assert-count 0 t:$_MUX_
+select -assert-count 0 t:$_MUX4_
+select -assert-count 0 t:$_MUX8_
+select -assert-count 1 t:$_MUX16_
+techmap -map +/simcells.v t:$_MUX16_
+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
+
+## mux_if_bal_9_1 (nodecode) :: https://github.com/YosysHQ/yosys/issues/1132
+
+design -load gold
+
+wreduce
+opt -full
+techmap
+muxcover -mux16=750 -nodecode
+clean
+opt_expr -mux_bool
+select -assert-count 0 t:$_MUX_
+select -assert-count 0 t:$_MUX4_
+select -assert-count 0 t:$_MUX8_
+select -assert-count 1 t:$_MUX16_
+techmap -map +/simcells.v t:$_MUX16_
+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/muxpack.v b/tests/various/muxpack.v
new file mode 100644
index 000000000..33ece1f16
--- /dev/null
+++ b/tests/various/muxpack.v
@@ -0,0 +1,259 @@
+module mux_if_unbal_4_1 #(parameter N=4, parameter W=1) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o);
+always @*
+ if (s == 0) o <= i[0*W+:W];
+ else if (s == 1) o <= i[1*W+:W];
+ else if (s == 2) o <= i[2*W+:W];
+ else if (s == 3) o <= i[3*W+:W];
+ else o <= {W{1'bx}};
+endmodule
+
+module mux_if_unbal_5_3 #(parameter N=5, parameter W=3) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o);
+always @* begin
+ o <= {W{1'bx}};
+ if (s == 0) o <= i[0*W+:W];
+ if (s == 1) o <= i[1*W+:W];
+ if (s == 2) o <= i[2*W+:W];
+ if (s == 3) o <= i[3*W+:W];
+ if (s == 4) o <= i[4*W+:W];
+end
+endmodule
+
+module mux_if_unbal_5_3_invert #(parameter N=5, parameter W=3) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o);
+always @*
+ if (s != 0)
+ if (s != 1)
+ if (s != 2)
+ if (s != 3)
+ if (s != 4) o <= i[4*W+:W];
+ else o <= i[0*W+:W];
+ else o <= i[3*W+:W];
+ else o <= i[2*W+:W];
+ else o <= i[1*W+:W];
+ else o <= {W{1'bx}};
+endmodule
+
+module mux_if_unbal_5_3_width_mismatch #(parameter N=5, parameter W=3) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o);
+always @* begin
+ o <= {W{1'bx}};
+ if (s == 0) o <= i[0*W+:W];
+ if (s == 1) o <= i[1*W+:W];
+ if (s == 2) o[W-2:0] <= i[2*W+:W-1];
+ if (s == 3) o <= i[3*W+:W];
+ if (s == 4) o <= i[4*W+:W];
+end
+endmodule
+
+module mux_if_unbal_4_1_missing #(parameter N=5, parameter W=3) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o);
+always @* begin
+ if (s == 0) o <= i[0*W+:W];
+// else if (s == 1) o <= i[1*W+:W];
+// else if (s == 2) o <= i[2*W+:W];
+ else if (s == 3) o <= i[3*W+:W];
+ else o <= {W{1'bx}};
+end
+endmodule
+
+module mux_if_unbal_5_3_order #(parameter N=5, parameter W=3) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o);
+always @* begin
+ o <= {W{1'bx}};
+ if (s == 3) o <= i[3*W+:W];
+ if (s == 2) o <= i[2*W+:W];
+ if (s == 1) o <= i[1*W+:W];
+ if (s == 4) o <= i[4*W+:W];
+ if (s == 0) o <= i[0*W+:W];
+end
+endmodule
+
+module mux_if_unbal_4_1_nonexcl #(parameter N=4, parameter W=1) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o);
+always @*
+ if (s == 0) o <= i[0*W+:W];
+ else if (s == 1) o <= i[1*W+:W];
+ else if (s == 2) o <= i[2*W+:W];
+ else if (s == 3) o <= i[3*W+:W];
+ else if (s == 0) o <= {W{1'b0}};
+ else o <= {W{1'bx}};
+endmodule
+
+module mux_if_unbal_5_3_nonexcl #(parameter N=5, parameter W=3) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o);
+always @* begin
+ o <= {W{1'bx}};
+ if (s == 0) o <= i[0*W+:W];
+ if (s == 1) o <= i[1*W+:W];
+ if (s == 2) o <= i[2*W+:W];
+ if (s == 3) o <= i[3*W+:W];
+ if (s == 4) o <= i[4*W+:W];
+ if (s == 0) o <= i[2*W+:W];
+end
+endmodule
+
+module mux_case_unbal_8_7#(parameter N=8, parameter W=7) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o);
+always @* begin
+ o <= {W{1'bx}};
+ case (s)
+ 0: o <= i[0*W+:W];
+ default:
+ case (s)
+ 1: o <= i[1*W+:W];
+ 2: o <= i[2*W+:W];
+ default:
+ case (s)
+ 3: o <= i[3*W+:W];
+ 4: o <= i[4*W+:W];
+ 5: o <= i[5*W+:W];
+ default:
+ case (s)
+ 6: o <= i[6*W+:W];
+ default: o <= i[7*W+:W];
+ endcase
+ endcase
+ endcase
+ endcase
+end
+endmodule
+
+module mux_if_bal_8_2 #(parameter N=8, parameter W=2) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o);
+always @*
+ if (s[0] == 1'b0)
+ if (s[1] == 1'b0)
+ if (s[2] == 1'b0)
+ o <= i[0*W+:W];
+ else
+ o <= i[1*W+:W];
+ else
+ if (s[2] == 1'b0)
+ o <= i[2*W+:W];
+ else
+ o <= i[3*W+:W];
+ else
+ if (s[1] == 1'b0)
+ if (s[2] == 1'b0)
+ o <= i[4*W+:W];
+ else
+ o <= i[5*W+:W];
+ else
+ if (s[2] == 1'b0)
+ o <= i[6*W+:W];
+ else
+ o <= i[7*W+:W];
+endmodule
+
+module mux_if_bal_5_1 #(parameter N=5, parameter W=1) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o);
+always @*
+ if (s[0] == 1'b0)
+ if (s[1] == 1'b0)
+ if (s[2] == 1'b0)
+ o <= i[0*W+:W];
+ else
+ o <= i[1*W+:W];
+ else
+ if (s[2] == 1'b0)
+ o <= i[2*W+:W];
+ else
+ o <= i[3*W+:W];
+ else
+ o <= i[4*W+:W];
+endmodule
+
+module cliffordwolf_nonexclusive_select (
+ input wire x, y, z,
+ input wire a, b, c, d,
+ output reg o
+);
+ always @* begin
+ o = a;
+ if (x) o = b;
+ if (y) o = c;
+ if (z) o = d;
+ end
+endmodule
+
+module cliffordwolf_freduce (
+ input wire [1:0] s,
+ input wire a, b, c, d,
+ output reg [3:0] o
+);
+ always @* begin
+ o = {4{a}};
+ if (s == 0) o = {3{b}};
+ if (s == 1) o = {2{c}};
+ if (s == 2) o = d;
+ end
+endmodule
+
+module case_nonexclusive_select (
+ input wire [1:0] x, y,
+ input wire a, b, c, d, e,
+ output reg o
+);
+ always @* begin
+ case (x)
+ 0: o = b;
+ 2: o = b;
+ 1: o = c;
+ default: begin
+ o = a;
+ if (y == 0) o = d;
+ if (y == 1) o = e;
+ end
+ endcase
+ end
+endmodule
+
+module case_nonoverlap (
+ input wire [2:0] x,
+ input wire a, b, c, d, e,
+ output reg o
+);
+ always @* begin
+ case (x)
+ 0, 2: o = b; // Creates $reduce_or
+ 1: o = c;
+ default:
+ case (x)
+ 3: o = d; 4: o = d; // Creates $reduce_or
+ 5: o = e;
+ default: o = 1'b0;
+ endcase
+ endcase
+ end
+endmodule
+
+module case_overlap (
+ input wire [2:0] x,
+ input wire a, b, c, d, e,
+ output reg o
+);
+ always @* begin
+ case (x)
+ 0, 2: o = b; // Creates $reduce_or
+ 1: o = c;
+ default:
+ case (x)
+ 0: o = 1'b1; // OVERLAP!
+ 3, 4: o = d; // Creates $reduce_or
+ 5: o = e;
+ default: o = 1'b0;
+ endcase
+ endcase
+ end
+endmodule
+
+module case_overlap2 (
+ input wire [2:0] x,
+ input wire a, b, c, d, e,
+ output reg o
+);
+ always @* begin
+ case (x)
+ 0: o = b; 2: o = b; // Creates $reduce_or
+ 1: o = c;
+ default:
+ case (x)
+ 0: o = d; 2: o = d; // Creates $reduce_or
+ 3: o = d; 4: o = d; // Creates $reduce_or
+ 5: o = e;
+ default: o = 1'b0;
+ endcase
+ endcase
+ end
+endmodule
diff --git a/tests/various/muxpack.ys b/tests/various/muxpack.ys
new file mode 100644
index 000000000..3e90419af
--- /dev/null
+++ b/tests/various/muxpack.ys
@@ -0,0 +1,268 @@
+read_verilog muxpack.v
+design -save read
+
+hierarchy -top mux_if_unbal_4_1
+prep
+design -save gold
+muxpack
+opt
+#stat
+select -assert-count 0 t:$mux
+select -assert-count 1 t:$pmux
+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 read
+hierarchy -top mux_if_unbal_5_3
+prep
+design -save gold
+muxpack
+opt
+#stat
+select -assert-count 0 t:$mux
+select -assert-count 1 t:$pmux
+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
+
+# TODO: Currently ExclusiveDatabase only analyses $eq cells
+#design -load read
+#hierarchy -top mux_if_unbal_5_3_invert
+#prep
+#design -save gold
+#muxpack
+#opt
+#stat
+#select -assert-count 0 t:$mux
+#select -assert-count 1 t:$pmux
+#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 read
+hierarchy -top mux_if_unbal_5_3_width_mismatch
+prep
+design -save gold
+muxpack
+opt
+#stat
+select -assert-count 0 t:$mux
+select -assert-count 2 t:$pmux
+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 read
+hierarchy -top mux_if_unbal_4_1_missing
+prep
+design -save gold
+muxpack
+opt
+#stat
+select -assert-count 0 t:$mux
+select -assert-count 1 t:$pmux
+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 read
+hierarchy -top mux_if_unbal_5_3_order
+prep
+design -save gold
+muxpack
+opt
+#stat
+select -assert-count 0 t:$mux
+select -assert-count 1 t:$pmux
+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 read
+hierarchy -top mux_if_unbal_4_1_nonexcl
+prep
+design -save gold
+muxpack
+opt
+#stat
+select -assert-count 0 t:$mux
+select -assert-count 1 t:$pmux
+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 read
+hierarchy -top mux_if_unbal_5_3_nonexcl
+prep
+design -save gold
+muxpack
+opt
+#stat
+select -assert-count 0 t:$mux
+select -assert-count 1 t:$pmux
+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 read
+hierarchy -top mux_case_unbal_8_7
+prep
+design -save gold
+muxpack
+opt
+#stat
+select -assert-count 0 t:$mux
+select -assert-count 1 t:$pmux
+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 read
+hierarchy -top mux_if_bal_8_2
+prep
+design -save gold
+muxpack
+opt
+#stat
+select -assert-count 7 t:$mux
+select -assert-count 0 t:$pmux
+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 read
+hierarchy -top mux_if_bal_5_1
+prep
+design -save gold
+muxpack
+opt
+#stat
+select -assert-count 4 t:$mux
+select -assert-count 0 t:$pmux
+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 read
+hierarchy -top cliffordwolf_nonexclusive_select
+prep
+design -save gold
+muxpack
+opt
+#stat
+select -assert-count 3 t:$mux
+select -assert-count 0 t:$pmux
+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 read
+#hierarchy -top cliffordwolf_freduce
+#prep
+#design -save gold
+#proc; opt; freduce; opt
+#show
+#muxpack
+#opt
+#stat
+#select -assert-count 0 t:$mux
+#select -assert-count 1 t:$pmux
+#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 read
+hierarchy -top case_nonexclusive_select
+prep
+design -save gold
+muxpack
+opt
+#stat
+select -assert-count 0 t:$mux
+select -assert-count 2 t:$pmux
+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 read
+hierarchy -top case_nonoverlap
+#prep # Do not prep otherwise $pmux's overlapping entry will get removed
+proc
+design -save gold
+opt -fast -mux_undef
+select -assert-count 2 t:$pmux
+muxpack
+opt
+#stat
+select -assert-count 0 t:$mux
+select -assert-count 1 t:$pmux
+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 read
+hierarchy -top case_overlap
+#prep # Do not prep otherwise $pmux's overlapping entry will get removed
+proc
+design -save gold
+opt -fast -mux_undef
+select -assert-count 2 t:$pmux
+muxpack
+opt
+#stat
+select -assert-count 0 t:$mux
+select -assert-count 2 t:$pmux
+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 read
+hierarchy -top case_overlap2
+#prep # Do not prep otherwise $pmux's overlapping entry will get removed
+proc
+design -save gold
+opt -fast -mux_undef
+select -assert-count 2 t:$pmux
+muxpack
+opt
+#stat
+select -assert-count 0 t:$mux
+select -assert-count 2 t:$pmux
+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
diff --git a/tests/various/opt_rmdff.v b/tests/various/opt_rmdff.v
deleted file mode 100644
index b1c06703c..000000000
--- a/tests/various/opt_rmdff.v
+++ /dev/null
@@ -1,50 +0,0 @@
-module opt_rmdff_test (input C, input D, input E, output [29:0] Q);
-\$dffe #(.WIDTH(1), .CLK_POLARITY(1), .EN_POLARITY(1)) remove0 (.CLK(C), .D(D), .EN(1'b0), .Q(Q[0])); // EN is never active
-(* init = "1'b1" *) wire Q1; assign Q[1] = Q1;
-\$dffe #(.WIDTH(1), .CLK_POLARITY(1), .EN_POLARITY(1)) remove1 (.CLK(C), .D(D), .EN(1'b0), .Q(Q1)); // EN is never active
-\$dffe #(.WIDTH(1), .CLK_POLARITY(1), .EN_POLARITY(1)) remove2 (.CLK(C), .D(D), .EN(1'bx), .Q(Q[2])); // EN is don't care
-\$dffe #(.WIDTH(1), .CLK_POLARITY(1), .EN_POLARITY(1)) keep3 (.CLK(C), .D(D), .EN(1'b1), .Q(Q[3])); // EN is always active
-(* init = "1'b0" *) wire Q4; assign Q[4] = Q4;
-\$dffe #(.WIDTH(1), .CLK_POLARITY(0), .EN_POLARITY(1)) keep4 (.CLK(C), .D(D), .EN(1'b1), .Q(Q4)); // EN is always active
-\$dffe #(.WIDTH(1), .CLK_POLARITY(1), .EN_POLARITY(0)) remove5 (.CLK(C), .D(D), .EN(1'b1), .Q(Q[5])); // EN is never active
-\$dffe #(.WIDTH(1), .CLK_POLARITY(1), .EN_POLARITY(0)) remove6 (.CLK(C), .D(D), .EN(1'bx), .Q(Q[6])); // EN is don't care
-(* init = "1'b0" *) wire Q7; assign Q[7] = Q7;
-\$dffe #(.WIDTH(1), .CLK_POLARITY(0), .EN_POLARITY(0)) keep7 (.CLK(C), .D(D), .EN(E), .Q(Q7)); // EN is non constant
-
-\$_DFFE_PP_ remove8 (.C(C), .D(D), .E(1'b0), .Q(Q[8])); // EN is never active
-(* init = "1'b1" *) wire Q9; assign Q[9] = Q9;
-\$_DFFE_PP_ remove9 (.C(C), .D(D), .E(1'b0), .Q(Q9)); // EN is never active
-\$_DFFE_PP_ remove10 (.C(C), .D(D), .E(1'bx), .Q(Q[10])); // EN is don't care
-\$_DFFE_PP_ keep11 (.C(C), .D(D), .E(1'b1), .Q(Q[11])); // EN is always active
-(* init = "1'b0" *) wire Q12; assign Q[12] = Q12;
-\$_DFFE_PP_ keep12 (.C(C), .D(D), .E(1'b1), .Q(Q12)); // EN is always active
-
-\$_DFFE_NN_ remove13 (.C(C), .D(D), .E(1'b1), .Q(Q[13])); // EN is never active
-(* init = "1'b1" *) wire Q14; assign Q[14] = Q14;
-\$_DFFE_NN_ remove14 (.C(C), .D(D), .E(1'b1), .Q(Q14)); // EN is never active
-\$_DFFE_NN_ remove15 (.C(C), .D(D), .E(1'bx), .Q(Q[15])); // EN is don't care
-\$_DFFE_NN_ keep16 (.C(C), .D(D), .E(1'b0), .Q(Q[16])); // EN is always active
-(* init = "1'b0" *) wire Q17; assign Q[17] = Q17;
-\$_DFFE_NN_ keep17 (.C(C), .D(D), .E(1'b0), .Q(Q17)); // EN is always active
-
-\$dffe #(.WIDTH(1), .CLK_POLARITY(1), .EN_POLARITY(1)) remove18 (.CLK(1'b0), .D(D), .EN(E), .Q(Q[18])); // CLK is constant
-(* init = "1'b1" *) wire Q19; assign Q[19] = Q19;
-\$dffe #(.WIDTH(1), .CLK_POLARITY(1), .EN_POLARITY(1)) remove19 (.CLK(1'b1), .D(D), .EN(E), .Q(Q19)); // CLK is constant
-\$dffe #(.WIDTH(1), .CLK_POLARITY(1), .EN_POLARITY(1)) remove20 (.CLK(C), .D(1'bx), .EN(E), .Q(Q[20])); // D is undriven, Q has no initial value
-(* init = "1'b0" *) wire Q21; assign Q[21] = Q21;
-\$dffe #(.WIDTH(1), .CLK_POLARITY(1), .EN_POLARITY(1)) keep21 (.CLK(C), .D(1'bx), .EN(E), .Q(Q21)); // D is undriven, Q has initial value
-//\$dffe #(.WIDTH(1), .CLK_POLARITY(0), .EN_POLARITY(1)) remove22 (.CLK(C), .D(1'b0), .EN(1'b1), .Q(Q[22])); // D is constant, no initial Q value, EN is always active
-// // (TODO, Q starts with 1'bx and becomes 1'b0)
-(* init = "1'b0" *) wire Q23; assign Q[23] = Q23;
-\$dffe #(.WIDTH(1), .CLK_POLARITY(1), .EN_POLARITY(1)) noenable23 (.CLK(C), .D(1'b0), .EN(1'b1), .Q(Q23)); // D is constant, initial Q value same as D, EN is always active
-(* init = "1'b1" *) wire Q24; assign Q[24] = Q24;
-\$dffe #(.WIDTH(1), .CLK_POLARITY(1), .EN_POLARITY(0)) keep24 (.CLK(C), .D(1'b0), .EN(1'b0), .Q(Q24)); // D is constant, initial Q value NOT same as D, EN is always active
-(* init = "1'b1" *) wire Q25; assign Q[25] = Q25;
-\$dffe #(.WIDTH(1), .CLK_POLARITY(1), .EN_POLARITY(0)) remove25 (.CLK(C), .D(1'b0), .EN(1'b1), .Q(Q25)); // D is constant, EN is never active
-\$dffe #(.WIDTH(1), .CLK_POLARITY(1), .EN_POLARITY(1)) remove26 (.CLK(C), .D(Q[26]), .EN(1'b1), .Q(Q[26])); // D is Q, EN is always active
-\$dffe #(.WIDTH(1), .CLK_POLARITY(1), .EN_POLARITY(0)) remove27 (.CLK(C), .D(Q[27]), .EN(1'b1), .Q(Q[27])); // D is Q, EN is never active, but no initial value
-\$dffe #(.WIDTH(1), .CLK_POLARITY(1), .EN_POLARITY(0)) remove28 (.CLK(C), .D(Q[28]), .EN(E), .Q(Q[28])); // EN is nonconst, but no initial value
-(* init = "1'b1" *) wire Q29; assign Q[29] = Q29;
-\$dffe #(.WIDTH(1), .CLK_POLARITY(1), .EN_POLARITY(1)) keep29 (.CLK(C), .D(Q[29]), .EN(1'b1), .Q(Q29)); // EN is always active, but with initial value
-
-endmodule
diff --git a/tests/various/opt_rmdff.ys b/tests/various/opt_rmdff.ys
deleted file mode 100644
index 081f81782..000000000
--- a/tests/various/opt_rmdff.ys
+++ /dev/null
@@ -1,26 +0,0 @@
-read_verilog -icells opt_rmdff.v
-prep
-design -stash gold
-read_verilog -icells opt_rmdff.v
-proc
-opt_rmdff
-
-select -assert-count 0 c:remove*
-select -assert-min 7 c:keep*
-select -assert-count 0 t:$dffe 7:$_DFFE_* %u c:noenable* %i
-
-design -stash gate
-
-design -import gold -as gold
-design -import gate -as gate
-
-equiv_make gold gate equiv
-hierarchy -top equiv
-equiv_simple -undef
-equiv_status -assert
-
-design -load gold
-stat
-
-design -load gate
-stat
diff --git a/tests/various/pmgen_reduce.ys b/tests/various/pmgen_reduce.ys
new file mode 100644
index 000000000..c214d3f25
--- /dev/null
+++ b/tests/various/pmgen_reduce.ys
@@ -0,0 +1,21 @@
+test_pmgen -generate reduce
+hierarchy -top pmtest_test_pmgen_pm_reduce
+flatten; opt_clean
+
+design -save gold
+test_pmgen -reduce_chain
+design -stash gate
+
+design -copy-from gold -as gold pmtest_test_pmgen_pm_reduce
+design -copy-from gate -as gate pmtest_test_pmgen_pm_reduce
+miter -equiv -flatten -make_assert gold gate miter
+sat -verify -prove-asserts miter
+
+design -load gold
+test_pmgen -reduce_tree
+design -stash gate
+
+design -copy-from gold -as gold pmtest_test_pmgen_pm_reduce
+design -copy-from gate -as gate pmtest_test_pmgen_pm_reduce
+miter -equiv -flatten -make_assert gold gate miter
+sat -verify -prove-asserts miter
diff --git a/tests/various/pmux2shiftx.v b/tests/various/pmux2shiftx.v
index fec84187b..563394080 100644
--- a/tests/various/pmux2shiftx.v
+++ b/tests/various/pmux2shiftx.v
@@ -32,3 +32,13 @@ module pmux2shiftx_test (
endcase
end
endmodule
+
+module issue01135(input [7:0] i, output o);
+always @*
+case (i[6:3])
+ 4: o <= i[0];
+ 3: o <= i[2];
+ 7: o <= i[3];
+ default: o <= 1'b0;
+endcase
+endmodule
diff --git a/tests/various/pmux2shiftx.ys b/tests/various/pmux2shiftx.ys
index deb134083..51ee2f7be 100644
--- a/tests/various/pmux2shiftx.ys
+++ b/tests/various/pmux2shiftx.ys
@@ -1,4 +1,7 @@
read_verilog pmux2shiftx.v
+design -save read
+
+hierarchy -top pmux2shiftx_test
prep
design -save gold
@@ -21,8 +24,16 @@ 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
-stat
-
-design -load gate
-stat
+#design -load gold
+#stat
+#
+#design -load gate
+#stat
+
+design -load read
+hierarchy -top issue01135
+proc
+pmux2shiftx -norange
+opt -full
+select -assert-count 0 t:$shift*
+select -assert-count 1 t:$pmux
diff --git a/tests/various/run-test.sh b/tests/various/run-test.sh
index d49553ede..ea56b70f0 100755
--- a/tests/various/run-test.sh
+++ b/tests/various/run-test.sh
@@ -1,14 +1,20 @@
#!/usr/bin/env bash
set -e
+{
+echo "all::"
for x in *.ys; do
- echo "Running $x.."
- ../../yosys -ql ${x%.ys}.log $x
+ echo "all:: run-$x"
+ echo "run-$x:"
+ echo " @echo 'Running $x..'"
+ echo " @../../yosys -ql ${x%.ys}.log $x"
done
-# Run any .sh files in this directory (with the exception of the file - run-test.sh
-shell_tests=$(echo *.sh | sed -e 's/run-test.sh//')
-if [ "$shell_tests" ]; then
- for s in $shell_tests; do
- echo "Running $s.."
- bash $s
- done
-fi
+for s in *.sh; do
+ if [ "$s" != "run-test.sh" ]; then
+ echo "all:: run-$s"
+ echo "run-$s:"
+ echo " @echo 'Running $s..'"
+ echo " @bash $s"
+ fi
+done
+} > run-test.mk
+exec ${MAKE:-make} -f run-test.mk
diff --git a/tests/various/script.ys b/tests/various/script.ys
new file mode 100644
index 000000000..66b7b5caa
--- /dev/null
+++ b/tests/various/script.ys
@@ -0,0 +1,20 @@
+read_verilog -formal <<EOT
+ module top;
+ foo bar();
+ foo asdf();
+ winnie the_pooh();
+
+ wire [1023:0] _RUNME0 = "select -assert-count 2 t:foo";
+ wire [1023:0] _RUNME1 = "select -assert-count 1 t:winnie";
+ endmodule
+
+ module other;
+ wire [1023:0] _DELETE = "cd; delete c:bar";
+ endmodule
+EOT
+
+script -scriptwire w:_RUNME*
+
+select w:_DELETE
+script -scriptwire
+select -assert-count 1 t:foo
diff --git a/tests/various/shregmap.v b/tests/various/shregmap.v
new file mode 100644
index 000000000..604c2c976
--- /dev/null
+++ b/tests/various/shregmap.v
@@ -0,0 +1,48 @@
+module shregmap_static_test(input i, clk, output [1:0] q);
+reg head = 1'b0;
+reg [3:0] shift1 = 4'b0000;
+reg [3:0] shift2 = 4'b0000;
+
+always @(posedge clk) begin
+ head <= i;
+ shift1 <= {shift1[2:0], head};
+ shift2 <= {shift2[2:0], head};
+end
+
+assign q = {shift2[3], shift1[3]};
+endmodule
+
+module $__SHREG_DFF_P_(input C, D, output Q);
+parameter DEPTH = 1;
+parameter [DEPTH-1:0] INIT = {DEPTH{1'b0}};
+reg [DEPTH-1:0] r = INIT;
+always @(posedge C)
+ r <= { r[DEPTH-2:0], D };
+assign Q = r[DEPTH-1];
+endmodule
+
+module shregmap_variable_test(input i, clk, input [1:0] l1, l2, output [1:0] q);
+reg head = 1'b0;
+reg [3:0] shift1 = 4'b0000;
+reg [3:0] shift2 = 4'b0000;
+
+always @(posedge clk) begin
+ head <= i;
+ shift1 <= {shift1[2:0], head};
+ shift2 <= {shift2[2:0], head};
+end
+
+assign q = {shift2[l2], shift1[l1]};
+endmodule
+
+module $__XILINX_SHREG_(input C, D, input [1:0] L, output Q);
+parameter CLKPOL = 1;
+parameter ENPOL = 1;
+parameter DEPTH = 1;
+parameter [DEPTH-1:0] INIT = {DEPTH{1'b0}};
+reg [DEPTH-1:0] r = INIT;
+wire clk = C ^ CLKPOL;
+always @(posedge C)
+ r <= { r[DEPTH-2:0], D };
+assign Q = r[L];
+endmodule
diff --git a/tests/various/shregmap.ys b/tests/various/shregmap.ys
new file mode 100644
index 000000000..0e5fe882b
--- /dev/null
+++ b/tests/various/shregmap.ys
@@ -0,0 +1,66 @@
+read_verilog shregmap.v
+design -save read
+
+design -copy-to model $__SHREG_DFF_P_
+hierarchy -top shregmap_static_test
+prep
+design -save gold
+
+techmap
+shregmap -init
+
+opt
+
+# stat
+# show -width
+select -assert-count 1 t:$_DFF_P_
+select -assert-count 2 t:$__SHREG_DFF_P_
+
+design -stash gate
+
+design -import gold -as gold
+design -import gate -as gate
+design -copy-from model -as $__SHREG_DFF_P_ \$__SHREG_DFF_P_
+prep
+
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -verify -prove-asserts -show-ports -seq 5 miter
+
+#design -load gold
+#stat
+
+#design -load gate
+#stat
+
+##########
+
+design -load read
+design -copy-to model $__XILINX_SHREG_
+hierarchy -top shregmap_variable_test
+prep
+design -save gold
+
+simplemap t:$dff t:$dffe
+shregmap -tech xilinx
+
+#stat
+# show -width
+# write_verilog -noexpr -norename
+select -assert-count 1 t:$_DFF_P_
+select -assert-count 2 t:$__XILINX_SHREG_
+
+design -stash gate
+
+design -import gold -as gold
+design -import gate -as gate
+design -copy-from model -as $__XILINX_SHREG_ \$__XILINX_SHREG_
+prep
+
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -verify -prove-asserts -show-ports -seq 5 miter
+
+# design -load gold
+# stat
+
+# design -load gate
+# stat
diff --git a/tests/various/signext.ys b/tests/various/signext.ys
new file mode 100644
index 000000000..0c8d671e7
--- /dev/null
+++ b/tests/various/signext.ys
@@ -0,0 +1,33 @@
+
+read_verilog -formal <<EOT
+module gate(input clk, output [32:0] o, p, q, r, s, t, u);
+assign o = 'bx;
+assign p = 1'bx;
+assign q = 'bz;
+assign r = 1'bz;
+assign s = 1'b0;
+assign t = 'b1;
+assign u = -'sb1;
+endmodule
+EOT
+
+proc
+
+## Equivalence checking
+
+read_verilog -formal <<EOT
+module gold(input clk, output [32:0] o, p, q, r, s, t, u);
+assign o = {33{1'bx}};
+assign p = {{32{1'b0}}, 1'bx};
+assign q = {33{1'bz}};
+assign r = {{32{1'b0}}, 1'bz};
+assign s = {33{1'b0}};
+assign t = {{32{1'b0}}, 1'b1};
+assign u = {33{1'b1}};
+endmodule
+EOT
+
+proc
+
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -verify -prove-asserts -show-ports -enable_undef miter
diff --git a/tests/various/specify.v b/tests/various/specify.v
index afc421da8..5d44d78f7 100644
--- a/tests/various/specify.v
+++ b/tests/various/specify.v
@@ -7,9 +7,11 @@ module test (
if (EN) Q <= D;
specify
- if (EN) (CLK *> (Q : D)) = (1, 2:3:4);
+`ifndef SKIP_UNSUPPORTED_IGN_PARSER_CONSTRUCTS
+ if (EN) (posedge CLK *> (Q : D)) = (1, 2:3:4);
$setup(D, posedge CLK &&& EN, 5);
$hold(posedge CLK, D &&& EN, 6);
+`endif
endspecify
endmodule
@@ -28,3 +30,10 @@ module test2 (
(B => Q) = 1.5;
endspecify
endmodule
+
+module issue01144(input clk, d, output q);
+specify
+ (posedge clk => (q +: d)) = (3,1);
+ (posedge clk *> (q +: d)) = (3,1);
+endspecify
+endmodule
diff --git a/tests/various/specify.ys b/tests/various/specify.ys
index a5ca07219..00597e1e2 100644
--- a/tests/various/specify.ys
+++ b/tests/various/specify.ys
@@ -54,3 +54,5 @@ equiv_struct
equiv_induct -seq 5
equiv_status -assert
design -reset
+
+read_verilog -DSKIP_UNSUPPORTED_IGN_PARSER_CONSTRUCTS specify.v
diff --git a/tests/various/wreduce.ys b/tests/various/wreduce.ys
new file mode 100644
index 000000000..2e0812c48
--- /dev/null
+++ b/tests/various/wreduce.ys
@@ -0,0 +1,79 @@
+read_verilog <<EOT
+module wreduce_sub_test(input [3:0] i, input [7:0] j, output [8:0] o);
+ assign o = (j >> 4) - i;
+endmodule
+EOT
+
+hierarchy -auto-top
+proc
+design -save gold
+
+opt_expr
+wreduce
+
+select -assert-count 1 t:$sub r:A_WIDTH=4 r:B_WIDTH=4 r:Y_WIDTH=5 %i %i %i
+
+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
+
+##########
+
+read_verilog <<EOT
+module wreduce_sub_signed_test(input signed [3:0] i, input signed [7:0] j, output signed [8:0] o);
+ assign o = (j >>> 4) - i;
+endmodule
+EOT
+
+hierarchy -auto-top
+proc
+design -save gold
+
+opt_expr
+wreduce
+
+select -assert-count 1 t:$sub r:A_WIDTH=4 r:B_WIDTH=4 r:Y_WIDTH=5 %i %i %i
+
+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
+
+##########
+
+# Testcase from: https://github.com/YosysHQ/yosys/commit/25680f6a078bb32f157bd580705656496717bafb
+design -reset
+read_verilog <<EOT
+module top(
+ input clk,
+ input rst,
+ input [2:0] a,
+ output [1:0] b
+);
+ reg [2:0] b_reg;
+ initial begin
+ b_reg <= 3'b0;
+ end
+
+ assign b = b_reg[1:0];
+ always @(posedge clk or posedge rst) begin
+ if(rst) begin
+ b_reg <= 3'b0;
+ end else begin
+ b_reg <= a;
+ end
+ end
+endmodule
+EOT
+
+proc
+wreduce
+
+select -assert-count 1 t:$adff r:ARST_VALUE=2'b00 %i
diff --git a/tests/various/write_gzip.ys b/tests/various/write_gzip.ys
new file mode 100644
index 000000000..524ecc33e
--- /dev/null
+++ b/tests/various/write_gzip.ys
@@ -0,0 +1,16 @@
+read_verilog <<EOT
+module top(input a, output y);
+assign y = !a;
+endmodule
+EOT
+
+prep -top top
+write_verilog write_gzip.v.gz
+design -reset
+
+! rm -f write_gzip.v
+! gunzip write_gzip.v.gz
+read_verilog write_gzip.v
+! rm -f write_gzip.v
+hierarchy -top top
+select -assert-any top
generated by cgit v1.2.3 (git 2.25.1) at 2025-05-29 11:22:23 +0000