3 hierarchy -top mux_if_unbal_4_1
9 select -assert-count 0 t:$mux
10 select -assert-count 1 t:$pmux
12 design -import gold -as gold
13 design -import gate -as gate
14 miter -equiv -flatten -make_assert -make_outputs gold gate miter
15 sat -verify -prove-asserts -show-ports miter
18 hierarchy -top mux_if_unbal_5_3
24 select -assert-count 0 t:$mux
25 select -assert-count 1 t:$pmux
27 design -import gold -as gold
28 design -import gate -as gate
29 miter -equiv -flatten -make_assert -make_outputs gold gate miter
30 sat -verify -prove-asserts -show-ports miter
33 hierarchy -top mux_if_unbal_5_3_invert
39 select -assert-count 0 t:$mux
40 select -assert-count 1 t:$pmux
42 design -import gold -as gold
43 design -import gate -as gate
44 miter -equiv -flatten -make_assert -make_outputs gold gate miter
45 sat -verify -prove-asserts -show-ports miter
48 hierarchy -top mux_if_unbal_5_3_width_mismatch
54 select -assert-count 0 t:$mux
55 select -assert-count 2 t:$pmux
57 design -import gold -as gold
58 design -import gate -as gate
59 miter -equiv -flatten -make_assert -make_outputs gold gate miter
60 sat -verify -prove-asserts -show-ports miter
63 hierarchy -top mux_if_unbal_4_1_missing
69 select -assert-count 0 t:$mux
70 select -assert-count 1 t:$pmux
72 design -import gold -as gold
73 design -import gate -as gate
74 miter -equiv -flatten -make_assert -make_outputs gold gate miter
75 sat -verify -prove-asserts -show-ports miter
78 hierarchy -top mux_if_unbal_5_3_order
84 select -assert-count 0 t:$mux
85 select -assert-count 1 t:$pmux
87 design -import gold -as gold
88 design -import gate -as gate
89 miter -equiv -flatten -make_assert -make_outputs gold gate miter
90 sat -verify -prove-asserts -show-ports miter
93 hierarchy -top mux_if_unbal_4_1_nonexcl
99 select -assert-count 0 t:$mux
100 select -assert-count 1 t:$pmux
102 design -import gold -as gold
103 design -import gate -as gate
104 miter -equiv -flatten -make_assert -make_outputs gold gate miter
105 sat -verify -prove-asserts -show-ports miter
108 hierarchy -top mux_if_unbal_5_3_nonexcl
114 select -assert-count 0 t:$mux
115 select -assert-count 1 t:$pmux
117 design -import gold -as gold
118 design -import gate -as gate
119 miter -equiv -flatten -make_assert -make_outputs gold gate miter
120 sat -verify -prove-asserts -show-ports miter
123 hierarchy -top mux_case_unbal_8_7
129 select -assert-count 0 t:$mux
130 select -assert-count 1 t:$pmux
132 design -import gold -as gold
133 design -import gate -as gate
134 miter -equiv -flatten -make_assert -make_outputs gold gate miter
135 sat -verify -prove-asserts -show-ports miter
138 hierarchy -top mux_if_bal_8_2
144 select -assert-count 7 t:$mux
145 select -assert-count 0 t:$pmux
147 design -import gold -as gold
148 design -import gate -as gate
149 miter -equiv -flatten -make_assert -make_outputs gold gate miter
150 sat -verify -prove-asserts -show-ports miter