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_5_3_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
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 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_5_3_missing
+prep
+design -save gold
+muxpack
+opt
+stat
+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