2 read_verilog -formal <<EOT
3 module gate (input [2:0] A, B, C, D, X, output reg [2:0] Y);
16 ## Example usage for "pmuxtree" and "muxcover"
28 ## Equivalence checking
30 read_verilog -formal <<EOT
31 module gold (input [2:0] A, B, C, D, X, output reg [2:0] Y);
45 techmap -map +/simcells.v t:$_MUX4_
47 equiv_make gold gate equiv
52 ## Partial matching MUX4
55 read_verilog -formal <<EOT
56 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);
75 select -assert-count 0 t:$_MUX_
76 select -assert-count 1 t:$_MUX4_
77 select -assert-count 0 t:$_MUX8_
78 select -assert-count 0 t:$_MUX16_
79 techmap -map +/simcells.v t:$_MUX4_
82 design -import gold -as gold
83 design -import gate -as gate
85 miter -equiv -flatten -make_assert -make_outputs gold gate miter
86 sat -verify -prove-asserts -show-ports miter
88 ## Partial matching MUX8
91 read_verilog -formal <<EOT
92 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);
117 muxcover -mux4=150 -mux8=200
118 select -assert-count 0 t:$_MUX_
119 select -assert-count 0 t:$_MUX4_
120 select -assert-count 1 t:$_MUX8_
121 select -assert-count 0 t:$_MUX16_
122 techmap -map +/simcells.v t:$_MUX8_
125 design -import gold -as gold
126 design -import gate -as gate
128 miter -equiv -flatten -make_assert -make_outputs gold gate miter
129 sat -verify -prove-asserts -show-ports miter
131 ## Partial matching MUX16
134 read_verilog -formal <<EOT
135 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);
173 muxcover -mux4=150 -mux8=200 -mux16=250
174 select -assert-count 0 t:$_MUX_
175 select -assert-count 0 t:$_MUX4_
176 select -assert-count 0 t:$_MUX8_
177 select -assert-count 1 t:$_MUX16_
178 techmap -map +/simcells.v t:$_MUX16_
181 design -import gold -as gold
182 design -import gate -as gate
184 miter -equiv -flatten -make_assert -make_outputs gold gate miter
185 sat -verify -prove-asserts -show-ports miter