read_verilog -formal <<EOT module gate (input [2:0] A, B, C, D, X, output reg [2:0] Y); always @* (* parallel_case *) casez (X) 3'b??1: Y = A; 3'b?1?: Y = B; 3'b1??: Y = C; 3'b000: Y = D; endcase endmodule EOT ## Examle usage for "pmuxtree" and "muxcover" proc pmuxtree techmap muxcover -mux4 splitnets -ports clean # show ## Equivalence checking read_verilog -formal <<EOT module gold (input [2:0] A, B, C, D, X, output reg [2:0] Y); always @* casez (X) 3'b001: Y = A; 3'b010: Y = B; 3'b100: Y = C; 3'b000: Y = D; default: Y = 'bx; endcase endmodule EOT proc splitnets -ports techmap -map +/simcells.v t:$_MUX4_ equiv_make gold gate equiv hierarchy -top equiv equiv_simple -undef equiv_status -assert