projects / yosys.git / blob
? search:
summary | shortlog | log | commit | commitdiff | tree
history | raw | HEAD
Bump version
[yosys.git] / kernel / satgen.cc
1 /*
2 * yosys -- Yosys Open SYnthesis Suite
3 *
4 * Copyright (C) 2012 Claire Xenia Wolf <claire@yosyshq.com>
5 *
6 * Permission to use, copy, modify, and/or distribute this software for any
7 * purpose with or without fee is hereby granted, provided that the above
8 * copyright notice and this permission notice appear in all copies.
9 *
10 * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
11 * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
12 * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
13 * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
14 * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
15 * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
16 * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
17 *
18 */
19
20 #include "kernel/satgen.h"
21 #include "kernel/ff.h"
22
23 USING_YOSYS_NAMESPACE
24
25 bool SatGen::importCell(RTLIL::Cell *cell, int timestep)
26 {
27 bool arith_undef_handled = false;
28 bool is_arith_compare = cell->type.in(ID($lt), ID($le), ID($ge), ID($gt));
29
30 if (model_undef && (cell->type.in(ID($add), ID($sub), ID($mul), ID($div), ID($mod), ID($divfloor), ID($modfloor)) || is_arith_compare))
31 {
32 std::vector<int> undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
33 std::vector<int> undef_b = importUndefSigSpec(cell->getPort(ID::B), timestep);
34 std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
35 if (is_arith_compare)
36 extendSignalWidth(undef_a, undef_b, cell, true);
37 else
38 extendSignalWidth(undef_a, undef_b, undef_y, cell, true);
39
40 int undef_any_a = ez->expression(ezSAT::OpOr, undef_a);
41 int undef_any_b = ez->expression(ezSAT::OpOr, undef_b);
42 int undef_y_bit = ez->OR(undef_any_a, undef_any_b);
43
44 if (cell->type.in(ID($div), ID($mod), ID($divfloor), ID($modfloor))) {
45 std::vector<int> b = importSigSpec(cell->getPort(ID::B), timestep);
46 undef_y_bit = ez->OR(undef_y_bit, ez->NOT(ez->expression(ezSAT::OpOr, b)));
47 }
48
49 if (is_arith_compare) {
50 for (size_t i = 1; i < undef_y.size(); i++)
51 ez->SET(ez->CONST_FALSE, undef_y.at(i));
52 ez->SET(undef_y_bit, undef_y.at(0));
53 } else {
54 std::vector<int> undef_y_bits(undef_y.size(), undef_y_bit);
55 ez->assume(ez->vec_eq(undef_y_bits, undef_y));
56 }
57
58 arith_undef_handled = true;
59 }
60
61 if (cell->type.in(ID($_AND_), ID($_NAND_), ID($_OR_), ID($_NOR_), ID($_XOR_), ID($_XNOR_), ID($_ANDNOT_), ID($_ORNOT_),
62 ID($and), ID($or), ID($xor), ID($xnor), ID($add), ID($sub)))
63 {
64 std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
65 std::vector<int> b = importDefSigSpec(cell->getPort(ID::B), timestep);
66 std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep);
67 extendSignalWidth(a, b, y, cell);
68
69 std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
70
71 if (cell->type.in(ID($and), ID($_AND_)))
72 ez->assume(ez->vec_eq(ez->vec_and(a, b), yy));
73 if (cell->type == ID($_NAND_))
74 ez->assume(ez->vec_eq(ez->vec_not(ez->vec_and(a, b)), yy));
75 if (cell->type.in(ID($or), ID($_OR_)))
76 ez->assume(ez->vec_eq(ez->vec_or(a, b), yy));
77 if (cell->type == ID($_NOR_))
78 ez->assume(ez->vec_eq(ez->vec_not(ez->vec_or(a, b)), yy));
79 if (cell->type.in(ID($xor), ID($_XOR_)))
80 ez->assume(ez->vec_eq(ez->vec_xor(a, b), yy));
81 if (cell->type.in(ID($xnor), ID($_XNOR_)))
82 ez->assume(ez->vec_eq(ez->vec_not(ez->vec_xor(a, b)), yy));
83 if (cell->type == ID($_ANDNOT_))
84 ez->assume(ez->vec_eq(ez->vec_and(a, ez->vec_not(b)), yy));
85 if (cell->type == ID($_ORNOT_))
86 ez->assume(ez->vec_eq(ez->vec_or(a, ez->vec_not(b)), yy));
87 if (cell->type == ID($add))
88 ez->assume(ez->vec_eq(ez->vec_add(a, b), yy));
89 if (cell->type == ID($sub))
90 ez->assume(ez->vec_eq(ez->vec_sub(a, b), yy));
91
92 if (model_undef && !arith_undef_handled)
93 {
94 std::vector<int> undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
95 std::vector<int> undef_b = importUndefSigSpec(cell->getPort(ID::B), timestep);
96 std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
97 extendSignalWidth(undef_a, undef_b, undef_y, cell, false);
98
99 if (cell->type.in(ID($and), ID($_AND_), ID($_NAND_))) {
100 std::vector<int> a0 = ez->vec_and(ez->vec_not(a), ez->vec_not(undef_a));
101 std::vector<int> b0 = ez->vec_and(ez->vec_not(b), ez->vec_not(undef_b));
102 std::vector<int> yX = ez->vec_and(ez->vec_or(undef_a, undef_b), ez->vec_not(ez->vec_or(a0, b0)));
103 ez->assume(ez->vec_eq(yX, undef_y));
104 }
105 else if (cell->type.in(ID($or), ID($_OR_), ID($_NOR_))) {
106 std::vector<int> a1 = ez->vec_and(a, ez->vec_not(undef_a));
107 std::vector<int> b1 = ez->vec_and(b, ez->vec_not(undef_b));
108 std::vector<int> yX = ez->vec_and(ez->vec_or(undef_a, undef_b), ez->vec_not(ez->vec_or(a1, b1)));
109 ez->assume(ez->vec_eq(yX, undef_y));
110 }
111 else if (cell->type.in(ID($xor), ID($xnor), ID($_XOR_), ID($_XNOR_))) {
112 std::vector<int> yX = ez->vec_or(undef_a, undef_b);
113 ez->assume(ez->vec_eq(yX, undef_y));
114 }
115 else if (cell->type == ID($_ANDNOT_)) {
116 std::vector<int> a0 = ez->vec_and(ez->vec_not(a), ez->vec_not(undef_a));
117 std::vector<int> b1 = ez->vec_and(b, ez->vec_not(undef_b));
118 std::vector<int> yX = ez->vec_and(ez->vec_or(undef_a, undef_b), ez->vec_not(ez->vec_or(a0, b1)));
119 ez->assume(ez->vec_eq(yX, undef_y));
120 }
121
122 else if (cell->type == ID($_ORNOT_)) {
123 std::vector<int> a1 = ez->vec_and(a, ez->vec_not(undef_a));
124 std::vector<int> b0 = ez->vec_and(ez->vec_not(b), ez->vec_not(undef_b));
125 std::vector<int> yX = ez->vec_and(ez->vec_or(undef_a, undef_b), ez->vec_not(ez->vec_or(a1, b0)));
126 ez->assume(ez->vec_eq(yX, undef_y));
127 }
128 else
129 log_abort();
130
131 undefGating(y, yy, undef_y);
132 }
133 else if (model_undef)
134 {
135 std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
136 undefGating(y, yy, undef_y);
137 }
138 return true;
139 }
140
141 if (cell->type.in(ID($_AOI3_), ID($_OAI3_), ID($_AOI4_), ID($_OAI4_)))
142 {
143 bool aoi_mode = cell->type.in(ID($_AOI3_), ID($_AOI4_));
144 bool three_mode = cell->type.in(ID($_AOI3_), ID($_OAI3_));
145
146 int a = importDefSigSpec(cell->getPort(ID::A), timestep).at(0);
147 int b = importDefSigSpec(cell->getPort(ID::B), timestep).at(0);
148 int c = importDefSigSpec(cell->getPort(ID::C), timestep).at(0);
149 int d = three_mode ? (aoi_mode ? ez->CONST_TRUE : ez->CONST_FALSE) : importDefSigSpec(cell->getPort(ID::D), timestep).at(0);
150 int y = importDefSigSpec(cell->getPort(ID::Y), timestep).at(0);
151 int yy = model_undef ? ez->literal() : y;
152
153 if (cell->type.in(ID($_AOI3_), ID($_AOI4_)))
154 ez->assume(ez->IFF(ez->NOT(ez->OR(ez->AND(a, b), ez->AND(c, d))), yy));
155 else
156 ez->assume(ez->IFF(ez->NOT(ez->AND(ez->OR(a, b), ez->OR(c, d))), yy));
157
158 if (model_undef)
159 {
160 int undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep).at(0);
161 int undef_b = importUndefSigSpec(cell->getPort(ID::B), timestep).at(0);
162 int undef_c = importUndefSigSpec(cell->getPort(ID::C), timestep).at(0);
163 int undef_d = three_mode ? ez->CONST_FALSE : importUndefSigSpec(cell->getPort(ID::D), timestep).at(0);
164 int undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep).at(0);
165
166 if (aoi_mode)
167 {
168 int a0 = ez->AND(ez->NOT(a), ez->NOT(undef_a));
169 int b0 = ez->AND(ez->NOT(b), ez->NOT(undef_b));
170 int c0 = ez->AND(ez->NOT(c), ez->NOT(undef_c));
171 int d0 = ez->AND(ez->NOT(d), ez->NOT(undef_d));
172
173 int ab = ez->AND(a, b), cd = ez->AND(c, d);
174 int undef_ab = ez->AND(ez->OR(undef_a, undef_b), ez->NOT(ez->OR(a0, b0)));
175 int undef_cd = ez->AND(ez->OR(undef_c, undef_d), ez->NOT(ez->OR(c0, d0)));
176
177 int ab1 = ez->AND(ab, ez->NOT(undef_ab));
178 int cd1 = ez->AND(cd, ez->NOT(undef_cd));
179 int yX = ez->AND(ez->OR(undef_ab, undef_cd), ez->NOT(ez->OR(ab1, cd1)));
180
181 ez->assume(ez->IFF(yX, undef_y));
182 }
183 else
184 {
185 int a1 = ez->AND(a, ez->NOT(undef_a));
186 int b1 = ez->AND(b, ez->NOT(undef_b));
187 int c1 = ez->AND(c, ez->NOT(undef_c));
188 int d1 = ez->AND(d, ez->NOT(undef_d));
189
190 int ab = ez->OR(a, b), cd = ez->OR(c, d);
191 int undef_ab = ez->AND(ez->OR(undef_a, undef_b), ez->NOT(ez->OR(a1, b1)));
192 int undef_cd = ez->AND(ez->OR(undef_c, undef_d), ez->NOT(ez->OR(c1, d1)));
193
194 int ab0 = ez->AND(ez->NOT(ab), ez->NOT(undef_ab));
195 int cd0 = ez->AND(ez->NOT(cd), ez->NOT(undef_cd));
196 int yX = ez->AND(ez->OR(undef_ab, undef_cd), ez->NOT(ez->OR(ab0, cd0)));
197
198 ez->assume(ez->IFF(yX, undef_y));
199 }
200
201 undefGating(y, yy, undef_y);
202 }
203
204 return true;
205 }
206
207 if (cell->type.in(ID($_NOT_), ID($not)))
208 {
209 std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
210 std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep);
211 extendSignalWidthUnary(a, y, cell);
212
213 std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
214 ez->assume(ez->vec_eq(ez->vec_not(a), yy));
215
216 if (model_undef) {
217 std::vector<int> undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
218 std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
219 extendSignalWidthUnary(undef_a, undef_y, cell, false);
220 ez->assume(ez->vec_eq(undef_a, undef_y));
221 undefGating(y, yy, undef_y);
222 }
223 return true;
224 }
225
226 if (cell->type.in(ID($_MUX_), ID($mux), ID($_NMUX_)))
227 {
228 std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
229 std::vector<int> b = importDefSigSpec(cell->getPort(ID::B), timestep);
230 std::vector<int> s = importDefSigSpec(cell->getPort(ID::S), timestep);
231 std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep);
232
233 std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
234 if (cell->type == ID($_NMUX_))
235 ez->assume(ez->vec_eq(ez->vec_not(ez->vec_ite(s.at(0), b, a)), yy));
236 else
237 ez->assume(ez->vec_eq(ez->vec_ite(s.at(0), b, a), yy));
238
239 if (model_undef)
240 {
241 std::vector<int> undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
242 std::vector<int> undef_b = importUndefSigSpec(cell->getPort(ID::B), timestep);
243 std::vector<int> undef_s = importUndefSigSpec(cell->getPort(ID::S), timestep);
244 std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
245
246 std::vector<int> unequal_ab = ez->vec_not(ez->vec_iff(a, b));
247 std::vector<int> undef_ab = ez->vec_or(unequal_ab, ez->vec_or(undef_a, undef_b));
248 std::vector<int> yX = ez->vec_ite(undef_s.at(0), undef_ab, ez->vec_ite(s.at(0), undef_b, undef_a));
249 ez->assume(ez->vec_eq(yX, undef_y));
250 undefGating(y, yy, undef_y);
251 }
252 return true;
253 }
254
255 if (cell->type == ID($bmux))
256 {
257 std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
258 std::vector<int> s = importDefSigSpec(cell->getPort(ID::S), timestep);
259 std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep);
260 std::vector<int> undef_a, undef_s, undef_y;
261
262 if (model_undef)
263 {
264 undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
265 undef_s = importUndefSigSpec(cell->getPort(ID::S), timestep);
266 undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
267 }
268
269 if (GetSize(s) == 0) {
270 ez->vec_set(a, y);
271 if (model_undef)
272 ez->vec_set(undef_a, undef_y);
273 } else {
274 for (int i = GetSize(s)-1; i >= 0; i--)
275 {
276 std::vector<int> out = (i == 0) ? y : ez->vec_var(a.size() / 2);
277 std::vector<int> yy = model_undef ? ez->vec_var(out.size()) : out;
278
279 std::vector<int> a0(a.begin(), a.begin() + a.size() / 2);
280 std::vector<int> a1(a.begin() + a.size() / 2, a.end());
281 ez->assume(ez->vec_eq(ez->vec_ite(s.at(i), a1, a0), yy));
282
283 if (model_undef)
284 {
285 std::vector<int> undef_out = (i == 0) ? undef_y : ez->vec_var(a.size() / 2);
286 std::vector<int> undef_a0(undef_a.begin(), undef_a.begin() + a.size() / 2);
287 std::vector<int> undef_a1(undef_a.begin() + a.size() / 2, undef_a.end());
288 std::vector<int> unequal_ab = ez->vec_not(ez->vec_iff(a0, a1));
289 std::vector<int> undef_ab = ez->vec_or(unequal_ab, ez->vec_or(undef_a0, undef_a1));
290 std::vector<int> yX = ez->vec_ite(undef_s.at(i), undef_ab, ez->vec_ite(s.at(i), undef_a1, undef_a0));
291 ez->assume(ez->vec_eq(yX, undef_out));
292 undefGating(out, yy, undef_out);
293
294 undef_a = undef_out;
295 }
296
297 a = out;
298 }
299 }
300 return true;
301 }
302
303 if (cell->type == ID($demux))
304 {
305 std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
306 std::vector<int> s = importDefSigSpec(cell->getPort(ID::S), timestep);
307 std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep);
308 std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
309 std::vector<int> undef_a, undef_s, undef_y;
310
311 if (model_undef)
312 {
313 undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
314 undef_s = importUndefSigSpec(cell->getPort(ID::S), timestep);
315 undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
316 }
317
318 if (GetSize(s) == 0) {
319 ez->vec_set(a, y);
320 if (model_undef)
321 ez->vec_set(undef_a, undef_y);
322 } else {
323 for (int i = 0; i < (1 << GetSize(s)); i++)
324 {
325 std::vector<int> ss;
326 for (int j = 0; j < GetSize(s); j++) {
327 if (i & 1 << j)
328 ss.push_back(s[j]);
329 else
330 ss.push_back(ez->NOT(s[j]));
331 }
332 int sss = ez->expression(ezSAT::OpAnd, ss);
333
334 for (int j = 0; j < GetSize(a); j++) {
335 ez->SET(ez->AND(sss, a[j]), yy.at(i * GetSize(a) + j));
336 }
337
338 if (model_undef)
339 {
340 int s0 = ez->expression(ezSAT::OpOr, ez->vec_and(ez->vec_not(ss), ez->vec_not(undef_s)));
341 int us = ez->AND(ez->NOT(s0), ez->expression(ezSAT::OpOr, undef_s));
342 for (int j = 0; j < GetSize(a); j++) {
343 int a0 = ez->AND(ez->NOT(a[j]), ez->NOT(undef_a[j]));
344 int yX = ez->AND(ez->OR(us, undef_a[j]), ez->NOT(ez->OR(s0, a0)));
345 ez->SET(yX, undef_y.at(i * GetSize(a) + j));
346 }
347 }
348 }
349 if (model_undef)
350 undefGating(y, yy, undef_y);
351 }
352 return true;
353 }
354
355 if (cell->type == ID($pmux))
356 {
357 std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
358 std::vector<int> b = importDefSigSpec(cell->getPort(ID::B), timestep);
359 std::vector<int> s = importDefSigSpec(cell->getPort(ID::S), timestep);
360 std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep);
361
362 std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
363
364 std::vector<int> tmp = a;
365 for (size_t i = 0; i < s.size(); i++) {
366 std::vector<int> part_of_b(b.begin()+i*a.size(), b.begin()+(i+1)*a.size());
367 tmp = ez->vec_ite(s.at(i), part_of_b, tmp);
368 }
369 ez->assume(ez->vec_eq(tmp, yy));
370
371 if (model_undef)
372 {
373 std::vector<int> undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
374 std::vector<int> undef_b = importUndefSigSpec(cell->getPort(ID::B), timestep);
375 std::vector<int> undef_s = importUndefSigSpec(cell->getPort(ID::S), timestep);
376 std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
377
378 int maybe_a = ez->CONST_TRUE;
379
380 std::vector<int> bits_set = std::vector<int>(undef_y.size(), ez->CONST_FALSE);
381 std::vector<int> bits_clr = std::vector<int>(undef_y.size(), ez->CONST_FALSE);
382
383 for (size_t i = 0; i < s.size(); i++)
384 {
385 std::vector<int> part_of_b(b.begin()+i*a.size(), b.begin()+(i+1)*a.size());
386 std::vector<int> part_of_undef_b(undef_b.begin()+i*a.size(), undef_b.begin()+(i+1)*a.size());
387
388 int maybe_s = ez->OR(s.at(i), undef_s.at(i));
389 int sure_s = ez->AND(s.at(i), ez->NOT(undef_s.at(i)));
390
391 maybe_a = ez->AND(maybe_a, ez->NOT(sure_s));
392
393 bits_set = ez->vec_ite(maybe_s, ez->vec_or(bits_set, ez->vec_or(part_of_b, part_of_undef_b)), bits_set);
394 bits_clr = ez->vec_ite(maybe_s, ez->vec_or(bits_clr, ez->vec_or(ez->vec_not(part_of_b), part_of_undef_b)), bits_clr);
395 }
396
397 bits_set = ez->vec_ite(maybe_a, ez->vec_or(bits_set, ez->vec_or(bits_set, ez->vec_or(a, undef_a))), bits_set);
398 bits_clr = ez->vec_ite(maybe_a, ez->vec_or(bits_clr, ez->vec_or(bits_clr, ez->vec_or(ez->vec_not(a), undef_a))), bits_clr);
399
400 ez->assume(ez->vec_eq(ez->vec_not(ez->vec_xor(bits_set, bits_clr)), undef_y));
401 undefGating(y, yy, undef_y);
402 }
403 return true;
404 }
405
406 if (cell->type.in(ID($pos), ID($neg)))
407 {
408 std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
409 std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep);
410 extendSignalWidthUnary(a, y, cell);
411
412 std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
413
414 if (cell->type == ID($pos)) {
415 ez->assume(ez->vec_eq(a, yy));
416 } else {
417 std::vector<int> zero(a.size(), ez->CONST_FALSE);
418 ez->assume(ez->vec_eq(ez->vec_sub(zero, a), yy));
419 }
420
421 if (model_undef)
422 {
423 std::vector<int> undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
424 std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
425 extendSignalWidthUnary(undef_a, undef_y, cell);
426
427 if (cell->type == ID($pos)) {
428 ez->assume(ez->vec_eq(undef_a, undef_y));
429 } else {
430 int undef_any_a = ez->expression(ezSAT::OpOr, undef_a);
431 std::vector<int> undef_y_bits(undef_y.size(), undef_any_a);
432 ez->assume(ez->vec_eq(undef_y_bits, undef_y));
433 }
434
435 undefGating(y, yy, undef_y);
436 }
437 return true;
438 }
439
440 if (cell->type.in(ID($reduce_and), ID($reduce_or), ID($reduce_xor), ID($reduce_xnor), ID($reduce_bool), ID($logic_not)))
441 {
442 std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
443 std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep);
444
445 std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
446
447 if (cell->type == ID($reduce_and))
448 ez->SET(ez->expression(ez->OpAnd, a), yy.at(0));
449 if (cell->type.in(ID($reduce_or), ID($reduce_bool)))
450 ez->SET(ez->expression(ez->OpOr, a), yy.at(0));
451 if (cell->type == ID($reduce_xor))
452 ez->SET(ez->expression(ez->OpXor, a), yy.at(0));
453 if (cell->type == ID($reduce_xnor))
454 ez->SET(ez->NOT(ez->expression(ez->OpXor, a)), yy.at(0));
455 if (cell->type == ID($logic_not))
456 ez->SET(ez->NOT(ez->expression(ez->OpOr, a)), yy.at(0));
457 for (size_t i = 1; i < y.size(); i++)
458 ez->SET(ez->CONST_FALSE, yy.at(i));
459
460 if (model_undef)
461 {
462 std::vector<int> undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
463 std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
464 int aX = ez->expression(ezSAT::OpOr, undef_a);
465
466 if (cell->type == ID($reduce_and)) {
467 int a0 = ez->expression(ezSAT::OpOr, ez->vec_and(ez->vec_not(a), ez->vec_not(undef_a)));
468 ez->assume(ez->IFF(ez->AND(ez->NOT(a0), aX), undef_y.at(0)));
469 }
470 else if (cell->type.in(ID($reduce_or), ID($reduce_bool), ID($logic_not))) {
471 int a1 = ez->expression(ezSAT::OpOr, ez->vec_and(a, ez->vec_not(undef_a)));
472 ez->assume(ez->IFF(ez->AND(ez->NOT(a1), aX), undef_y.at(0)));
473 }
474 else if (cell->type.in(ID($reduce_xor), ID($reduce_xnor))) {
475 ez->assume(ez->IFF(aX, undef_y.at(0)));
476 } else
477 log_abort();
478
479 for (size_t i = 1; i < undef_y.size(); i++)
480 ez->SET(ez->CONST_FALSE, undef_y.at(i));
481
482 undefGating(y, yy, undef_y);
483 }
484 return true;
485 }
486
487 if (cell->type.in(ID($logic_and), ID($logic_or)))
488 {
489 std::vector<int> vec_a = importDefSigSpec(cell->getPort(ID::A), timestep);
490 std::vector<int> vec_b = importDefSigSpec(cell->getPort(ID::B), timestep);
491
492 int a = ez->expression(ez->OpOr, vec_a);
493 int b = ez->expression(ez->OpOr, vec_b);
494 std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep);
495
496 std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
497
498 if (cell->type == ID($logic_and))
499 ez->SET(ez->expression(ez->OpAnd, a, b), yy.at(0));
500 else
501 ez->SET(ez->expression(ez->OpOr, a, b), yy.at(0));
502 for (size_t i = 1; i < y.size(); i++)
503 ez->SET(ez->CONST_FALSE, yy.at(i));
504
505 if (model_undef)
506 {
507 std::vector<int> undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
508 std::vector<int> undef_b = importUndefSigSpec(cell->getPort(ID::B), timestep);
509 std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
510
511 int a0 = ez->NOT(ez->OR(ez->expression(ezSAT::OpOr, vec_a), ez->expression(ezSAT::OpOr, undef_a)));
512 int b0 = ez->NOT(ez->OR(ez->expression(ezSAT::OpOr, vec_b), ez->expression(ezSAT::OpOr, undef_b)));
513 int a1 = ez->expression(ezSAT::OpOr, ez->vec_and(vec_a, ez->vec_not(undef_a)));
514 int b1 = ez->expression(ezSAT::OpOr, ez->vec_and(vec_b, ez->vec_not(undef_b)));
515 int aX = ez->expression(ezSAT::OpOr, undef_a);
516 int bX = ez->expression(ezSAT::OpOr, undef_b);
517
518 if (cell->type == ID($logic_and))
519 ez->SET(ez->AND(ez->OR(aX, bX), ez->NOT(ez->AND(a1, b1)), ez->NOT(a0), ez->NOT(b0)), undef_y.at(0));
520 else if (cell->type == ID($logic_or))
521 ez->SET(ez->AND(ez->OR(aX, bX), ez->NOT(ez->AND(a0, b0)), ez->NOT(a1), ez->NOT(b1)), undef_y.at(0));
522 else
523 log_abort();
524
525 for (size_t i = 1; i < undef_y.size(); i++)
526 ez->SET(ez->CONST_FALSE, undef_y.at(i));
527
528 undefGating(y, yy, undef_y);
529 }
530 return true;
531 }
532
533 if (cell->type.in(ID($lt), ID($le), ID($eq), ID($ne), ID($eqx), ID($nex), ID($ge), ID($gt)))
534 {
535 bool is_signed = cell->parameters[ID::A_SIGNED].as_bool() && cell->parameters[ID::B_SIGNED].as_bool();
536 std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
537 std::vector<int> b = importDefSigSpec(cell->getPort(ID::B), timestep);
538 std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep);
539 extendSignalWidth(a, b, cell);
540
541 std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
542
543 if (model_undef && cell->type.in(ID($eqx), ID($nex))) {
544 std::vector<int> undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
545 std::vector<int> undef_b = importUndefSigSpec(cell->getPort(ID::B), timestep);
546 extendSignalWidth(undef_a, undef_b, cell, true);
547 a = ez->vec_or(a, undef_a);
548 b = ez->vec_or(b, undef_b);
549 }
550
551 if (cell->type == ID($lt))
552 ez->SET(is_signed ? ez->vec_lt_signed(a, b) : ez->vec_lt_unsigned(a, b), yy.at(0));
553 if (cell->type == ID($le))
554 ez->SET(is_signed ? ez->vec_le_signed(a, b) : ez->vec_le_unsigned(a, b), yy.at(0));
555 if (cell->type.in(ID($eq), ID($eqx)))
556 ez->SET(ez->vec_eq(a, b), yy.at(0));
557 if (cell->type.in(ID($ne), ID($nex)))
558 ez->SET(ez->vec_ne(a, b), yy.at(0));
559 if (cell->type == ID($ge))
560 ez->SET(is_signed ? ez->vec_ge_signed(a, b) : ez->vec_ge_unsigned(a, b), yy.at(0));
561 if (cell->type == ID($gt))
562 ez->SET(is_signed ? ez->vec_gt_signed(a, b) : ez->vec_gt_unsigned(a, b), yy.at(0));
563 for (size_t i = 1; i < y.size(); i++)
564 ez->SET(ez->CONST_FALSE, yy.at(i));
565
566 if (model_undef && cell->type.in(ID($eqx), ID($nex)))
567 {
568 std::vector<int> undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
569 std::vector<int> undef_b = importUndefSigSpec(cell->getPort(ID::B), timestep);
570 std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
571 extendSignalWidth(undef_a, undef_b, cell, true);
572
573 if (cell->type == ID($eqx))
574 yy.at(0) = ez->AND(yy.at(0), ez->vec_eq(undef_a, undef_b));
575 else
576 yy.at(0) = ez->OR(yy.at(0), ez->vec_ne(undef_a, undef_b));
577
578 for (size_t i = 0; i < y.size(); i++)
579 ez->SET(ez->CONST_FALSE, undef_y.at(i));
580
581 ez->assume(ez->vec_eq(y, yy));
582 }
583 else if (model_undef && cell->type.in(ID($eq), ID($ne)))
584 {
585 std::vector<int> undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
586 std::vector<int> undef_b = importUndefSigSpec(cell->getPort(ID::B), timestep);
587 std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
588 extendSignalWidth(undef_a, undef_b, cell, true);
589
590 int undef_any_a = ez->expression(ezSAT::OpOr, undef_a);
591 int undef_any_b = ez->expression(ezSAT::OpOr, undef_b);
592 int undef_any = ez->OR(undef_any_a, undef_any_b);
593
594 std::vector<int> masked_a_bits = ez->vec_or(a, ez->vec_or(undef_a, undef_b));
595 std::vector<int> masked_b_bits = ez->vec_or(b, ez->vec_or(undef_a, undef_b));
596
597 int masked_ne = ez->vec_ne(masked_a_bits, masked_b_bits);
598 int undef_y_bit = ez->AND(undef_any, ez->NOT(masked_ne));
599
600 for (size_t i = 1; i < undef_y.size(); i++)
601 ez->SET(ez->CONST_FALSE, undef_y.at(i));
602 ez->SET(undef_y_bit, undef_y.at(0));
603
604 undefGating(y, yy, undef_y);
605 }
606 else
607 {
608 if (model_undef) {
609 std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
610 undefGating(y, yy, undef_y);
611 }
612 log_assert(!model_undef || arith_undef_handled);
613 }
614 return true;
615 }
616
617 if (cell->type.in(ID($shl), ID($shr), ID($sshl), ID($sshr), ID($shift), ID($shiftx)))
618 {
619 std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
620 std::vector<int> b = importDefSigSpec(cell->getPort(ID::B), timestep);
621 std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep);
622
623 int extend_bit = ez->CONST_FALSE;
624
625 if (cell->parameters[ID::A_SIGNED].as_bool())
626 extend_bit = a.back();
627
628 while (y.size() < a.size())
629 y.push_back(ez->literal());
630 while (y.size() > a.size())
631 a.push_back(extend_bit);
632
633 std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
634 std::vector<int> shifted_a;
635
636 if (cell->type.in( ID($shl), ID($sshl)))
637 shifted_a = ez->vec_shift_left(a, b, false, ez->CONST_FALSE, ez->CONST_FALSE);
638
639 if (cell->type == ID($shr))
640 shifted_a = ez->vec_shift_right(a, b, false, ez->CONST_FALSE, ez->CONST_FALSE);
641
642 if (cell->type == ID($sshr))
643 shifted_a = ez->vec_shift_right(a, b, false, cell->parameters[ID::A_SIGNED].as_bool() ? a.back() : ez->CONST_FALSE, ez->CONST_FALSE);
644
645 if (cell->type.in(ID($shift), ID($shiftx)))
646 shifted_a = ez->vec_shift_right(a, b, cell->parameters[ID::B_SIGNED].as_bool(), ez->CONST_FALSE, ez->CONST_FALSE);
647
648 ez->assume(ez->vec_eq(shifted_a, yy));
649
650 if (model_undef)
651 {
652 std::vector<int> undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
653 std::vector<int> undef_b = importUndefSigSpec(cell->getPort(ID::B), timestep);
654 std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
655 std::vector<int> undef_a_shifted;
656
657 extend_bit = cell->type == ID($shiftx) ? ez->CONST_TRUE : ez->CONST_FALSE;
658 if (cell->parameters[ID::A_SIGNED].as_bool())
659 extend_bit = undef_a.back();
660
661 while (undef_y.size() < undef_a.size())
662 undef_y.push_back(ez->literal());
663 while (undef_y.size() > undef_a.size())
664 undef_a.push_back(extend_bit);
665
666 if (cell->type.in(ID($shl), ID($sshl)))
667 undef_a_shifted = ez->vec_shift_left(undef_a, b, false, ez->CONST_FALSE, ez->CONST_FALSE);
668
669 if (cell->type == ID($shr))
670 undef_a_shifted = ez->vec_shift_right(undef_a, b, false, ez->CONST_FALSE, ez->CONST_FALSE);
671
672 if (cell->type == ID($sshr))
673 undef_a_shifted = ez->vec_shift_right(undef_a, b, false, cell->parameters[ID::A_SIGNED].as_bool() ? undef_a.back() : ez->CONST_FALSE, ez->CONST_FALSE);
674
675 if (cell->type == ID($shift))
676 undef_a_shifted = ez->vec_shift_right(undef_a, b, cell->parameters[ID::B_SIGNED].as_bool(), ez->CONST_FALSE, ez->CONST_FALSE);
677
678 if (cell->type == ID($shiftx))
679 undef_a_shifted = ez->vec_shift_right(undef_a, b, cell->parameters[ID::B_SIGNED].as_bool(), ez->CONST_TRUE, ez->CONST_TRUE);
680
681 int undef_any_b = ez->expression(ezSAT::OpOr, undef_b);
682 std::vector<int> undef_all_y_bits(undef_y.size(), undef_any_b);
683 ez->assume(ez->vec_eq(ez->vec_or(undef_a_shifted, undef_all_y_bits), undef_y));
684 undefGating(y, yy, undef_y);
685 }
686 return true;
687 }
688
689 if (cell->type == ID($mul))
690 {
691 std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
692 std::vector<int> b = importDefSigSpec(cell->getPort(ID::B), timestep);
693 std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep);
694 extendSignalWidth(a, b, y, cell);
695
696 std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
697
698 std::vector<int> tmp(a.size(), ez->CONST_FALSE);
699 for (int i = 0; i < int(a.size()); i++)
700 {
701 std::vector<int> shifted_a(a.size(), ez->CONST_FALSE);
702 for (int j = i; j < int(a.size()); j++)
703 shifted_a.at(j) = a.at(j-i);
704 tmp = ez->vec_ite(b.at(i), ez->vec_add(tmp, shifted_a), tmp);
705 }
706 ez->assume(ez->vec_eq(tmp, yy));
707
708 if (model_undef) {
709 log_assert(arith_undef_handled);
710 std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
711 undefGating(y, yy, undef_y);
712 }
713 return true;
714 }
715
716 if (cell->type == ID($macc))
717 {
718 std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
719 std::vector<int> b = importDefSigSpec(cell->getPort(ID::B), timestep);
720 std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep);
721
722 Macc macc;
723 macc.from_cell(cell);
724
725 std::vector<int> tmp(GetSize(y), ez->CONST_FALSE);
726
727 for (auto &port : macc.ports)
728 {
729 std::vector<int> in_a = importDefSigSpec(port.in_a, timestep);
730 std::vector<int> in_b = importDefSigSpec(port.in_b, timestep);
731
732 while (GetSize(in_a) < GetSize(y))
733 in_a.push_back(port.is_signed && !in_a.empty() ? in_a.back() : ez->CONST_FALSE);
734 in_a.resize(GetSize(y));
735
736 if (GetSize(in_b))
737 {
738 while (GetSize(in_b) < GetSize(y))
739 in_b.push_back(port.is_signed && !in_b.empty() ? in_b.back() : ez->CONST_FALSE);
740 in_b.resize(GetSize(y));
741
742 for (int i = 0; i < GetSize(in_b); i++) {
743 std::vector<int> shifted_a(in_a.size(), ez->CONST_FALSE);
744 for (int j = i; j < int(in_a.size()); j++)
745 shifted_a.at(j) = in_a.at(j-i);
746 if (port.do_subtract)
747 tmp = ez->vec_ite(in_b.at(i), ez->vec_sub(tmp, shifted_a), tmp);
748 else
749 tmp = ez->vec_ite(in_b.at(i), ez->vec_add(tmp, shifted_a), tmp);
750 }
751 }
752 else
753 {
754 if (port.do_subtract)
755 tmp = ez->vec_sub(tmp, in_a);
756 else
757 tmp = ez->vec_add(tmp, in_a);
758 }
759 }
760
761 for (int i = 0; i < GetSize(b); i++) {
762 std::vector<int> val(GetSize(y), ez->CONST_FALSE);
763 val.at(0) = b.at(i);
764 tmp = ez->vec_add(tmp, val);
765 }
766
767 if (model_undef)
768 {
769 std::vector<int> undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
770 std::vector<int> undef_b = importUndefSigSpec(cell->getPort(ID::B), timestep);
771
772 int undef_any_a = ez->expression(ezSAT::OpOr, undef_a);
773 int undef_any_b = ez->expression(ezSAT::OpOr, undef_b);
774
775 std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
776 ez->assume(ez->vec_eq(undef_y, std::vector<int>(GetSize(y), ez->OR(undef_any_a, undef_any_b))));
777
778 undefGating(y, tmp, undef_y);
779 }
780 else
781 ez->assume(ez->vec_eq(y, tmp));
782
783 return true;
784 }
785
786 if (cell->type.in(ID($div), ID($mod), ID($divfloor), ID($modfloor)))
787 {
788 std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
789 std::vector<int> b = importDefSigSpec(cell->getPort(ID::B), timestep);
790 std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep);
791 extendSignalWidth(a, b, y, cell);
792
793 std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
794
795 std::vector<int> a_u, b_u;
796 if (cell->parameters[ID::A_SIGNED].as_bool() && cell->parameters[ID::B_SIGNED].as_bool()) {
797 a_u = ez->vec_ite(a.back(), ez->vec_neg(a), a);
798 b_u = ez->vec_ite(b.back(), ez->vec_neg(b), b);
799 } else {
800 a_u = a;
801 b_u = b;
802 }
803
804 std::vector<int> chain_buf = a_u;
805 std::vector<int> y_u(a_u.size(), ez->CONST_FALSE);
806 for (int i = int(a.size())-1; i >= 0; i--)
807 {
808 chain_buf.insert(chain_buf.end(), chain_buf.size(), ez->CONST_FALSE);
809
810 std::vector<int> b_shl(i, ez->CONST_FALSE);
811 b_shl.insert(b_shl.end(), b_u.begin(), b_u.end());
812 b_shl.insert(b_shl.end(), chain_buf.size()-b_shl.size(), ez->CONST_FALSE);
813
814 y_u.at(i) = ez->vec_ge_unsigned(chain_buf, b_shl);
815 chain_buf = ez->vec_ite(y_u.at(i), ez->vec_sub(chain_buf, b_shl), chain_buf);
816
817 chain_buf.erase(chain_buf.begin() + a_u.size(), chain_buf.end());
818 }
819
820 std::vector<int> y_tmp = ignore_div_by_zero ? yy : ez->vec_var(y.size());
821
822 // modulo calculation
823 std::vector<int> modulo_trunc;
824 int floored_eq_trunc;
825 if (cell->parameters[ID::A_SIGNED].as_bool() && cell->parameters[ID::B_SIGNED].as_bool()) {
826 modulo_trunc = ez->vec_ite(a.back(), ez->vec_neg(chain_buf), chain_buf);
827 // floor == trunc when sgn(a) == sgn(b) or trunc == 0
828 floored_eq_trunc = ez->OR(ez->IFF(a.back(), b.back()), ez->NOT(ez->expression(ezSAT::OpOr, modulo_trunc)));
829 } else {
830 modulo_trunc = chain_buf;
831 floored_eq_trunc = ez->CONST_TRUE;
832 }
833
834 if (cell->type == ID($div)) {
835 if (cell->parameters[ID::A_SIGNED].as_bool() && cell->parameters[ID::B_SIGNED].as_bool())
836 ez->assume(ez->vec_eq(y_tmp, ez->vec_ite(ez->XOR(a.back(), b.back()), ez->vec_neg(y_u), y_u)));
837 else
838 ez->assume(ez->vec_eq(y_tmp, y_u));
839 } else if (cell->type == ID($mod)) {
840 ez->assume(ez->vec_eq(y_tmp, modulo_trunc));
841 } else if (cell->type == ID($divfloor)) {
842 if (cell->parameters[ID::A_SIGNED].as_bool() && cell->parameters[ID::B_SIGNED].as_bool())
843 ez->assume(ez->vec_eq(y_tmp, ez->vec_ite(
844 ez->XOR(a.back(), b.back()),
845 ez->vec_neg(ez->vec_ite(
846 ez->vec_reduce_or(modulo_trunc),
847 ez->vec_add(y_u, ez->vec_const_unsigned(1, y_u.size())),
848 y_u
849 )),
850 y_u
851 )));
852 else
853 ez->assume(ez->vec_eq(y_tmp, y_u));
854 } else if (cell->type == ID($modfloor)) {
855 ez->assume(ez->vec_eq(y_tmp, ez->vec_ite(floored_eq_trunc, modulo_trunc, ez->vec_add(modulo_trunc, b))));
856 }
857
858 if (ignore_div_by_zero) {
859 ez->assume(ez->expression(ezSAT::OpOr, b));
860 } else {
861 std::vector<int> div_zero_result;
862 if (cell->type.in(ID($div), ID($divfloor))) {
863 if (cell->parameters[ID::A_SIGNED].as_bool() && cell->parameters[ID::B_SIGNED].as_bool()) {
864 std::vector<int> all_ones(y.size(), ez->CONST_TRUE);
865 std::vector<int> only_first_one(y.size(), ez->CONST_FALSE);
866 only_first_one.at(0) = ez->CONST_TRUE;
867 div_zero_result = ez->vec_ite(a.back(), only_first_one, all_ones);
868 } else {
869 div_zero_result.insert(div_zero_result.end(), cell->getPort(ID::A).size(), ez->CONST_TRUE);
870 div_zero_result.insert(div_zero_result.end(), y.size() - div_zero_result.size(), ez->CONST_FALSE);
871 }
872 } else if (cell->type.in(ID($mod), ID($modfloor))) {
873 // a mod 0 = a
874 int copy_a_bits = min(cell->getPort(ID::A).size(), cell->getPort(ID::B).size());
875 div_zero_result.insert(div_zero_result.end(), a.begin(), a.begin() + copy_a_bits);
876 if (cell->parameters[ID::A_SIGNED].as_bool() && cell->parameters[ID::B_SIGNED].as_bool())
877 div_zero_result.insert(div_zero_result.end(), y.size() - div_zero_result.size(), div_zero_result.back());
878 else
879 div_zero_result.insert(div_zero_result.end(), y.size() - div_zero_result.size(), ez->CONST_FALSE);
880 }
881 ez->assume(ez->vec_eq(yy, ez->vec_ite(ez->expression(ezSAT::OpOr, b), y_tmp, div_zero_result)));
882 }
883
884 if (model_undef) {
885 log_assert(arith_undef_handled);
886 std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
887 undefGating(y, yy, undef_y);
888 }
889 return true;
890 }
891
892 if (cell->type == ID($lut))
893 {
894 std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
895 std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep);
896
897 std::vector<int> lut;
898 for (auto bit : cell->getParam(ID::LUT).bits)
899 lut.push_back(bit == State::S1 ? ez->CONST_TRUE : ez->CONST_FALSE);
900 while (GetSize(lut) < (1 << GetSize(a)))
901 lut.push_back(ez->CONST_FALSE);
902 lut.resize(1 << GetSize(a));
903
904 if (model_undef)
905 {
906 std::vector<int> undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
907 std::vector<int> t(lut), u(GetSize(t), ez->CONST_FALSE);
908
909 for (int i = GetSize(a)-1; i >= 0; i--)
910 {
911 std::vector<int> t0(t.begin(), t.begin() + GetSize(t)/2);
912 std::vector<int> t1(t.begin() + GetSize(t)/2, t.end());
913
914 std::vector<int> u0(u.begin(), u.begin() + GetSize(u)/2);
915 std::vector<int> u1(u.begin() + GetSize(u)/2, u.end());
916
917 t = ez->vec_ite(a[i], t1, t0);
918 u = ez->vec_ite(undef_a[i], ez->vec_or(ez->vec_xor(t0, t1), ez->vec_or(u0, u1)), ez->vec_ite(a[i], u1, u0));
919 }
920
921 log_assert(GetSize(t) == 1);
922 log_assert(GetSize(u) == 1);
923 undefGating(y, t, u);
924 ez->assume(ez->vec_eq(importUndefSigSpec(cell->getPort(ID::Y), timestep), u));
925 }
926 else
927 {
928 std::vector<int> t = lut;
929 for (int i = GetSize(a)-1; i >= 0; i--)
930 {
931 std::vector<int> t0(t.begin(), t.begin() + GetSize(t)/2);
932 std::vector<int> t1(t.begin() + GetSize(t)/2, t.end());
933 t = ez->vec_ite(a[i], t1, t0);
934 }
935
936 log_assert(GetSize(t) == 1);
937 ez->assume(ez->vec_eq(y, t));
938 }
939 return true;
940 }
941
942 if (cell->type == ID($sop))
943 {
944 std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
945 int y = importDefSigSpec(cell->getPort(ID::Y), timestep).at(0);
946
947 int width = cell->getParam(ID::WIDTH).as_int();
948 int depth = cell->getParam(ID::DEPTH).as_int();
949
950 vector<State> table_raw = cell->getParam(ID::TABLE).bits;
951 while (GetSize(table_raw) < 2*width*depth)
952 table_raw.push_back(State::S0);
953
954 vector<vector<int>> table(depth);
955
956 for (int i = 0; i < depth; i++)
957 for (int j = 0; j < width; j++)
958 {
959 bool pat0 = (table_raw[2*width*i + 2*j + 0] == State::S1);
960 bool pat1 = (table_raw[2*width*i + 2*j + 1] == State::S1);
961
962 if (pat0 && !pat1)
963 table.at(i).push_back(0);
964 else if (!pat0 && pat1)
965 table.at(i).push_back(1);
966 else
967 table.at(i).push_back(-1);
968 }
969
970 if (model_undef)
971 {
972 std::vector<int> products, undef_products;
973 std::vector<int> undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
974 int undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep).at(0);
975
976 for (int i = 0; i < depth; i++)
977 {
978 std::vector<int> cmp_a, cmp_ua, cmp_b;
979
980 for (int j = 0; j < width; j++)
981 if (table.at(i).at(j) >= 0) {
982 cmp_a.push_back(a.at(j));
983 cmp_ua.push_back(undef_a.at(j));
984 cmp_b.push_back(table.at(i).at(j) ? ez->CONST_TRUE : ez->CONST_FALSE);
985 }
986
987 std::vector<int> masked_a = ez->vec_or(cmp_a, cmp_ua);
988 std::vector<int> masked_b = ez->vec_or(cmp_b, cmp_ua);
989
990 int masked_eq = ez->vec_eq(masked_a, masked_b);
991 int any_undef = ez->expression(ezSAT::OpOr, cmp_ua);
992
993 undef_products.push_back(ez->AND(any_undef, masked_eq));
994 products.push_back(ez->AND(ez->NOT(any_undef), masked_eq));
995 }
996
997 int yy = ez->expression(ezSAT::OpOr, products);
998 ez->SET(undef_y, ez->AND(ez->NOT(yy), ez->expression(ezSAT::OpOr, undef_products)));
999 undefGating(y, yy, undef_y);
1000 }
1001 else
1002 {
1003 std::vector<int> products;
1004
1005 for (int i = 0; i < depth; i++)
1006 {
1007 std::vector<int> cmp_a, cmp_b;
1008
1009 for (int j = 0; j < width; j++)
1010 if (table.at(i).at(j) >= 0) {
1011 cmp_a.push_back(a.at(j));
1012 cmp_b.push_back(table.at(i).at(j) ? ez->CONST_TRUE : ez->CONST_FALSE);
1013 }
1014
1015 products.push_back(ez->vec_eq(cmp_a, cmp_b));
1016 }
1017
1018 ez->SET(y, ez->expression(ezSAT::OpOr, products));
1019 }
1020
1021 return true;
1022 }
1023
1024 if (cell->type == ID($fa))
1025 {
1026 std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
1027 std::vector<int> b = importDefSigSpec(cell->getPort(ID::B), timestep);
1028 std::vector<int> c = importDefSigSpec(cell->getPort(ID::C), timestep);
1029 std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep);
1030 std::vector<int> x = importDefSigSpec(cell->getPort(ID::X), timestep);
1031
1032 std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
1033 std::vector<int> xx = model_undef ? ez->vec_var(x.size()) : x;
1034
1035 std::vector<int> t1 = ez->vec_xor(a, b);
1036 ez->assume(ez->vec_eq(yy, ez->vec_xor(t1, c)));
1037
1038 std::vector<int> t2 = ez->vec_and(a, b);
1039 std::vector<int> t3 = ez->vec_and(c, t1);
1040 ez->assume(ez->vec_eq(xx, ez->vec_or(t2, t3)));
1041
1042 if (model_undef)
1043 {
1044 std::vector<int> undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
1045 std::vector<int> undef_b = importUndefSigSpec(cell->getPort(ID::B), timestep);
1046 std::vector<int> undef_c = importUndefSigSpec(cell->getPort(ID::C), timestep);
1047
1048 std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
1049 std::vector<int> undef_x = importUndefSigSpec(cell->getPort(ID::X), timestep);
1050
1051 ez->assume(ez->vec_eq(undef_y, ez->vec_or(ez->vec_or(undef_a, undef_b), undef_c)));
1052 ez->assume(ez->vec_eq(undef_x, undef_y));
1053
1054 undefGating(y, yy, undef_y);
1055 undefGating(x, xx, undef_x);
1056 }
1057 return true;
1058 }
1059
1060 if (cell->type == ID($lcu))
1061 {
1062 std::vector<int> p = importDefSigSpec(cell->getPort(ID::P), timestep);
1063 std::vector<int> g = importDefSigSpec(cell->getPort(ID::G), timestep);
1064 std::vector<int> ci = importDefSigSpec(cell->getPort(ID::CI), timestep);
1065 std::vector<int> co = importDefSigSpec(cell->getPort(ID::CO), timestep);
1066
1067 std::vector<int> yy = model_undef ? ez->vec_var(co.size()) : co;
1068
1069 for (int i = 0; i < GetSize(co); i++)
1070 ez->SET(yy[i], ez->OR(g[i], ez->AND(p[i], i ? yy[i-1] : ci[0])));
1071
1072 if (model_undef)
1073 {
1074 std::vector<int> undef_p = importUndefSigSpec(cell->getPort(ID::P), timestep);
1075 std::vector<int> undef_g = importUndefSigSpec(cell->getPort(ID::G), timestep);
1076 std::vector<int> undef_ci = importUndefSigSpec(cell->getPort(ID::CI), timestep);
1077 std::vector<int> undef_co = importUndefSigSpec(cell->getPort(ID::CO), timestep);
1078
1079 int undef_any_p = ez->expression(ezSAT::OpOr, undef_p);
1080 int undef_any_g = ez->expression(ezSAT::OpOr, undef_g);
1081 int undef_any_ci = ez->expression(ezSAT::OpOr, undef_ci);
1082 int undef_co_bit = ez->OR(undef_any_p, undef_any_g, undef_any_ci);
1083
1084 std::vector<int> undef_co_bits(undef_co.size(), undef_co_bit);
1085 ez->assume(ez->vec_eq(undef_co_bits, undef_co));
1086
1087 undefGating(co, yy, undef_co);
1088 }
1089 return true;
1090 }
1091
1092 if (cell->type == ID($alu))
1093 {
1094 std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
1095 std::vector<int> b = importDefSigSpec(cell->getPort(ID::B), timestep);
1096 std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep);
1097 std::vector<int> x = importDefSigSpec(cell->getPort(ID::X), timestep);
1098 std::vector<int> ci = importDefSigSpec(cell->getPort(ID::CI), timestep);
1099 std::vector<int> bi = importDefSigSpec(cell->getPort(ID::BI), timestep);
1100 std::vector<int> co = importDefSigSpec(cell->getPort(ID::CO), timestep);
1101
1102 extendSignalWidth(a, b, y, cell);
1103 extendSignalWidth(a, b, x, cell);
1104 extendSignalWidth(a, b, co, cell);
1105
1106 std::vector<int> def_y = model_undef ? ez->vec_var(y.size()) : y;
1107 std::vector<int> def_x = model_undef ? ez->vec_var(x.size()) : x;
1108 std::vector<int> def_co = model_undef ? ez->vec_var(co.size()) : co;
1109
1110 log_assert(GetSize(y) == GetSize(x));
1111 log_assert(GetSize(y) == GetSize(co));
1112 log_assert(GetSize(ci) == 1);
1113 log_assert(GetSize(bi) == 1);
1114
1115 for (int i = 0; i < GetSize(y); i++)
1116 {
1117 int s1 = a.at(i), s2 = ez->XOR(b.at(i), bi.at(0)), s3 = i ? co.at(i-1) : ci.at(0);
1118 ez->SET(def_x.at(i), ez->XOR(s1, s2));
1119 ez->SET(def_y.at(i), ez->XOR(def_x.at(i), s3));
1120 ez->SET(def_co.at(i), ez->OR(ez->AND(s1, s2), ez->AND(s1, s3), ez->AND(s2, s3)));
1121 }
1122
1123 if (model_undef)
1124 {
1125 std::vector<int> undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
1126 std::vector<int> undef_b = importUndefSigSpec(cell->getPort(ID::B), timestep);
1127 std::vector<int> undef_ci = importUndefSigSpec(cell->getPort(ID::CI), timestep);
1128 std::vector<int> undef_bi = importUndefSigSpec(cell->getPort(ID::BI), timestep);
1129
1130 std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
1131 std::vector<int> undef_x = importUndefSigSpec(cell->getPort(ID::X), timestep);
1132 std::vector<int> undef_co = importUndefSigSpec(cell->getPort(ID::CO), timestep);
1133
1134 extendSignalWidth(undef_a, undef_b, undef_y, cell);
1135 extendSignalWidth(undef_a, undef_b, undef_x, cell);
1136 extendSignalWidth(undef_a, undef_b, undef_co, cell);
1137
1138 std::vector<int> all_inputs_undef;
1139 all_inputs_undef.insert(all_inputs_undef.end(), undef_a.begin(), undef_a.end());
1140 all_inputs_undef.insert(all_inputs_undef.end(), undef_b.begin(), undef_b.end());
1141 all_inputs_undef.insert(all_inputs_undef.end(), undef_ci.begin(), undef_ci.end());
1142 all_inputs_undef.insert(all_inputs_undef.end(), undef_bi.begin(), undef_bi.end());
1143 int undef_any = ez->expression(ezSAT::OpOr, all_inputs_undef);
1144
1145 for (int i = 0; i < GetSize(undef_y); i++) {
1146 ez->SET(undef_y.at(i), undef_any);
1147 ez->SET(undef_x.at(i), ez->OR(undef_a.at(i), undef_b.at(i), undef_bi.at(0)));
1148 ez->SET(undef_co.at(i), undef_any);
1149 }
1150
1151 undefGating(y, def_y, undef_y);
1152 undefGating(x, def_x, undef_x);
1153 undefGating(co, def_co, undef_co);
1154 }
1155 return true;
1156 }
1157
1158 if (cell->type == ID($slice))
1159 {
1160 RTLIL::SigSpec a = cell->getPort(ID::A);
1161 RTLIL::SigSpec y = cell->getPort(ID::Y);
1162 ez->assume(signals_eq(a.extract(cell->parameters.at(ID::OFFSET).as_int(), y.size()), y, timestep));
1163 return true;
1164 }
1165
1166 if (cell->type == ID($concat))
1167 {
1168 RTLIL::SigSpec a = cell->getPort(ID::A);
1169 RTLIL::SigSpec b = cell->getPort(ID::B);
1170 RTLIL::SigSpec y = cell->getPort(ID::Y);
1171
1172 RTLIL::SigSpec ab = a;
1173 ab.append(b);
1174
1175 ez->assume(signals_eq(ab, y, timestep));
1176 return true;
1177 }
1178
1179 if (timestep > 0 && RTLIL::builtin_ff_cell_types().count(cell->type))
1180 {
1181 FfData ff(nullptr, cell);
1182
1183 // Latches and FFs with async inputs are not supported — use clk2fflogic or async2sync first.
1184 if (ff.has_aload || ff.has_arst || ff.has_sr)
1185 return false;
1186
1187 if (timestep == 1)
1188 {
1189 initial_state.add((*sigmap)(cell->getPort(ID::Q)));
1190 }
1191 else
1192 {
1193 std::vector<int> d = importDefSigSpec(cell->getPort(ID::D), timestep-1);
1194 std::vector<int> undef_d;
1195 if (model_undef)
1196 undef_d = importUndefSigSpec(cell->getPort(ID::D), timestep-1);
1197 if (ff.has_srst && ff.has_ce && ff.ce_over_srst) {
1198 int srst = importDefSigSpec(ff.sig_srst, timestep-1).at(0);
1199 std::vector<int> rval = importDefSigSpec(ff.val_srst, timestep-1);
1200 int undef_srst;
1201 std::vector<int> undef_rval;
1202 if (model_undef) {
1203 undef_srst = importUndefSigSpec(ff.sig_srst, timestep-1).at(0);
1204 undef_rval = importUndefSigSpec(ff.val_srst, timestep-1);
1205 }
1206 if (ff.pol_srst)
1207 std::tie(d, undef_d) = mux(srst, undef_srst, d, undef_d, rval, undef_rval);
1208 else
1209 std::tie(d, undef_d) = mux(srst, undef_srst, rval, undef_rval, d, undef_d);
1210 }
1211 if (ff.has_ce) {
1212 int ce = importDefSigSpec(ff.sig_ce, timestep-1).at(0);
1213 std::vector<int> old_q = importDefSigSpec(ff.sig_q, timestep-1);
1214 int undef_ce;
1215 std::vector<int> undef_old_q;
1216 if (model_undef) {
1217 undef_ce = importUndefSigSpec(ff.sig_ce, timestep-1).at(0);
1218 undef_old_q = importUndefSigSpec(ff.sig_q, timestep-1);
1219 }
1220 if (ff.pol_ce)
1221 std::tie(d, undef_d) = mux(ce, undef_ce, old_q, undef_old_q, d, undef_d);
1222 else
1223 std::tie(d, undef_d) = mux(ce, undef_ce, d, undef_d, old_q, undef_old_q);
1224 }
1225 if (ff.has_srst && !(ff.has_ce && ff.ce_over_srst)) {
1226 int srst = importDefSigSpec(ff.sig_srst, timestep-1).at(0);
1227 std::vector<int> rval = importDefSigSpec(ff.val_srst, timestep-1);
1228 int undef_srst;
1229 std::vector<int> undef_rval;
1230 if (model_undef) {
1231 undef_srst = importUndefSigSpec(ff.sig_srst, timestep-1).at(0);
1232 undef_rval = importUndefSigSpec(ff.val_srst, timestep-1);
1233 }
1234 if (ff.pol_srst)
1235 std::tie(d, undef_d) = mux(srst, undef_srst, d, undef_d, rval, undef_rval);
1236 else
1237 std::tie(d, undef_d) = mux(srst, undef_srst, rval, undef_rval, d, undef_d);
1238 }
1239 std::vector<int> q = importDefSigSpec(cell->getPort(ID::Q), timestep);
1240
1241 std::vector<int> qq = model_undef ? ez->vec_var(q.size()) : q;
1242 ez->assume(ez->vec_eq(d, qq));
1243
1244 if (model_undef)
1245 {
1246 std::vector<int> undef_q = importUndefSigSpec(cell->getPort(ID::Q), timestep);
1247
1248 ez->assume(ez->vec_eq(undef_d, undef_q));
1249 undefGating(q, qq, undef_q);
1250 }
1251 }
1252 return true;
1253 }
1254
1255 if (cell->type == ID($anyconst))
1256 {
1257 if (timestep < 2)
1258 return true;
1259
1260 std::vector<int> d = importDefSigSpec(cell->getPort(ID::Y), timestep-1);
1261 std::vector<int> q = importDefSigSpec(cell->getPort(ID::Y), timestep);
1262
1263 std::vector<int> qq = model_undef ? ez->vec_var(q.size()) : q;
1264 ez->assume(ez->vec_eq(d, qq));
1265
1266 if (model_undef)
1267 {
1268 std::vector<int> undef_d = importUndefSigSpec(cell->getPort(ID::Y), timestep-1);
1269 std::vector<int> undef_q = importUndefSigSpec(cell->getPort(ID::Y), timestep);
1270
1271 ez->assume(ez->vec_eq(undef_d, undef_q));
1272 undefGating(q, qq, undef_q);
1273 }
1274 return true;
1275 }
1276
1277 if (cell->type == ID($anyseq))
1278 {
1279 return true;
1280 }
1281
1282 if (cell->type.in(ID($_BUF_), ID($equiv)))
1283 {
1284 std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
1285 std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep);
1286 extendSignalWidthUnary(a, y, cell);
1287
1288 std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
1289 ez->assume(ez->vec_eq(a, yy));
1290
1291 if (model_undef) {
1292 std::vector<int> undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
1293 std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
1294 extendSignalWidthUnary(undef_a, undef_y, cell, false);
1295 ez->assume(ez->vec_eq(undef_a, undef_y));
1296 undefGating(y, yy, undef_y);
1297 }
1298 return true;
1299 }
1300
1301 if (cell->type == ID($initstate))
1302 {
1303 auto key = make_pair(prefix, timestep);
1304 if (initstates.count(key) == 0)
1305 initstates[key] = false;
1306
1307 std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep);
1308 log_assert(GetSize(y) == 1);
1309 ez->SET(y[0], initstates[key] ? ez->CONST_TRUE : ez->CONST_FALSE);
1310
1311 if (model_undef) {
1312 std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
1313 log_assert(GetSize(undef_y) == 1);
1314 ez->SET(undef_y[0], ez->CONST_FALSE);
1315 }
1316
1317 return true;
1318 }
1319
1320 if (cell->type == ID($assert))
1321 {
1322 std::string pf = prefix + (timestep == -1 ? "" : stringf("@%d:", timestep));
1323 asserts_a[pf].append((*sigmap)(cell->getPort(ID::A)));
1324 asserts_en[pf].append((*sigmap)(cell->getPort(ID::EN)));
1325 return true;
1326 }
1327
1328 if (cell->type == ID($assume))
1329 {
1330 std::string pf = prefix + (timestep == -1 ? "" : stringf("@%d:", timestep));
1331 assumes_a[pf].append((*sigmap)(cell->getPort(ID::A)));
1332 assumes_en[pf].append((*sigmap)(cell->getPort(ID::EN)));
1333 return true;
1334 }
1335
1336 // Unsupported internal cell types: $pow $fsm $mem*
1337 // .. and all sequential cells with asynchronous inputs
1338 return false;
1339 }