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