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
120 select -assert-count 0 t:$_MUX_
121 select -assert-count 0 t:$_MUX4_
122 select -assert-count 1 t:$_MUX8_
123 select -assert-count 0 t:$_MUX16_
124 techmap -map +/simcells.v t:$_MUX8_
127 design -import gold -as gold
128 design -import gate -as gate
130 miter -equiv -flatten -make_assert -make_outputs gold gate miter
131 sat -verify -prove-asserts -show-ports miter
133 ## Partial matching MUX16
136 read_verilog -formal <<EOT
137 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);
175 muxcover -mux4=150 -mux8=200 -mux16=250
178 select -assert-count 0 t:$_MUX_
179 select -assert-count 0 t:$_MUX4_
180 select -assert-count 0 t:$_MUX8_
181 select -assert-count 1 t:$_MUX16_
182 techmap -map +/simcells.v t:$_MUX16_
185 design -import gold -as gold
186 design -import gate -as gate
188 miter -equiv -flatten -make_assert -make_outputs gold gate miter
189 sat -verify -prove-asserts -show-ports miter