aboutsummaryrefslogtreecommitdiffstats
path: root/tests
diff options
context:
space:
mode:
Diffstat (limited to 'tests')
-rw-r--r--tests/aiger/.gitignore3
-rwxr-xr-xtests/aiger/run-test.sh10
-rw-r--r--tests/simple/arrays02.sv16
-rw-r--r--tests/simple/defvalue.sv22
-rw-r--r--tests/simple/generate.v11
-rw-r--r--tests/simple_abc9/abc.box2
-rw-r--r--tests/simple_abc9/abc9.v269
-rwxr-xr-xtests/simple_abc9/run-test.sh22
-rwxr-xr-xtests/tools/autotest.sh29
-rw-r--r--tests/various/.gitignore3
-rw-r--r--tests/various/muxcover.ys141
-rw-r--r--tests/various/signext.ys33
12 files changed, 539 insertions, 22 deletions
diff --git a/tests/aiger/.gitignore b/tests/aiger/.gitignore
index 073f46157..9a26bb8f4 100644
--- a/tests/aiger/.gitignore
+++ b/tests/aiger/.gitignore
@@ -1,2 +1 @@
-*.log
-*.out
+/*_ref.v
diff --git a/tests/aiger/run-test.sh b/tests/aiger/run-test.sh
index f52eb4ac1..5246c1b48 100755
--- a/tests/aiger/run-test.sh
+++ b/tests/aiger/run-test.sh
@@ -10,8 +10,9 @@ for aag in *.aag; do
# Since ABC cannot read *.aag, read the *.aig instead
# (which would have been created by the reference aig2aig utility,
# available from http://fmv.jku.at/aiger/)
- ../../yosys-abc -c "read -c ${aag%.*}.aig; write ${aag%.*}_ref.v"
- ../../yosys -p "
+ echo "Checking $aag."
+ ../../yosys-abc -q "read -c ${aag%.*}.aig; write ${aag%.*}_ref.v"
+ ../../yosys -qp "
read_verilog ${aag%.*}_ref.v
prep
design -stash gold
@@ -26,8 +27,9 @@ sat -verify -prove-asserts -show-ports -seq 16 miter
done
for aig in *.aig; do
- ../../yosys-abc -c "read -c $aig; write ${aig%.*}_ref.v"
- ../../yosys -p "
+ echo "Checking $aig."
+ ../../yosys-abc -q "read -c $aig; write ${aig%.*}_ref.v"
+ ../../yosys -qp "
read_verilog ${aig%.*}_ref.v
prep
design -stash gold
diff --git a/tests/simple/arrays02.sv b/tests/simple/arrays02.sv
new file mode 100644
index 000000000..76c2a7388
--- /dev/null
+++ b/tests/simple/arrays02.sv
@@ -0,0 +1,16 @@
+module uut_arrays02(clock, we, addr, wr_data, rd_data);
+
+input clock, we;
+input [3:0] addr, wr_data;
+output [3:0] rd_data;
+reg [3:0] rd_data;
+
+reg [3:0] memory [16];
+
+always @(posedge clock) begin
+ if (we)
+ memory[addr] <= wr_data;
+ rd_data <= memory[addr];
+end
+
+endmodule
diff --git a/tests/simple/defvalue.sv b/tests/simple/defvalue.sv
new file mode 100644
index 000000000..b0a087ecb
--- /dev/null
+++ b/tests/simple/defvalue.sv
@@ -0,0 +1,22 @@
+module top(input clock, input [3:0] delta, output [3:0] cnt1, cnt2);
+ cnt #(1) foo (.clock, .cnt(cnt1), .delta);
+ cnt #(2) bar (.clock, .cnt(cnt2));
+endmodule
+
+module cnt #(
+ parameter integer initval = 0
+) (
+ input clock,
+ output logic [3:0] cnt = initval,
+`ifdef __ICARUS__
+ input [3:0] delta
+`else
+ input [3:0] delta = 10
+`endif
+);
+`ifdef __ICARUS__
+ assign (weak0, weak1) delta = 10;
+`endif
+ always @(posedge clock)
+ cnt <= cnt + delta;
+endmodule
diff --git a/tests/simple/generate.v b/tests/simple/generate.v
index 3c55682cb..0e353ad9b 100644
--- a/tests/simple/generate.v
+++ b/tests/simple/generate.v
@@ -148,3 +148,14 @@ generate
endgenerate
assign out = steps[WIDTH].outer[0].val;
endmodule
+
+// ------------------------------------------
+
+module gen_test6(output [3:0] o);
+generate
+ genvar i;
+ for (i = 3; i >= 0; i = i-1) begin
+ assign o[i] = 1'b0;
+ end
+endgenerate
+endmodule
diff --git a/tests/simple_abc9/abc.box b/tests/simple_abc9/abc.box
new file mode 100644
index 000000000..a8801d807
--- /dev/null
+++ b/tests/simple_abc9/abc.box
@@ -0,0 +1,2 @@
+MUXF8 1 0 3 1
+1 1 1
diff --git a/tests/simple_abc9/abc9.v b/tests/simple_abc9/abc9.v
new file mode 100644
index 000000000..64b625efe
--- /dev/null
+++ b/tests/simple_abc9/abc9.v
@@ -0,0 +1,269 @@
+module abc9_test001(input a, output o);
+assign o = a;
+endmodule
+
+module abc9_test002(input [1:0] a, output o);
+assign o = a[1];
+endmodule
+
+module abc9_test003(input [1:0] a, output [1:0] o);
+assign o = a;
+endmodule
+
+module abc9_test004(input [1:0] a, output o);
+assign o = ^a;
+endmodule
+
+module abc9_test005(input [1:0] a, output o, output p);
+assign o = ^a;
+assign p = ~o;
+endmodule
+
+module abc9_test006(input [1:0] a, output [2:0] o);
+assign o[0] = ^a;
+assign o[1] = ~o[0];
+assign o[2] = o[1];
+endmodule
+
+module abc9_test007(input a, output o);
+wire b, c;
+assign c = ~a;
+assign b = c;
+abc9_test007_sub s(b, o);
+endmodule
+
+module abc9_test007_sub(input a, output b);
+assign b = a;
+endmodule
+
+module abc9_test008(input a, output o);
+wire b, c;
+assign b = ~a;
+assign c = b;
+abc9_test008_sub s(b, o);
+endmodule
+
+module abc9_test008_sub(input a, output b);
+assign b = ~a;
+endmodule
+
+module abc9_test009(inout io, input oe);
+reg latch;
+always @(io or oe)
+ if (!oe)
+ latch <= io;
+assign io = oe ? ~latch : 1'bz;
+endmodule
+
+module abc9_test010(inout [7:0] io, input oe);
+reg [7:0] latch;
+always @(io or oe)
+ if (!oe)
+ latch <= io;
+assign io = oe ? ~latch : 8'bz;
+endmodule
+
+module abc9_test011(inout io, input oe);
+reg latch;
+always @(io or oe)
+ if (!oe)
+ latch <= io;
+//assign io = oe ? ~latch : 8'bz;
+endmodule
+
+module abc9_test012(inout io, input oe);
+reg latch;
+//always @(io or oe)
+// if (!oe)
+// latch <= io;
+assign io = oe ? ~latch : 8'bz;
+endmodule
+
+module abc9_test013(inout [3:0] io, input oe);
+reg [3:0] latch;
+always @(io or oe)
+ if (!oe)
+ latch[3:0] <= io[3:0];
+ else
+ latch[7:4] <= io;
+assign io[3:0] = oe ? ~latch[3:0] : 4'bz;
+assign io[7:4] = !oe ? {latch[4], latch[7:3]} : 4'bz;
+endmodule
+
+module abc9_test014(inout [7:0] io, input oe);
+abc9_test012_sub sub(io, oe);
+endmodule
+
+module abc9_test012_sub(inout [7:0] io, input oe);
+reg [7:0] latch;
+always @(io or oe)
+ if (!oe)
+ latch[3:0] <= io;
+ else
+ latch[7:4] <= io;
+assign io[3:0] = oe ? ~latch[3:0] : 4'bz;
+assign io[7:4] = !oe ? {latch[4], latch[7:3]} : 4'bz;
+endmodule
+
+module abc9_test015(input a, output b, input c);
+assign b = ~a;
+(* keep *) wire d;
+assign d = ~c;
+endmodule
+
+module abc9_test016(input a, output b);
+assign b = ~a;
+(* keep *) reg c;
+always @* c <= ~a;
+endmodule
+
+module abc9_test017(input a, output b);
+assign b = ~a;
+(* keep *) reg c;
+always @* c = b;
+endmodule
+
+module abc9_test018(input a, output b, output c);
+assign b = ~a;
+(* keep *) wire [1:0] d;
+assign c = &d;
+endmodule
+
+module abc9_test019(input a, output b);
+assign b = ~a;
+(* keep *) reg [1:0] c;
+reg d;
+always @* d <= &c;
+endmodule
+
+module abc9_test020(input a, output b);
+assign b = ~a;
+(* keep *) reg [1:0] c;
+(* keep *) reg d;
+always @* d <= &c;
+endmodule
+
+// Citation: https://github.com/alexforencich/verilog-ethernet
+module abc9_test021(clk, rst, s_eth_hdr_valid, s_eth_hdr_ready, s_eth_dest_mac, s_eth_src_mac, s_eth_type, s_eth_payload_axis_tdata, s_eth_payload_axis_tkeep, s_eth_payload_axis_tvalid, s_eth_payload_axis_tready, s_eth_payload_axis_tlast, s_eth_payload_axis_tid, s_eth_payload_axis_tdest, s_eth_payload_axis_tuser, m_eth_hdr_valid, m_eth_hdr_ready, m_eth_dest_mac, m_eth_src_mac, m_eth_type, m_eth_payload_axis_tdata, m_eth_payload_axis_tkeep, m_eth_payload_axis_tvalid, m_eth_payload_axis_tready, m_eth_payload_axis_tlast, m_eth_payload_axis_tid, m_eth_payload_axis_tdest, m_eth_payload_axis_tuser);
+ input clk;
+ output [47:0] m_eth_dest_mac;
+ input m_eth_hdr_ready;
+ output m_eth_hdr_valid;
+ output [7:0] m_eth_payload_axis_tdata;
+ output [7:0] m_eth_payload_axis_tdest;
+ output [7:0] m_eth_payload_axis_tid;
+ output m_eth_payload_axis_tkeep;
+ output m_eth_payload_axis_tlast;
+ input m_eth_payload_axis_tready;
+ output m_eth_payload_axis_tuser;
+ output m_eth_payload_axis_tvalid;
+ output [47:0] m_eth_src_mac;
+ output [15:0] m_eth_type;
+ input rst;
+ input [191:0] s_eth_dest_mac;
+ output [3:0] s_eth_hdr_ready;
+ input [3:0] s_eth_hdr_valid;
+ input [31:0] s_eth_payload_axis_tdata;
+ input [31:0] s_eth_payload_axis_tdest;
+ input [31:0] s_eth_payload_axis_tid;
+ input [3:0] s_eth_payload_axis_tkeep;
+ input [3:0] s_eth_payload_axis_tlast;
+ output [3:0] s_eth_payload_axis_tready;
+ input [3:0] s_eth_payload_axis_tuser;
+ input [3:0] s_eth_payload_axis_tvalid;
+ input [191:0] s_eth_src_mac;
+ input [63:0] s_eth_type;
+ (* keep *)
+ wire [0:0] grant, request;
+ wire a;
+ not u0 (
+ a,
+ grant[0]
+ );
+ and u1 (
+ request[0],
+ s_eth_hdr_valid[0],
+ a
+ );
+ (* keep *)
+ MUXF8 u2 (
+ .I0(1'bx),
+ .I1(1'bx),
+ .O(o),
+ .S(1'bx)
+ );
+ arbiter arb_inst (
+ .acknowledge(acknowledge),
+ .clk(clk),
+ .grant(grant),
+ .grant_encoded(grant_encoded),
+ .grant_valid(grant_valid),
+ .request(request),
+ .rst(rst)
+ );
+endmodule
+
+module arbiter (clk, rst, request, acknowledge, grant, grant_valid, grant_encoded);
+ input [3:0] acknowledge;
+ input clk;
+ output [3:0] grant;
+ output [1:0] grant_encoded;
+ output grant_valid;
+ input [3:0] request;
+ input rst;
+endmodule
+
+(* abc_box_id=1 *)
+module MUXF8(input I0, I1, S, output O);
+endmodule
+
+// Citation: https://github.com/alexforencich/verilog-ethernet
+// TODO: yosys -p "synth_xilinx -abc9 -top abc9_test022" abc9.v -q
+// returns before b4321a31
+// Warning: Wire abc9_test022.\m_eth_payload_axis_tkeep [7] is used but has no
+// driver.
+// Warning: Wire abc9_test022.\m_eth_payload_axis_tkeep [3] is used but has no
+// driver.
+module abc9_test022
+(
+ input wire clk,
+ input wire i,
+ output wire [7:0] m_eth_payload_axis_tkeep
+);
+ reg [7:0] m_eth_payload_axis_tkeep_reg = 8'd0;
+ assign m_eth_payload_axis_tkeep = m_eth_payload_axis_tkeep_reg;
+ always @(posedge clk)
+ m_eth_payload_axis_tkeep_reg <= i ? 8'hff : 8'h0f;
+endmodule
+
+// Citation: https://github.com/riscv/riscv-bitmanip
+// TODO: yosys -p "synth_xilinx -abc9 -top abc9_test023" abc9.v -q
+// returns before 14233843
+// Warning: Wire abc9_test023.\dout [1] is used but has no driver.
+module abc9_test023 #(
+ parameter integer N = 2,
+ parameter integer M = 2
+) (
+ input [7:0] din,
+ output [M-1:0] dout
+);
+ wire [2*M-1:0] mask = {M{1'b1}};
+ assign dout = (mask << din[N-1:0]) >> M;
+endmodule
+
+module abc9_test024(input [3:0] i, output [3:0] o);
+abc9_test024_sub a(i[1:0], o[1:0]);
+endmodule
+
+module abc9_test024_sub(input [1:0] i, output [1:0] o);
+assign o = i;
+endmodule
+
+module abc9_test025(input [3:0] i, output [3:0] o);
+abc9_test024_sub a(i[2:1], o[2:1]);
+endmodule
+
+module abc9_test026(output [3:0] o, p);
+assign o = { 1'b1, 1'bx };
+assign p = { 1'b1, 1'bx, 1'b0 };
+endmodule
diff --git a/tests/simple_abc9/run-test.sh b/tests/simple_abc9/run-test.sh
new file mode 100755
index 000000000..4935d41ad
--- /dev/null
+++ b/tests/simple_abc9/run-test.sh
@@ -0,0 +1,22 @@
+#!/bin/bash
+
+OPTIND=1
+seed="" # default to no seed specified
+while getopts "S:" opt
+do
+ case "$opt" in
+ S) arg="${OPTARG#"${OPTARG%%[![:space:]]*}"}" # remove leading space
+ seed="SEED=$arg" ;;
+ esac
+done
+shift "$((OPTIND-1))"
+
+# check for Icarus Verilog
+if ! which iverilog > /dev/null ; then
+ echo "$0: Error: Icarus Verilog 'iverilog' not found."
+ exit 1
+fi
+
+cp ../simple/*.v .
+DOLLAR='?'
+exec ${MAKE:-make} -f ../tools/autotest.mk $seed *.v EXTRA_FLAGS="-p 'hierarchy; synth -run coarse; opt -full; techmap; abc9 -lut 4 -box ../abc.box; stat; check -assert; select -assert-none t:${DOLLAR}_NOT_ t:${DOLLAR}_AND_ %%'"
diff --git a/tests/tools/autotest.sh b/tests/tools/autotest.sh
index 23964a751..96d9cdda9 100755
--- a/tests/tools/autotest.sh
+++ b/tests/tools/autotest.sh
@@ -89,8 +89,7 @@ done
compile_and_run() {
exe="$1"; output="$2"; shift 2
- ext=${1##*.}
- if [ "$ext" == "sv" ]; then
+ if [ "${2##*.}" == "sv" ]; then
language_gen="-g2012"
else
language_gen="-g2005"
@@ -142,23 +141,25 @@ do
cd ${bn}.out
fn=$(basename $fn)
bn=$(basename $bn)
+ refext=v
rm -f ${bn}_ref.fir
if [[ "$ext" == "v" ]]; then
egrep -v '^\s*`timescale' ../$fn > ${bn}_ref.${ext}
elif [[ "$ext" == "aig" ]] || [[ "$ext" == "aag" ]]; then
- "$toolsdir"/../../yosys-abc -c "read_aiger ../${fn}; write ${bn}_ref.v"
+ "$toolsdir"/../../yosys-abc -c "read_aiger ../${fn}; write ${bn}_ref.${refext}"
else
- cp ../${fn} ${bn}_ref.${ext}
+ refext=$ext
+ cp ../${fn} ${bn}_ref.${refext}
fi
if [ ! -f ../${bn}_tb.v ]; then
- "$toolsdir"/../../yosys -f "$frontend $include_opts" -b "test_autotb $autotb_opts" -o ${bn}_tb.v ${bn}_ref.v
+ "$toolsdir"/../../yosys -f "$frontend $include_opts" -b "test_autotb $autotb_opts" -o ${bn}_tb.v ${bn}_ref.${refext}
else
cp ../${bn}_tb.v ${bn}_tb.v
fi
if $genvcd; then sed -i 's,// \$dump,$dump,g' ${bn}_tb.v; fi
- compile_and_run ${bn}_tb_ref ${bn}_out_ref ${bn}_tb.v ${bn}_ref.v $libs \
+ compile_and_run ${bn}_tb_ref ${bn}_out_ref ${bn}_tb.v ${bn}_ref.${refext} $libs \
"$toolsdir"/../../techlibs/common/simlib.v \
"$toolsdir"/../../techlibs/common/simcells.v
if $genvcd; then mv testbench.vcd ${bn}_ref.vcd; fi
@@ -175,25 +176,25 @@ do
test_count=$(( test_count + 1 ))
}
- if [ "$frontend" = "verific" -o "$frontend" = "verific_gates" ] && grep -q VERIFIC-SKIP ${bn}_ref.v; then
+ if [ "$frontend" = "verific" -o "$frontend" = "verific_gates" ] && grep -q VERIFIC-SKIP ${bn}_ref.${refext}; then
touch ../${bn}.skip
return
fi
if [ -n "$scriptfiles" ]; then
- test_passes -f "$frontend $include_opts" ${bn}_ref.v $scriptfiles
+ test_passes -f "$frontend $include_opts" ${bn}_ref.${refext} $scriptfiles
elif [ -n "$scriptopt" ]; then
- test_passes -f "$frontend $include_opts" -p "$scriptopt" ${bn}_ref.v
+ test_passes -f "$frontend $include_opts" -p "$scriptopt" ${bn}_ref.${refext}
elif [ "$frontend" = "verific" ]; then
- test_passes -p "verific -vlog2k ${bn}_ref.v; verific -import -all; opt; memory;;"
+ test_passes -p "verific -vlog2k ${bn}_ref.${refext}; verific -import -all; opt; memory;;"
elif [ "$frontend" = "verific_gates" ]; then
- test_passes -p "verific -vlog2k ${bn}_ref.v; verific -import -gates -all; opt; memory;;"
+ test_passes -p "verific -vlog2k ${bn}_ref.${refext}; verific -import -gates -all; opt; memory;;"
else
- test_passes -f "$frontend $include_opts" -p "hierarchy; proc; opt; memory; opt; fsm; opt -full -fine" ${bn}_ref.v
- test_passes -f "$frontend $include_opts" -p "hierarchy; synth -run coarse; techmap; opt; abc -dff" ${bn}_ref.v
+ test_passes -f "$frontend $include_opts" -p "hierarchy; proc; opt; memory; opt; fsm; opt -full -fine" ${bn}_ref.${refext}
+ test_passes -f "$frontend $include_opts" -p "hierarchy; synth -run coarse; techmap; opt; abc -dff" ${bn}_ref.${refext}
if [ -n "$firrtl2verilog" ]; then
if test -z "$xfirrtl" || ! grep "$fn" "$xfirrtl" ; then
- "$toolsdir"/../../yosys -b "firrtl" -o ${bn}_ref.fir -f "$frontend $include_opts" -p "prep -nordff; proc; opt; memory; opt; fsm; opt -full -fine; pmuxtree" ${bn}_ref.v
+ "$toolsdir"/../../yosys -b "firrtl" -o ${bn}_ref.fir -f "$frontend $include_opts" -p "prep -nordff; proc; opt; memory; opt; fsm; opt -full -fine; pmuxtree" ${bn}_ref.${refext}
$firrtl2verilog -i ${bn}_ref.fir -o ${bn}_ref.fir.v
test_passes -f "$frontend $include_opts" -p "hierarchy; proc; opt; memory; opt; fsm; opt -full -fine" ${bn}_ref.fir.v
fi
diff --git a/tests/various/.gitignore b/tests/various/.gitignore
index 397b4a762..7b3e8c68e 100644
--- a/tests/various/.gitignore
+++ b/tests/various/.gitignore
@@ -1 +1,2 @@
-*.log
+/*.log
+/*.out
diff --git a/tests/various/muxcover.ys b/tests/various/muxcover.ys
index 7ac460f13..8ef619b46 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,142 @@ 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
+
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
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-26 08:42:12 +0000