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
191 ## MUX2 in MUX4 :: https://github.com/YosysHQ/yosys/issues/1132
194 read_verilog -formal <<EOT
195 module mux2in4(input [1:0] i, input s, output o);
196 assign o = s ? i[1] : i[0];
203 muxcover -mux4=0 -nodecode
206 select -assert-count 0 t:$_MUX_
207 select -assert-count 1 t:$_MUX4_
208 select -assert-count 0 t:$_MUX8_
209 select -assert-count 0 t:$_MUX16_
210 techmap -map +/simcells.v t:$_MUX4_
213 design -import gold -as gold
214 design -import gate -as gate
216 miter -equiv -flatten -make_assert -make_outputs gold gate miter
217 sat -verify -prove-asserts -show-ports miter
219 ## MUX2 in MUX8 :: https://github.com/YosysHQ/yosys/issues/1132
222 read_verilog -formal <<EOT
223 module mux2in8(input [1:0] i, input s, output o);
224 assign o = s ? i[1] : i[0];
231 muxcover -mux8=0 -nodecode
234 select -assert-count 0 t:$_MUX_
235 select -assert-count 0 t:$_MUX4_
236 select -assert-count 1 t:$_MUX8_
237 select -assert-count 0 t:$_MUX16_
238 techmap -map +/simcells.v t:$_MUX8_
241 design -import gold -as gold
242 design -import gate -as gate
244 miter -equiv -flatten -make_assert -make_outputs gold gate miter
245 sat -verify -prove-asserts -show-ports miter
247 ## MUX4 in MUX8 :: https://github.com/YosysHQ/yosys/issues/1132
250 read_verilog -formal <<EOT
251 module mux4in8(input [3:0] i, input [1:0] s, output o);
252 assign o = s[1] ? (s[0] ? i[3] : i[2]) : (s[0] ? i[1] : i[0]);
259 muxcover -mux8=0 -nodecode
262 select -assert-count 0 t:$_MUX_
263 select -assert-count 0 t:$_MUX4_
264 select -assert-count 1 t:$_MUX8_
265 select -assert-count 0 t:$_MUX16_
266 techmap -map +/simcells.v t:$_MUX8_
269 design -import gold -as gold
270 design -import gate -as gate
272 miter -equiv -flatten -make_assert -make_outputs gold gate miter
273 sat -verify -prove-asserts -show-ports miter
275 ## MUX2 in MUX16 :: https://github.com/YosysHQ/yosys/issues/1132
278 read_verilog -formal <<EOT
279 module mux2in16(input [1:0] i, input s, output o);
280 assign o = s ? i[1] : i[0];
287 muxcover -mux16=0 -nodecode
290 select -assert-count 0 t:$_MUX_
291 select -assert-count 0 t:$_MUX4_
292 select -assert-count 0 t:$_MUX8_
293 select -assert-count 1 t:$_MUX16_
294 techmap -map +/simcells.v t:$_MUX16_
297 design -import gold -as gold
298 design -import gate -as gate
300 miter -equiv -flatten -make_assert -make_outputs gold gate miter
301 sat -verify -prove-asserts -show-ports miter
303 ## MUX4 in MUX16 :: https://github.com/YosysHQ/yosys/issues/1132
306 read_verilog -formal <<EOT
307 module mux4in16(input [3:0] i, input [1:0] s, output o);
308 assign o = s[1] ? (s[0] ? i[3] : i[2]) : (s[0] ? i[1] : i[0]);
315 muxcover -mux16=0 -nodecode
318 select -assert-count 0 t:$_MUX_
319 select -assert-count 0 t:$_MUX4_
320 select -assert-count 0 t:$_MUX8_
321 select -assert-count 1 t:$_MUX16_
322 techmap -map +/simcells.v t:$_MUX16_
325 design -import gold -as gold
326 design -import gate -as gate
328 miter -equiv -flatten -make_assert -make_outputs gold gate miter
329 sat -verify -prove-asserts -show-ports miter
331 ## MUX8 in MUX16 :: https://github.com/YosysHQ/yosys/issues/1132
334 read_verilog -formal <<EOT
335 module mux4in16(input [7:0] i, input [2:0] s, output o);
336 assign o = s[2] ? s[1] ? (s[0] ? i[3] : i[2]) : (s[0] ? i[1] : i[0])
337 : s[1] ? (s[0] ? i[7] : i[6]) : (s[0] ? i[5] : i[4]);
344 muxcover -mux16=0 -nodecode
347 select -assert-count 0 t:$_MUX_
348 select -assert-count 0 t:$_MUX4_
349 select -assert-count 0 t:$_MUX8_
350 select -assert-count 1 t:$_MUX16_
351 techmap -map +/simcells.v t:$_MUX16_
354 design -import gold -as gold
355 design -import gate -as gate
357 miter -equiv -flatten -make_assert -make_outputs gold gate miter
358 sat -verify -prove-asserts -show-ports miter