4 hierarchy -top mux_if_unbal_4_1
10 select -assert-count 0 t:$mux
11 select -assert-count 1 t:$pmux
13 design -import gold -as gold
14 design -import gate -as gate
15 miter -equiv -flatten -make_assert -make_outputs gold gate miter
16 sat -verify -prove-asserts -show-ports miter
19 hierarchy -top mux_if_unbal_5_3
25 select -assert-count 0 t:$mux
26 select -assert-count 1 t:$pmux
28 design -import gold -as gold
29 design -import gate -as gate
30 miter -equiv -flatten -make_assert -make_outputs gold gate miter
31 sat -verify -prove-asserts -show-ports miter
33 # TODO: Currently ExclusiveDatabase only analyses $eq cells
35 #hierarchy -top mux_if_unbal_5_3_invert
41 #select -assert-count 0 t:$mux
42 #select -assert-count 1 t:$pmux
44 #design -import gold -as gold
45 #design -import gate -as gate
46 #miter -equiv -flatten -make_assert -make_outputs gold gate miter
47 #sat -verify -prove-asserts -show-ports miter
50 hierarchy -top mux_if_unbal_5_3_width_mismatch
56 select -assert-count 0 t:$mux
57 select -assert-count 2 t:$pmux
59 design -import gold -as gold
60 design -import gate -as gate
61 miter -equiv -flatten -make_assert -make_outputs gold gate miter
62 sat -verify -prove-asserts -show-ports miter
65 hierarchy -top mux_if_unbal_4_1_missing
71 select -assert-count 0 t:$mux
72 select -assert-count 1 t:$pmux
74 design -import gold -as gold
75 design -import gate -as gate
76 miter -equiv -flatten -make_assert -make_outputs gold gate miter
77 sat -verify -prove-asserts -show-ports miter
80 hierarchy -top mux_if_unbal_5_3_order
86 select -assert-count 0 t:$mux
87 select -assert-count 1 t:$pmux
89 design -import gold -as gold
90 design -import gate -as gate
91 miter -equiv -flatten -make_assert -make_outputs gold gate miter
92 sat -verify -prove-asserts -show-ports miter
95 hierarchy -top mux_if_unbal_4_1_nonexcl
101 select -assert-count 0 t:$mux
102 select -assert-count 1 t:$pmux
104 design -import gold -as gold
105 design -import gate -as gate
106 miter -equiv -flatten -make_assert -make_outputs gold gate miter
107 sat -verify -prove-asserts -show-ports miter
110 hierarchy -top mux_if_unbal_5_3_nonexcl
116 select -assert-count 0 t:$mux
117 select -assert-count 1 t:$pmux
119 design -import gold -as gold
120 design -import gate -as gate
121 miter -equiv -flatten -make_assert -make_outputs gold gate miter
122 sat -verify -prove-asserts -show-ports miter
125 hierarchy -top mux_case_unbal_8_7
131 select -assert-count 0 t:$mux
132 select -assert-count 1 t:$pmux
134 design -import gold -as gold
135 design -import gate -as gate
136 miter -equiv -flatten -make_assert -make_outputs gold gate miter
137 sat -verify -prove-asserts -show-ports miter
140 hierarchy -top mux_if_bal_8_2
146 select -assert-count 7 t:$mux
147 select -assert-count 0 t:$pmux
149 design -import gold -as gold
150 design -import gate -as gate
151 miter -equiv -flatten -make_assert -make_outputs gold gate miter
152 sat -verify -prove-asserts -show-ports miter
155 hierarchy -top mux_if_bal_5_1
161 select -assert-count 4 t:$mux
162 select -assert-count 0 t:$pmux
164 design -import gold -as gold
165 design -import gate -as gate
166 miter -equiv -flatten -make_assert -make_outputs gold gate miter
167 sat -verify -prove-asserts -show-ports miter
170 hierarchy -top cliffordwolf_nonexclusive_select
176 select -assert-count 3 t:$mux
177 select -assert-count 0 t:$pmux
179 design -import gold -as gold
180 design -import gate -as gate
181 miter -equiv -flatten -make_assert -make_outputs gold gate miter
182 sat -verify -prove-asserts -show-ports miter
185 #hierarchy -top cliffordwolf_freduce
188 #proc; opt; freduce; opt
193 #select -assert-count 0 t:$mux
194 #select -assert-count 1 t:$pmux
196 #design -import gold -as gold
197 #design -import gate -as gate
198 #miter -equiv -flatten -make_assert -make_outputs gold gate miter
199 #sat -verify -prove-asserts -show-ports miter
202 hierarchy -top case_nonexclusive_select
208 select -assert-count 0 t:$mux
209 select -assert-count 2 t:$pmux
211 design -import gold -as gold
212 design -import gate -as gate
213 miter -equiv -flatten -make_assert -make_outputs gold gate miter
214 sat -verify -prove-asserts -show-ports miter
217 hierarchy -top case_nonoverlap
223 select -assert-count 0 t:$mux
224 select -assert-count 1 t:$pmux
226 design -import gold -as gold
227 design -import gate -as gate
228 miter -equiv -flatten -make_assert -make_outputs gold gate miter
229 sat -verify -prove-asserts -show-ports miter
232 hierarchy -top case_overlap
233 #prep # Do not prep otherwise $pmux's overlapping entry will get removed
239 select -assert-count 0 t:$mux
240 select -assert-count 2 t:$pmux
242 design -import gold -as gold
243 design -import gate -as gate
244 miter -equiv -flatten -make_assert -make_outputs gold gate miter
245 sat -verify -prove-asserts -show-ports miter