2 * yosys -- Yosys Open SYnthesis Suite
4 * Copyright (C) 2012 Clifford Wolf <clifford@clifford.at>
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.
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.
23 #include "kernel/rtlil.h"
24 #include "kernel/sigtools.h"
25 #include "kernel/celltypes.h"
26 #include "kernel/macc.h"
28 #include "libs/ezsat/ezminisat.h"
32 // defined in kernel/register.cc
33 extern struct SatSolver
*yosys_satsolver_list
;
34 extern struct SatSolver
*yosys_satsolver
;
40 virtual ezSAT
*create() = 0;
42 SatSolver(string name
) : name(name
) {
43 next
= yosys_satsolver_list
;
44 yosys_satsolver_list
= this;
47 virtual ~SatSolver() {
48 auto p
= &yosys_satsolver_list
;
55 if (yosys_satsolver
== this)
56 yosys_satsolver
= yosys_satsolver_list
;
60 struct ezSatPtr
: public std::unique_ptr
<ezSAT
> {
61 ezSatPtr() : unique_ptr
<ezSAT
>(yosys_satsolver
->create()) { }
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 std::map
<std::pair
<std::string
, int>, bool> initstates
;
74 bool ignore_div_by_zero
;
77 SatGen(ezSAT
*ez
, SigMap
*sigmap
, std::string prefix
= std::string()) :
78 ez(ez
), sigmap(sigmap
), prefix(prefix
), ignore_div_by_zero(false), model_undef(false)
82 void setContext(SigMap
*sigmap
, std::string prefix
= std::string())
84 this->sigmap
= sigmap
;
85 this->prefix
= prefix
;
88 std::vector
<int> importSigSpecWorker(RTLIL::SigSpec sig
, std::string
&pf
, bool undef_mode
, bool dup_undef
)
90 log_assert(!undef_mode
|| model_undef
);
94 vec
.reserve(GetSize(sig
));
97 if (bit
.wire
== NULL
) {
98 if (model_undef
&& dup_undef
&& bit
== RTLIL::State::Sx
)
99 vec
.push_back(ez
->frozen_literal());
101 vec
.push_back(bit
== (undef_mode
? RTLIL::State::Sx
: RTLIL::State::S1
) ? ez
->CONST_TRUE
: ez
->CONST_FALSE
);
103 std::string name
= pf
+ (bit
.wire
->width
== 1 ? stringf("%s", log_id(bit
.wire
)) : stringf("%s [%d]", log_id(bit
.wire
->name
), bit
.offset
));
104 vec
.push_back(ez
->frozen_literal(name
));
105 imported_signals
[pf
][bit
] = vec
.back();
110 std::vector
<int> importSigSpec(RTLIL::SigSpec sig
, int timestep
= -1)
112 log_assert(timestep
!= 0);
113 std::string pf
= prefix
+ (timestep
== -1 ? "" : stringf("@%d:", timestep
));
114 return importSigSpecWorker(sig
, pf
, false, false);
117 std::vector
<int> importDefSigSpec(RTLIL::SigSpec sig
, int timestep
= -1)
119 log_assert(timestep
!= 0);
120 std::string pf
= prefix
+ (timestep
== -1 ? "" : stringf("@%d:", timestep
));
121 return importSigSpecWorker(sig
, pf
, false, true);
124 std::vector
<int> importUndefSigSpec(RTLIL::SigSpec sig
, int timestep
= -1)
126 log_assert(timestep
!= 0);
127 std::string pf
= "undef:" + prefix
+ (timestep
== -1 ? "" : stringf("@%d:", timestep
));
128 return importSigSpecWorker(sig
, pf
, true, false);
131 int importSigBit(RTLIL::SigBit bit
, int timestep
= -1)
133 log_assert(timestep
!= 0);
134 std::string pf
= prefix
+ (timestep
== -1 ? "" : stringf("@%d:", timestep
));
135 return importSigSpecWorker(bit
, pf
, false, false).front();
138 int importDefSigBit(RTLIL::SigBit bit
, int timestep
= -1)
140 log_assert(timestep
!= 0);
141 std::string pf
= prefix
+ (timestep
== -1 ? "" : stringf("@%d:", timestep
));
142 return importSigSpecWorker(bit
, pf
, false, true).front();
145 int importUndefSigBit(RTLIL::SigBit bit
, int timestep
= -1)
147 log_assert(timestep
!= 0);
148 std::string pf
= "undef:" + prefix
+ (timestep
== -1 ? "" : stringf("@%d:", timestep
));
149 return importSigSpecWorker(bit
, pf
, true, false).front();
152 bool importedSigBit(RTLIL::SigBit bit
, int timestep
= -1)
154 log_assert(timestep
!= 0);
155 std::string pf
= prefix
+ (timestep
== -1 ? "" : stringf("@%d:", timestep
));
156 return imported_signals
[pf
].count(bit
) != 0;
159 void getAsserts(RTLIL::SigSpec
&sig_a
, RTLIL::SigSpec
&sig_en
, int timestep
= -1)
161 std::string pf
= prefix
+ (timestep
== -1 ? "" : stringf("@%d:", timestep
));
162 sig_a
= asserts_a
[pf
];
163 sig_en
= asserts_en
[pf
];
166 void getAssumes(RTLIL::SigSpec
&sig_a
, RTLIL::SigSpec
&sig_en
, int timestep
= -1)
168 std::string pf
= prefix
+ (timestep
== -1 ? "" : stringf("@%d:", timestep
));
169 sig_a
= assumes_a
[pf
];
170 sig_en
= assumes_en
[pf
];
173 int importAsserts(int timestep
= -1)
175 std::vector
<int> check_bits
, enable_bits
;
176 std::string pf
= prefix
+ (timestep
== -1 ? "" : stringf("@%d:", timestep
));
178 check_bits
= ez
->vec_and(ez
->vec_not(importUndefSigSpec(asserts_a
[pf
], timestep
)), importDefSigSpec(asserts_a
[pf
], timestep
));
179 enable_bits
= ez
->vec_and(ez
->vec_not(importUndefSigSpec(asserts_en
[pf
], timestep
)), importDefSigSpec(asserts_en
[pf
], timestep
));
181 check_bits
= importDefSigSpec(asserts_a
[pf
], timestep
);
182 enable_bits
= importDefSigSpec(asserts_en
[pf
], timestep
);
184 return ez
->vec_reduce_and(ez
->vec_or(check_bits
, ez
->vec_not(enable_bits
)));
187 int importAssumes(int timestep
= -1)
189 std::vector
<int> check_bits
, enable_bits
;
190 std::string pf
= prefix
+ (timestep
== -1 ? "" : stringf("@%d:", timestep
));
192 check_bits
= ez
->vec_and(ez
->vec_not(importUndefSigSpec(assumes_a
[pf
], timestep
)), importDefSigSpec(assumes_a
[pf
], timestep
));
193 enable_bits
= ez
->vec_and(ez
->vec_not(importUndefSigSpec(assumes_en
[pf
], timestep
)), importDefSigSpec(assumes_en
[pf
], timestep
));
195 check_bits
= importDefSigSpec(assumes_a
[pf
], timestep
);
196 enable_bits
= importDefSigSpec(assumes_en
[pf
], timestep
);
198 return ez
->vec_reduce_and(ez
->vec_or(check_bits
, ez
->vec_not(enable_bits
)));
201 int signals_eq(RTLIL::SigSpec lhs
, RTLIL::SigSpec rhs
, int timestep_lhs
= -1, int timestep_rhs
= -1)
203 if (timestep_rhs
< 0)
204 timestep_rhs
= timestep_lhs
;
206 log_assert(lhs
.size() == rhs
.size());
208 std::vector
<int> vec_lhs
= importSigSpec(lhs
, timestep_lhs
);
209 std::vector
<int> vec_rhs
= importSigSpec(rhs
, timestep_rhs
);
212 return ez
->vec_eq(vec_lhs
, vec_rhs
);
214 std::vector
<int> undef_lhs
= importUndefSigSpec(lhs
, timestep_lhs
);
215 std::vector
<int> undef_rhs
= importUndefSigSpec(rhs
, timestep_rhs
);
217 std::vector
<int> eq_bits
;
218 for (int i
= 0; i
< lhs
.size(); i
++)
219 eq_bits
.push_back(ez
->AND(ez
->IFF(undef_lhs
.at(i
), undef_rhs
.at(i
)),
220 ez
->IFF(ez
->OR(vec_lhs
.at(i
), undef_lhs
.at(i
)), ez
->OR(vec_rhs
.at(i
), undef_rhs
.at(i
)))));
221 return ez
->expression(ezSAT::OpAnd
, eq_bits
);
224 void extendSignalWidth(std::vector
<int> &vec_a
, std::vector
<int> &vec_b
, RTLIL::Cell
*cell
, size_t y_width
= 0, bool forced_signed
= false)
226 bool is_signed
= forced_signed
;
227 if (!forced_signed
&& cell
->parameters
.count("\\A_SIGNED") > 0 && cell
->parameters
.count("\\B_SIGNED") > 0)
228 is_signed
= cell
->parameters
["\\A_SIGNED"].as_bool() && cell
->parameters
["\\B_SIGNED"].as_bool();
229 while (vec_a
.size() < vec_b
.size() || vec_a
.size() < y_width
)
230 vec_a
.push_back(is_signed
&& vec_a
.size() > 0 ? vec_a
.back() : ez
->CONST_FALSE
);
231 while (vec_b
.size() < vec_a
.size() || vec_b
.size() < y_width
)
232 vec_b
.push_back(is_signed
&& vec_b
.size() > 0 ? vec_b
.back() : ez
->CONST_FALSE
);
235 void extendSignalWidth(std::vector
<int> &vec_a
, std::vector
<int> &vec_b
, std::vector
<int> &vec_y
, RTLIL::Cell
*cell
, bool forced_signed
= false)
237 extendSignalWidth(vec_a
, vec_b
, cell
, vec_y
.size(), forced_signed
);
238 while (vec_y
.size() < vec_a
.size())
239 vec_y
.push_back(ez
->literal());
242 void extendSignalWidthUnary(std::vector
<int> &vec_a
, std::vector
<int> &vec_y
, RTLIL::Cell
*cell
, bool forced_signed
= false)
244 bool is_signed
= forced_signed
|| (cell
->parameters
.count("\\A_SIGNED") > 0 && cell
->parameters
["\\A_SIGNED"].as_bool());
245 while (vec_a
.size() < vec_y
.size())
246 vec_a
.push_back(is_signed
&& vec_a
.size() > 0 ? vec_a
.back() : ez
->CONST_FALSE
);
247 while (vec_y
.size() < vec_a
.size())
248 vec_y
.push_back(ez
->literal());
251 void undefGating(std::vector
<int> &vec_y
, std::vector
<int> &vec_yy
, std::vector
<int> &vec_undef
)
253 log_assert(model_undef
);
254 log_assert(vec_y
.size() == vec_yy
.size());
255 if (vec_y
.size() > vec_undef
.size()) {
256 std::vector
<int> trunc_y(vec_y
.begin(), vec_y
.begin() + vec_undef
.size());
257 std::vector
<int> trunc_yy(vec_yy
.begin(), vec_yy
.begin() + vec_undef
.size());
258 ez
->assume(ez
->expression(ezSAT::OpAnd
, ez
->vec_or(vec_undef
, ez
->vec_iff(trunc_y
, trunc_yy
))));
260 log_assert(vec_y
.size() == vec_undef
.size());
261 ez
->assume(ez
->expression(ezSAT::OpAnd
, ez
->vec_or(vec_undef
, ez
->vec_iff(vec_y
, vec_yy
))));
265 void undefGating(int y
, int yy
, int undef
)
267 ez
->assume(ez
->OR(undef
, ez
->IFF(y
, yy
)));
270 void setInitState(int timestep
)
272 auto key
= make_pair(prefix
, timestep
);
273 log_assert(initstates
.count(key
) == 0 || initstates
.at(key
) == true);
274 initstates
[key
] = true;
277 bool importCell(RTLIL::Cell
*cell
, int timestep
= -1)
279 bool arith_undef_handled
= false;
280 bool is_arith_compare
= cell
->type
.in("$lt", "$le", "$ge", "$gt");
282 if (model_undef
&& (cell
->type
.in("$add", "$sub", "$mul", "$div", "$mod") || is_arith_compare
))
284 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
285 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort("\\B"), timestep
);
286 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
287 if (is_arith_compare
)
288 extendSignalWidth(undef_a
, undef_b
, cell
, true);
290 extendSignalWidth(undef_a
, undef_b
, undef_y
, cell
, true);
292 int undef_any_a
= ez
->expression(ezSAT::OpOr
, undef_a
);
293 int undef_any_b
= ez
->expression(ezSAT::OpOr
, undef_b
);
294 int undef_y_bit
= ez
->OR(undef_any_a
, undef_any_b
);
296 if (cell
->type
== "$div" || cell
->type
== "$mod") {
297 std::vector
<int> b
= importSigSpec(cell
->getPort("\\B"), timestep
);
298 undef_y_bit
= ez
->OR(undef_y_bit
, ez
->NOT(ez
->expression(ezSAT::OpOr
, b
)));
301 if (is_arith_compare
) {
302 for (size_t i
= 1; i
< undef_y
.size(); i
++)
303 ez
->SET(ez
->CONST_FALSE
, undef_y
.at(i
));
304 ez
->SET(undef_y_bit
, undef_y
.at(0));
306 std::vector
<int> undef_y_bits(undef_y
.size(), undef_y_bit
);
307 ez
->assume(ez
->vec_eq(undef_y_bits
, undef_y
));
310 arith_undef_handled
= true;
313 if (cell
->type
.in("$_AND_", "$_NAND_", "$_OR_", "$_NOR_", "$_XOR_", "$_XNOR_",
314 "$and", "$or", "$xor", "$xnor", "$add", "$sub"))
316 std::vector
<int> a
= importDefSigSpec(cell
->getPort("\\A"), timestep
);
317 std::vector
<int> b
= importDefSigSpec(cell
->getPort("\\B"), timestep
);
318 std::vector
<int> y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
319 extendSignalWidth(a
, b
, y
, cell
);
321 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
323 if (cell
->type
== "$and" || cell
->type
== "$_AND_")
324 ez
->assume(ez
->vec_eq(ez
->vec_and(a
, b
), yy
));
325 if (cell
->type
== "$_NAND_")
326 ez
->assume(ez
->vec_eq(ez
->vec_not(ez
->vec_and(a
, b
)), yy
));
327 if (cell
->type
== "$or" || cell
->type
== "$_OR_")
328 ez
->assume(ez
->vec_eq(ez
->vec_or(a
, b
), yy
));
329 if (cell
->type
== "$_NOR_")
330 ez
->assume(ez
->vec_eq(ez
->vec_not(ez
->vec_or(a
, b
)), yy
));
331 if (cell
->type
== "$xor" || cell
->type
== "$_XOR_")
332 ez
->assume(ez
->vec_eq(ez
->vec_xor(a
, b
), yy
));
333 if (cell
->type
== "$xnor" || cell
->type
== "$_XNOR_")
334 ez
->assume(ez
->vec_eq(ez
->vec_not(ez
->vec_xor(a
, b
)), yy
));
335 if (cell
->type
== "$add")
336 ez
->assume(ez
->vec_eq(ez
->vec_add(a
, b
), yy
));
337 if (cell
->type
== "$sub")
338 ez
->assume(ez
->vec_eq(ez
->vec_sub(a
, b
), yy
));
340 if (model_undef
&& !arith_undef_handled
)
342 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
343 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort("\\B"), timestep
);
344 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
345 extendSignalWidth(undef_a
, undef_b
, undef_y
, cell
, false);
347 if (cell
->type
.in("$and", "$_AND_", "$_NAND_")) {
348 std::vector
<int> a0
= ez
->vec_and(ez
->vec_not(a
), ez
->vec_not(undef_a
));
349 std::vector
<int> b0
= ez
->vec_and(ez
->vec_not(b
), ez
->vec_not(undef_b
));
350 std::vector
<int> yX
= ez
->vec_and(ez
->vec_or(undef_a
, undef_b
), ez
->vec_not(ez
->vec_or(a0
, b0
)));
351 ez
->assume(ez
->vec_eq(yX
, undef_y
));
353 else if (cell
->type
.in("$or", "$_OR_", "$_NOR_")) {
354 std::vector
<int> a1
= ez
->vec_and(a
, ez
->vec_not(undef_a
));
355 std::vector
<int> b1
= ez
->vec_and(b
, ez
->vec_not(undef_b
));
356 std::vector
<int> yX
= ez
->vec_and(ez
->vec_or(undef_a
, undef_b
), ez
->vec_not(ez
->vec_or(a1
, b1
)));
357 ez
->assume(ez
->vec_eq(yX
, undef_y
));
359 else if (cell
->type
.in("$xor", "$xnor", "$_XOR_", "$_XNOR_")) {
360 std::vector
<int> yX
= ez
->vec_or(undef_a
, undef_b
);
361 ez
->assume(ez
->vec_eq(yX
, undef_y
));
366 undefGating(y
, yy
, undef_y
);
368 else if (model_undef
)
370 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
371 undefGating(y
, yy
, undef_y
);
376 if (cell
->type
.in("$_AOI3_", "$_OAI3_", "$_AOI4_", "$_OAI4_"))
378 bool aoi_mode
= cell
->type
.in("$_AOI3_", "$_AOI4_");
379 bool three_mode
= cell
->type
.in("$_AOI3_", "$_OAI3_");
381 int a
= importDefSigSpec(cell
->getPort("\\A"), timestep
).at(0);
382 int b
= importDefSigSpec(cell
->getPort("\\B"), timestep
).at(0);
383 int c
= importDefSigSpec(cell
->getPort("\\C"), timestep
).at(0);
384 int d
= three_mode
? (aoi_mode
? ez
->CONST_TRUE
: ez
->CONST_FALSE
) : importDefSigSpec(cell
->getPort("\\D"), timestep
).at(0);
385 int y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
).at(0);
386 int yy
= model_undef
? ez
->literal() : y
;
388 if (cell
->type
.in("$_AOI3_", "$_AOI4_"))
389 ez
->assume(ez
->IFF(ez
->NOT(ez
->OR(ez
->AND(a
, b
), ez
->AND(c
, d
))), yy
));
391 ez
->assume(ez
->IFF(ez
->NOT(ez
->AND(ez
->OR(a
, b
), ez
->OR(c
, d
))), yy
));
395 int undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
).at(0);
396 int undef_b
= importUndefSigSpec(cell
->getPort("\\B"), timestep
).at(0);
397 int undef_c
= importUndefSigSpec(cell
->getPort("\\C"), timestep
).at(0);
398 int undef_d
= three_mode
? ez
->CONST_FALSE
: importUndefSigSpec(cell
->getPort("\\D"), timestep
).at(0);
399 int undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
).at(0);
403 int a0
= ez
->AND(ez
->NOT(a
), ez
->NOT(undef_a
));
404 int b0
= ez
->AND(ez
->NOT(b
), ez
->NOT(undef_b
));
405 int c0
= ez
->AND(ez
->NOT(c
), ez
->NOT(undef_c
));
406 int d0
= ez
->AND(ez
->NOT(d
), ez
->NOT(undef_d
));
408 int ab
= ez
->AND(a
, b
), cd
= ez
->AND(c
, d
);
409 int undef_ab
= ez
->AND(ez
->OR(undef_a
, undef_b
), ez
->NOT(ez
->OR(a0
, b0
)));
410 int undef_cd
= ez
->AND(ez
->OR(undef_c
, undef_d
), ez
->NOT(ez
->OR(c0
, d0
)));
412 int ab1
= ez
->AND(ab
, ez
->NOT(undef_ab
));
413 int cd1
= ez
->AND(cd
, ez
->NOT(undef_cd
));
414 int yX
= ez
->AND(ez
->OR(undef_ab
, undef_cd
), ez
->NOT(ez
->OR(ab1
, cd1
)));
416 ez
->assume(ez
->IFF(yX
, undef_y
));
420 int a1
= ez
->AND(a
, ez
->NOT(undef_a
));
421 int b1
= ez
->AND(b
, ez
->NOT(undef_b
));
422 int c1
= ez
->AND(c
, ez
->NOT(undef_c
));
423 int d1
= ez
->AND(d
, ez
->NOT(undef_d
));
425 int ab
= ez
->OR(a
, b
), cd
= ez
->OR(c
, d
);
426 int undef_ab
= ez
->AND(ez
->OR(undef_a
, undef_b
), ez
->NOT(ez
->OR(a1
, b1
)));
427 int undef_cd
= ez
->AND(ez
->OR(undef_c
, undef_d
), ez
->NOT(ez
->OR(c1
, d1
)));
429 int ab0
= ez
->AND(ez
->NOT(ab
), ez
->NOT(undef_ab
));
430 int cd0
= ez
->AND(ez
->NOT(cd
), ez
->NOT(undef_cd
));
431 int yX
= ez
->AND(ez
->OR(undef_ab
, undef_cd
), ez
->NOT(ez
->OR(ab0
, cd0
)));
433 ez
->assume(ez
->IFF(yX
, undef_y
));
436 undefGating(y
, yy
, undef_y
);
442 if (cell
->type
== "$_NOT_" || cell
->type
== "$not")
444 std::vector
<int> a
= importDefSigSpec(cell
->getPort("\\A"), timestep
);
445 std::vector
<int> y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
446 extendSignalWidthUnary(a
, y
, cell
);
448 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
449 ez
->assume(ez
->vec_eq(ez
->vec_not(a
), yy
));
452 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
453 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
454 extendSignalWidthUnary(undef_a
, undef_y
, cell
, false);
455 ez
->assume(ez
->vec_eq(undef_a
, undef_y
));
456 undefGating(y
, yy
, undef_y
);
461 if (cell
->type
== "$_MUX_" || cell
->type
== "$mux")
463 std::vector
<int> a
= importDefSigSpec(cell
->getPort("\\A"), timestep
);
464 std::vector
<int> b
= importDefSigSpec(cell
->getPort("\\B"), timestep
);
465 std::vector
<int> s
= importDefSigSpec(cell
->getPort("\\S"), timestep
);
466 std::vector
<int> y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
468 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
469 ez
->assume(ez
->vec_eq(ez
->vec_ite(s
.at(0), b
, a
), yy
));
473 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
474 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort("\\B"), timestep
);
475 std::vector
<int> undef_s
= importUndefSigSpec(cell
->getPort("\\S"), timestep
);
476 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
478 std::vector
<int> unequal_ab
= ez
->vec_not(ez
->vec_iff(a
, b
));
479 std::vector
<int> undef_ab
= ez
->vec_or(unequal_ab
, ez
->vec_or(undef_a
, undef_b
));
480 std::vector
<int> yX
= ez
->vec_ite(undef_s
.at(0), undef_ab
, ez
->vec_ite(s
.at(0), undef_b
, undef_a
));
481 ez
->assume(ez
->vec_eq(yX
, undef_y
));
482 undefGating(y
, yy
, undef_y
);
487 if (cell
->type
== "$pmux")
489 std::vector
<int> a
= importDefSigSpec(cell
->getPort("\\A"), timestep
);
490 std::vector
<int> b
= importDefSigSpec(cell
->getPort("\\B"), timestep
);
491 std::vector
<int> s
= importDefSigSpec(cell
->getPort("\\S"), timestep
);
492 std::vector
<int> y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
494 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
496 std::vector
<int> tmp
= a
;
497 for (size_t i
= 0; i
< s
.size(); i
++) {
498 std::vector
<int> part_of_b(b
.begin()+i
*a
.size(), b
.begin()+(i
+1)*a
.size());
499 tmp
= ez
->vec_ite(s
.at(i
), part_of_b
, tmp
);
501 ez
->assume(ez
->vec_eq(tmp
, yy
));
505 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
506 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort("\\B"), timestep
);
507 std::vector
<int> undef_s
= importUndefSigSpec(cell
->getPort("\\S"), timestep
);
508 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
510 int maybe_a
= ez
->CONST_TRUE
;
512 std::vector
<int> bits_set
= std::vector
<int>(undef_y
.size(), ez
->CONST_FALSE
);
513 std::vector
<int> bits_clr
= std::vector
<int>(undef_y
.size(), ez
->CONST_FALSE
);
515 for (size_t i
= 0; i
< s
.size(); i
++)
517 std::vector
<int> part_of_b(b
.begin()+i
*a
.size(), b
.begin()+(i
+1)*a
.size());
518 std::vector
<int> part_of_undef_b(undef_b
.begin()+i
*a
.size(), undef_b
.begin()+(i
+1)*a
.size());
520 int maybe_s
= ez
->OR(s
.at(i
), undef_s
.at(i
));
521 int sure_s
= ez
->AND(s
.at(i
), ez
->NOT(undef_s
.at(i
)));
523 maybe_a
= ez
->AND(maybe_a
, ez
->NOT(sure_s
));
525 bits_set
= ez
->vec_ite(maybe_s
, 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(ez
->vec_not(part_of_b
), part_of_undef_b
)), bits_clr
);
529 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
);
530 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
);
532 ez
->assume(ez
->vec_eq(ez
->vec_not(ez
->vec_xor(bits_set
, bits_clr
)), undef_y
));
533 undefGating(y
, yy
, undef_y
);
538 if (cell
->type
== "$pos" || cell
->type
== "$neg")
540 std::vector
<int> a
= importDefSigSpec(cell
->getPort("\\A"), timestep
);
541 std::vector
<int> y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
542 extendSignalWidthUnary(a
, y
, cell
);
544 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
546 if (cell
->type
== "$pos") {
547 ez
->assume(ez
->vec_eq(a
, yy
));
549 std::vector
<int> zero(a
.size(), ez
->CONST_FALSE
);
550 ez
->assume(ez
->vec_eq(ez
->vec_sub(zero
, a
), yy
));
555 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
556 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
557 extendSignalWidthUnary(undef_a
, undef_y
, cell
);
559 if (cell
->type
== "$pos") {
560 ez
->assume(ez
->vec_eq(undef_a
, undef_y
));
562 int undef_any_a
= ez
->expression(ezSAT::OpOr
, undef_a
);
563 std::vector
<int> undef_y_bits(undef_y
.size(), undef_any_a
);
564 ez
->assume(ez
->vec_eq(undef_y_bits
, undef_y
));
567 undefGating(y
, yy
, undef_y
);
572 if (cell
->type
== "$reduce_and" || cell
->type
== "$reduce_or" || cell
->type
== "$reduce_xor" ||
573 cell
->type
== "$reduce_xnor" || cell
->type
== "$reduce_bool" || cell
->type
== "$logic_not")
575 std::vector
<int> a
= importDefSigSpec(cell
->getPort("\\A"), timestep
);
576 std::vector
<int> y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
578 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
580 if (cell
->type
== "$reduce_and")
581 ez
->SET(ez
->expression(ez
->OpAnd
, a
), yy
.at(0));
582 if (cell
->type
== "$reduce_or" || cell
->type
== "$reduce_bool")
583 ez
->SET(ez
->expression(ez
->OpOr
, a
), yy
.at(0));
584 if (cell
->type
== "$reduce_xor")
585 ez
->SET(ez
->expression(ez
->OpXor
, a
), yy
.at(0));
586 if (cell
->type
== "$reduce_xnor")
587 ez
->SET(ez
->NOT(ez
->expression(ez
->OpXor
, a
)), yy
.at(0));
588 if (cell
->type
== "$logic_not")
589 ez
->SET(ez
->NOT(ez
->expression(ez
->OpOr
, a
)), yy
.at(0));
590 for (size_t i
= 1; i
< y
.size(); i
++)
591 ez
->SET(ez
->CONST_FALSE
, yy
.at(i
));
595 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
596 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
597 int aX
= ez
->expression(ezSAT::OpOr
, undef_a
);
599 if (cell
->type
== "$reduce_and") {
600 int a0
= ez
->expression(ezSAT::OpOr
, ez
->vec_and(ez
->vec_not(a
), ez
->vec_not(undef_a
)));
601 ez
->assume(ez
->IFF(ez
->AND(ez
->NOT(a0
), aX
), undef_y
.at(0)));
603 else if (cell
->type
== "$reduce_or" || cell
->type
== "$reduce_bool" || cell
->type
== "$logic_not") {
604 int a1
= ez
->expression(ezSAT::OpOr
, ez
->vec_and(a
, ez
->vec_not(undef_a
)));
605 ez
->assume(ez
->IFF(ez
->AND(ez
->NOT(a1
), aX
), undef_y
.at(0)));
607 else if (cell
->type
== "$reduce_xor" || cell
->type
== "$reduce_xnor") {
608 ez
->assume(ez
->IFF(aX
, undef_y
.at(0)));
612 for (size_t i
= 1; i
< undef_y
.size(); i
++)
613 ez
->SET(ez
->CONST_FALSE
, undef_y
.at(i
));
615 undefGating(y
, yy
, undef_y
);
620 if (cell
->type
== "$logic_and" || cell
->type
== "$logic_or")
622 std::vector
<int> vec_a
= importDefSigSpec(cell
->getPort("\\A"), timestep
);
623 std::vector
<int> vec_b
= importDefSigSpec(cell
->getPort("\\B"), timestep
);
625 int a
= ez
->expression(ez
->OpOr
, vec_a
);
626 int b
= ez
->expression(ez
->OpOr
, vec_b
);
627 std::vector
<int> y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
629 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
631 if (cell
->type
== "$logic_and")
632 ez
->SET(ez
->expression(ez
->OpAnd
, a
, b
), yy
.at(0));
634 ez
->SET(ez
->expression(ez
->OpOr
, a
, b
), yy
.at(0));
635 for (size_t i
= 1; i
< y
.size(); i
++)
636 ez
->SET(ez
->CONST_FALSE
, yy
.at(i
));
640 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
641 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort("\\B"), timestep
);
642 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
644 int a0
= ez
->NOT(ez
->OR(ez
->expression(ezSAT::OpOr
, vec_a
), ez
->expression(ezSAT::OpOr
, undef_a
)));
645 int b0
= ez
->NOT(ez
->OR(ez
->expression(ezSAT::OpOr
, vec_b
), ez
->expression(ezSAT::OpOr
, undef_b
)));
646 int a1
= ez
->expression(ezSAT::OpOr
, ez
->vec_and(vec_a
, ez
->vec_not(undef_a
)));
647 int b1
= ez
->expression(ezSAT::OpOr
, ez
->vec_and(vec_b
, ez
->vec_not(undef_b
)));
648 int aX
= ez
->expression(ezSAT::OpOr
, undef_a
);
649 int bX
= ez
->expression(ezSAT::OpOr
, undef_b
);
651 if (cell
->type
== "$logic_and")
652 ez
->SET(ez
->AND(ez
->OR(aX
, bX
), ez
->NOT(ez
->AND(a1
, b1
)), ez
->NOT(a0
), ez
->NOT(b0
)), undef_y
.at(0));
653 else if (cell
->type
== "$logic_or")
654 ez
->SET(ez
->AND(ez
->OR(aX
, bX
), ez
->NOT(ez
->AND(a0
, b0
)), ez
->NOT(a1
), ez
->NOT(b1
)), undef_y
.at(0));
658 for (size_t i
= 1; i
< undef_y
.size(); i
++)
659 ez
->SET(ez
->CONST_FALSE
, undef_y
.at(i
));
661 undefGating(y
, yy
, undef_y
);
666 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")
668 bool is_signed
= cell
->parameters
["\\A_SIGNED"].as_bool() && cell
->parameters
["\\B_SIGNED"].as_bool();
669 std::vector
<int> a
= importDefSigSpec(cell
->getPort("\\A"), timestep
);
670 std::vector
<int> b
= importDefSigSpec(cell
->getPort("\\B"), timestep
);
671 std::vector
<int> y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
672 extendSignalWidth(a
, b
, cell
);
674 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
676 if (model_undef
&& (cell
->type
== "$eqx" || cell
->type
== "$nex")) {
677 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
678 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort("\\B"), timestep
);
679 extendSignalWidth(undef_a
, undef_b
, cell
, true);
680 a
= ez
->vec_or(a
, undef_a
);
681 b
= ez
->vec_or(b
, undef_b
);
684 if (cell
->type
== "$lt")
685 ez
->SET(is_signed
? ez
->vec_lt_signed(a
, b
) : ez
->vec_lt_unsigned(a
, b
), yy
.at(0));
686 if (cell
->type
== "$le")
687 ez
->SET(is_signed
? ez
->vec_le_signed(a
, b
) : ez
->vec_le_unsigned(a
, b
), yy
.at(0));
688 if (cell
->type
== "$eq" || cell
->type
== "$eqx")
689 ez
->SET(ez
->vec_eq(a
, b
), yy
.at(0));
690 if (cell
->type
== "$ne" || cell
->type
== "$nex")
691 ez
->SET(ez
->vec_ne(a
, b
), yy
.at(0));
692 if (cell
->type
== "$ge")
693 ez
->SET(is_signed
? ez
->vec_ge_signed(a
, b
) : ez
->vec_ge_unsigned(a
, b
), yy
.at(0));
694 if (cell
->type
== "$gt")
695 ez
->SET(is_signed
? ez
->vec_gt_signed(a
, b
) : ez
->vec_gt_unsigned(a
, b
), yy
.at(0));
696 for (size_t i
= 1; i
< y
.size(); i
++)
697 ez
->SET(ez
->CONST_FALSE
, yy
.at(i
));
699 if (model_undef
&& (cell
->type
== "$eqx" || cell
->type
== "$nex"))
701 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
702 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort("\\B"), timestep
);
703 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
704 extendSignalWidth(undef_a
, undef_b
, cell
, true);
706 if (cell
->type
== "$eqx")
707 yy
.at(0) = ez
->AND(yy
.at(0), ez
->vec_eq(undef_a
, undef_b
));
709 yy
.at(0) = ez
->OR(yy
.at(0), ez
->vec_ne(undef_a
, undef_b
));
711 for (size_t i
= 0; i
< y
.size(); i
++)
712 ez
->SET(ez
->CONST_FALSE
, undef_y
.at(i
));
714 ez
->assume(ez
->vec_eq(y
, yy
));
716 else if (model_undef
&& (cell
->type
== "$eq" || cell
->type
== "$ne"))
718 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
719 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort("\\B"), timestep
);
720 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
721 extendSignalWidth(undef_a
, undef_b
, cell
, true);
723 int undef_any_a
= ez
->expression(ezSAT::OpOr
, undef_a
);
724 int undef_any_b
= ez
->expression(ezSAT::OpOr
, undef_b
);
725 int undef_any
= ez
->OR(undef_any_a
, undef_any_b
);
727 std::vector
<int> masked_a_bits
= ez
->vec_or(a
, ez
->vec_or(undef_a
, undef_b
));
728 std::vector
<int> masked_b_bits
= ez
->vec_or(b
, ez
->vec_or(undef_a
, undef_b
));
730 int masked_ne
= ez
->vec_ne(masked_a_bits
, masked_b_bits
);
731 int undef_y_bit
= ez
->AND(undef_any
, ez
->NOT(masked_ne
));
733 for (size_t i
= 1; i
< undef_y
.size(); i
++)
734 ez
->SET(ez
->CONST_FALSE
, undef_y
.at(i
));
735 ez
->SET(undef_y_bit
, undef_y
.at(0));
737 undefGating(y
, yy
, undef_y
);
742 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
743 undefGating(y
, yy
, undef_y
);
745 log_assert(!model_undef
|| arith_undef_handled
);
750 if (cell
->type
== "$shl" || cell
->type
== "$shr" || cell
->type
== "$sshl" || cell
->type
== "$sshr" || cell
->type
== "$shift" || cell
->type
== "$shiftx")
752 std::vector
<int> a
= importDefSigSpec(cell
->getPort("\\A"), timestep
);
753 std::vector
<int> b
= importDefSigSpec(cell
->getPort("\\B"), timestep
);
754 std::vector
<int> y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
756 int extend_bit
= ez
->CONST_FALSE
;
758 if (!cell
->type
.in("$shift", "$shiftx") && cell
->parameters
["\\A_SIGNED"].as_bool())
759 extend_bit
= a
.back();
761 while (y
.size() < a
.size())
762 y
.push_back(ez
->literal());
763 while (y
.size() > a
.size())
764 a
.push_back(extend_bit
);
766 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
767 std::vector
<int> shifted_a
;
769 if (cell
->type
== "$shl" || cell
->type
== "$sshl")
770 shifted_a
= ez
->vec_shift_left(a
, b
, false, ez
->CONST_FALSE
, ez
->CONST_FALSE
);
772 if (cell
->type
== "$shr")
773 shifted_a
= ez
->vec_shift_right(a
, b
, false, ez
->CONST_FALSE
, ez
->CONST_FALSE
);
775 if (cell
->type
== "$sshr")
776 shifted_a
= ez
->vec_shift_right(a
, b
, false, cell
->parameters
["\\A_SIGNED"].as_bool() ? a
.back() : ez
->CONST_FALSE
, ez
->CONST_FALSE
);
778 if (cell
->type
== "$shift" || cell
->type
== "$shiftx")
779 shifted_a
= ez
->vec_shift_right(a
, b
, cell
->parameters
["\\B_SIGNED"].as_bool(), ez
->CONST_FALSE
, ez
->CONST_FALSE
);
781 ez
->assume(ez
->vec_eq(shifted_a
, yy
));
785 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
786 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort("\\B"), timestep
);
787 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
788 std::vector
<int> undef_a_shifted
;
790 extend_bit
= cell
->type
== "$shiftx" ? ez
->CONST_TRUE
: ez
->CONST_FALSE
;
791 if (!cell
->type
.in("$shift", "$shiftx") && cell
->parameters
["\\A_SIGNED"].as_bool())
792 extend_bit
= undef_a
.back();
794 while (undef_y
.size() < undef_a
.size())
795 undef_y
.push_back(ez
->literal());
796 while (undef_y
.size() > undef_a
.size())
797 undef_a
.push_back(extend_bit
);
799 if (cell
->type
== "$shl" || cell
->type
== "$sshl")
800 undef_a_shifted
= ez
->vec_shift_left(undef_a
, b
, false, ez
->CONST_FALSE
, ez
->CONST_FALSE
);
802 if (cell
->type
== "$shr")
803 undef_a_shifted
= ez
->vec_shift_right(undef_a
, b
, false, ez
->CONST_FALSE
, ez
->CONST_FALSE
);
805 if (cell
->type
== "$sshr")
806 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
);
808 if (cell
->type
== "$shift")
809 undef_a_shifted
= ez
->vec_shift_right(undef_a
, b
, cell
->parameters
["\\B_SIGNED"].as_bool(), ez
->CONST_FALSE
, ez
->CONST_FALSE
);
811 if (cell
->type
== "$shiftx")
812 undef_a_shifted
= ez
->vec_shift_right(undef_a
, b
, cell
->parameters
["\\B_SIGNED"].as_bool(), ez
->CONST_TRUE
, ez
->CONST_TRUE
);
814 int undef_any_b
= ez
->expression(ezSAT::OpOr
, undef_b
);
815 std::vector
<int> undef_all_y_bits(undef_y
.size(), undef_any_b
);
816 ez
->assume(ez
->vec_eq(ez
->vec_or(undef_a_shifted
, undef_all_y_bits
), undef_y
));
817 undefGating(y
, yy
, undef_y
);
822 if (cell
->type
== "$mul")
824 std::vector
<int> a
= importDefSigSpec(cell
->getPort("\\A"), timestep
);
825 std::vector
<int> b
= importDefSigSpec(cell
->getPort("\\B"), timestep
);
826 std::vector
<int> y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
827 extendSignalWidth(a
, b
, y
, cell
);
829 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
831 std::vector
<int> tmp(a
.size(), ez
->CONST_FALSE
);
832 for (int i
= 0; i
< int(a
.size()); i
++)
834 std::vector
<int> shifted_a(a
.size(), ez
->CONST_FALSE
);
835 for (int j
= i
; j
< int(a
.size()); j
++)
836 shifted_a
.at(j
) = a
.at(j
-i
);
837 tmp
= ez
->vec_ite(b
.at(i
), ez
->vec_add(tmp
, shifted_a
), tmp
);
839 ez
->assume(ez
->vec_eq(tmp
, yy
));
842 log_assert(arith_undef_handled
);
843 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
844 undefGating(y
, yy
, undef_y
);
849 if (cell
->type
== "$macc")
851 std::vector
<int> a
= importDefSigSpec(cell
->getPort("\\A"), timestep
);
852 std::vector
<int> b
= importDefSigSpec(cell
->getPort("\\B"), timestep
);
853 std::vector
<int> y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
856 macc
.from_cell(cell
);
858 std::vector
<int> tmp(GetSize(y
), ez
->CONST_FALSE
);
860 for (auto &port
: macc
.ports
)
862 std::vector
<int> in_a
= importDefSigSpec(port
.in_a
, timestep
);
863 std::vector
<int> in_b
= importDefSigSpec(port
.in_b
, timestep
);
865 while (GetSize(in_a
) < GetSize(y
))
866 in_a
.push_back(port
.is_signed
&& !in_a
.empty() ? in_a
.back() : ez
->CONST_FALSE
);
867 in_a
.resize(GetSize(y
));
871 while (GetSize(in_b
) < GetSize(y
))
872 in_b
.push_back(port
.is_signed
&& !in_b
.empty() ? in_b
.back() : ez
->CONST_FALSE
);
873 in_b
.resize(GetSize(y
));
875 for (int i
= 0; i
< GetSize(in_b
); i
++) {
876 std::vector
<int> shifted_a(in_a
.size(), ez
->CONST_FALSE
);
877 for (int j
= i
; j
< int(in_a
.size()); j
++)
878 shifted_a
.at(j
) = in_a
.at(j
-i
);
879 if (port
.do_subtract
)
880 tmp
= ez
->vec_ite(in_b
.at(i
), ez
->vec_sub(tmp
, shifted_a
), tmp
);
882 tmp
= ez
->vec_ite(in_b
.at(i
), ez
->vec_add(tmp
, shifted_a
), tmp
);
887 if (port
.do_subtract
)
888 tmp
= ez
->vec_sub(tmp
, in_a
);
890 tmp
= ez
->vec_add(tmp
, in_a
);
894 for (int i
= 0; i
< GetSize(b
); i
++) {
895 std::vector
<int> val(GetSize(y
), ez
->CONST_FALSE
);
897 tmp
= ez
->vec_add(tmp
, val
);
902 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
903 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort("\\B"), timestep
);
905 int undef_any_a
= ez
->expression(ezSAT::OpOr
, undef_a
);
906 int undef_any_b
= ez
->expression(ezSAT::OpOr
, undef_b
);
908 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
909 ez
->assume(ez
->vec_eq(undef_y
, std::vector
<int>(GetSize(y
), ez
->OR(undef_any_a
, undef_any_b
))));
911 undefGating(y
, tmp
, undef_y
);
914 ez
->assume(ez
->vec_eq(y
, tmp
));
919 if (cell
->type
== "$div" || cell
->type
== "$mod")
921 std::vector
<int> a
= importDefSigSpec(cell
->getPort("\\A"), timestep
);
922 std::vector
<int> b
= importDefSigSpec(cell
->getPort("\\B"), timestep
);
923 std::vector
<int> y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
924 extendSignalWidth(a
, b
, y
, cell
);
926 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
928 std::vector
<int> a_u
, b_u
;
929 if (cell
->parameters
["\\A_SIGNED"].as_bool() && cell
->parameters
["\\B_SIGNED"].as_bool()) {
930 a_u
= ez
->vec_ite(a
.back(), ez
->vec_neg(a
), a
);
931 b_u
= ez
->vec_ite(b
.back(), ez
->vec_neg(b
), b
);
937 std::vector
<int> chain_buf
= a_u
;
938 std::vector
<int> y_u(a_u
.size(), ez
->CONST_FALSE
);
939 for (int i
= int(a
.size())-1; i
>= 0; i
--)
941 chain_buf
.insert(chain_buf
.end(), chain_buf
.size(), ez
->CONST_FALSE
);
943 std::vector
<int> b_shl(i
, ez
->CONST_FALSE
);
944 b_shl
.insert(b_shl
.end(), b_u
.begin(), b_u
.end());
945 b_shl
.insert(b_shl
.end(), chain_buf
.size()-b_shl
.size(), ez
->CONST_FALSE
);
947 y_u
.at(i
) = ez
->vec_ge_unsigned(chain_buf
, b_shl
);
948 chain_buf
= ez
->vec_ite(y_u
.at(i
), ez
->vec_sub(chain_buf
, b_shl
), chain_buf
);
950 chain_buf
.erase(chain_buf
.begin() + a_u
.size(), chain_buf
.end());
953 std::vector
<int> y_tmp
= ignore_div_by_zero
? yy
: ez
->vec_var(y
.size());
954 if (cell
->type
== "$div") {
955 if (cell
->parameters
["\\A_SIGNED"].as_bool() && cell
->parameters
["\\B_SIGNED"].as_bool())
956 ez
->assume(ez
->vec_eq(y_tmp
, ez
->vec_ite(ez
->XOR(a
.back(), b
.back()), ez
->vec_neg(y_u
), y_u
)));
958 ez
->assume(ez
->vec_eq(y_tmp
, y_u
));
960 if (cell
->parameters
["\\A_SIGNED"].as_bool() && cell
->parameters
["\\B_SIGNED"].as_bool())
961 ez
->assume(ez
->vec_eq(y_tmp
, ez
->vec_ite(a
.back(), ez
->vec_neg(chain_buf
), chain_buf
)));
963 ez
->assume(ez
->vec_eq(y_tmp
, chain_buf
));
966 if (ignore_div_by_zero
) {
967 ez
->assume(ez
->expression(ezSAT::OpOr
, b
));
969 std::vector
<int> div_zero_result
;
970 if (cell
->type
== "$div") {
971 if (cell
->parameters
["\\A_SIGNED"].as_bool() && cell
->parameters
["\\B_SIGNED"].as_bool()) {
972 std::vector
<int> all_ones(y
.size(), ez
->CONST_TRUE
);
973 std::vector
<int> only_first_one(y
.size(), ez
->CONST_FALSE
);
974 only_first_one
.at(0) = ez
->CONST_TRUE
;
975 div_zero_result
= ez
->vec_ite(a
.back(), only_first_one
, all_ones
);
977 div_zero_result
.insert(div_zero_result
.end(), cell
->getPort("\\A").size(), ez
->CONST_TRUE
);
978 div_zero_result
.insert(div_zero_result
.end(), y
.size() - div_zero_result
.size(), ez
->CONST_FALSE
);
981 int copy_a_bits
= min(cell
->getPort("\\A").size(), cell
->getPort("\\B").size());
982 div_zero_result
.insert(div_zero_result
.end(), a
.begin(), a
.begin() + copy_a_bits
);
983 if (cell
->parameters
["\\A_SIGNED"].as_bool() && cell
->parameters
["\\B_SIGNED"].as_bool())
984 div_zero_result
.insert(div_zero_result
.end(), y
.size() - div_zero_result
.size(), div_zero_result
.back());
986 div_zero_result
.insert(div_zero_result
.end(), y
.size() - div_zero_result
.size(), ez
->CONST_FALSE
);
988 ez
->assume(ez
->vec_eq(yy
, ez
->vec_ite(ez
->expression(ezSAT::OpOr
, b
), y_tmp
, div_zero_result
)));
992 log_assert(arith_undef_handled
);
993 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
994 undefGating(y
, yy
, undef_y
);
999 if (cell
->type
== "$lut")
1001 std::vector
<int> a
= importDefSigSpec(cell
->getPort("\\A"), timestep
);
1002 std::vector
<int> y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
1004 std::vector
<int> lut
;
1005 for (auto bit
: cell
->getParam("\\LUT").bits
)
1006 lut
.push_back(bit
== RTLIL::S1
? ez
->CONST_TRUE
: ez
->CONST_FALSE
);
1007 while (GetSize(lut
) < (1 << GetSize(a
)))
1008 lut
.push_back(ez
->CONST_FALSE
);
1009 lut
.resize(1 << GetSize(a
));
1013 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
1014 std::vector
<int> t(lut
), u(GetSize(t
), ez
->CONST_FALSE
);
1016 for (int i
= GetSize(a
)-1; i
>= 0; i
--)
1018 std::vector
<int> t0(t
.begin(), t
.begin() + GetSize(t
)/2);
1019 std::vector
<int> t1(t
.begin() + GetSize(t
)/2, t
.end());
1021 std::vector
<int> u0(u
.begin(), u
.begin() + GetSize(u
)/2);
1022 std::vector
<int> u1(u
.begin() + GetSize(u
)/2, u
.end());
1024 t
= ez
->vec_ite(a
[i
], t1
, t0
);
1025 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 log_assert(GetSize(t
) == 1);
1029 log_assert(GetSize(u
) == 1);
1030 undefGating(y
, t
, u
);
1031 ez
->assume(ez
->vec_eq(importUndefSigSpec(cell
->getPort("\\Y"), timestep
), u
));
1035 std::vector
<int> t
= lut
;
1036 for (int i
= GetSize(a
)-1; i
>= 0; i
--)
1038 std::vector
<int> t0(t
.begin(), t
.begin() + GetSize(t
)/2);
1039 std::vector
<int> t1(t
.begin() + GetSize(t
)/2, t
.end());
1040 t
= ez
->vec_ite(a
[i
], t1
, t0
);
1043 log_assert(GetSize(t
) == 1);
1044 ez
->assume(ez
->vec_eq(y
, t
));
1049 if (cell
->type
== "$sop")
1051 std::vector
<int> a
= importDefSigSpec(cell
->getPort("\\A"), timestep
);
1052 int y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
).at(0);
1054 int width
= cell
->getParam("\\WIDTH").as_int();
1055 int depth
= cell
->getParam("\\DEPTH").as_int();
1057 vector
<State
> table_raw
= cell
->getParam("\\TABLE").bits
;
1058 while (GetSize(table_raw
) < 2*width
*depth
)
1059 table_raw
.push_back(State::S0
);
1061 vector
<vector
<int>> table(depth
);
1063 for (int i
= 0; i
< depth
; i
++)
1064 for (int j
= 0; j
< width
; j
++)
1066 bool pat0
= (table_raw
[2*width
*i
+ 2*j
+ 0] == State::S1
);
1067 bool pat1
= (table_raw
[2*width
*i
+ 2*j
+ 1] == State::S1
);
1070 table
.at(i
).push_back(0);
1071 else if (!pat0
&& pat1
)
1072 table
.at(i
).push_back(1);
1074 table
.at(i
).push_back(-1);
1079 std::vector
<int> products
, undef_products
;
1080 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
1081 int undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
).at(0);
1083 for (int i
= 0; i
< depth
; i
++)
1085 std::vector
<int> cmp_a
, cmp_ua
, cmp_b
;
1087 for (int j
= 0; j
< width
; j
++)
1088 if (table
.at(i
).at(j
) >= 0) {
1089 cmp_a
.push_back(a
.at(j
));
1090 cmp_ua
.push_back(undef_a
.at(j
));
1091 cmp_b
.push_back(table
.at(i
).at(j
) ? ez
->CONST_TRUE
: ez
->CONST_FALSE
);
1094 std::vector
<int> masked_a
= ez
->vec_or(cmp_a
, cmp_ua
);
1095 std::vector
<int> masked_b
= ez
->vec_or(cmp_b
, cmp_ua
);
1097 int masked_eq
= ez
->vec_eq(masked_a
, masked_b
);
1098 int any_undef
= ez
->expression(ezSAT::OpOr
, cmp_ua
);
1100 undef_products
.push_back(ez
->AND(any_undef
, masked_eq
));
1101 products
.push_back(ez
->AND(ez
->NOT(any_undef
), masked_eq
));
1104 int yy
= ez
->expression(ezSAT::OpOr
, products
);
1105 ez
->SET(undef_y
, ez
->AND(ez
->NOT(yy
), ez
->expression(ezSAT::OpOr
, undef_products
)));
1106 undefGating(y
, yy
, undef_y
);
1110 std::vector
<int> products
;
1112 for (int i
= 0; i
< depth
; i
++)
1114 std::vector
<int> cmp_a
, cmp_b
;
1116 for (int j
= 0; j
< width
; j
++)
1117 if (table
.at(i
).at(j
) >= 0) {
1118 cmp_a
.push_back(a
.at(j
));
1119 cmp_b
.push_back(table
.at(i
).at(j
) ? ez
->CONST_TRUE
: ez
->CONST_FALSE
);
1122 products
.push_back(ez
->vec_eq(cmp_a
, cmp_b
));
1125 ez
->SET(y
, ez
->expression(ezSAT::OpOr
, products
));
1131 if (cell
->type
== "$fa")
1133 std::vector
<int> a
= importDefSigSpec(cell
->getPort("\\A"), timestep
);
1134 std::vector
<int> b
= importDefSigSpec(cell
->getPort("\\B"), timestep
);
1135 std::vector
<int> c
= importDefSigSpec(cell
->getPort("\\C"), timestep
);
1136 std::vector
<int> y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
1137 std::vector
<int> x
= importDefSigSpec(cell
->getPort("\\X"), timestep
);
1139 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
1140 std::vector
<int> xx
= model_undef
? ez
->vec_var(x
.size()) : x
;
1142 std::vector
<int> t1
= ez
->vec_xor(a
, b
);
1143 ez
->assume(ez
->vec_eq(yy
, ez
->vec_xor(t1
, c
)));
1145 std::vector
<int> t2
= ez
->vec_and(a
, b
);
1146 std::vector
<int> t3
= ez
->vec_and(c
, t1
);
1147 ez
->assume(ez
->vec_eq(xx
, ez
->vec_or(t2
, t3
)));
1151 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
1152 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort("\\B"), timestep
);
1153 std::vector
<int> undef_c
= importUndefSigSpec(cell
->getPort("\\C"), timestep
);
1155 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
1156 std::vector
<int> undef_x
= importUndefSigSpec(cell
->getPort("\\X"), timestep
);
1158 ez
->assume(ez
->vec_eq(undef_y
, ez
->vec_or(ez
->vec_or(undef_a
, undef_b
), undef_c
)));
1159 ez
->assume(ez
->vec_eq(undef_x
, undef_y
));
1161 undefGating(y
, yy
, undef_y
);
1162 undefGating(x
, xx
, undef_x
);
1167 if (cell
->type
== "$lcu")
1169 std::vector
<int> p
= importDefSigSpec(cell
->getPort("\\P"), timestep
);
1170 std::vector
<int> g
= importDefSigSpec(cell
->getPort("\\G"), timestep
);
1171 std::vector
<int> ci
= importDefSigSpec(cell
->getPort("\\CI"), timestep
);
1172 std::vector
<int> co
= importDefSigSpec(cell
->getPort("\\CO"), timestep
);
1174 std::vector
<int> yy
= model_undef
? ez
->vec_var(co
.size()) : co
;
1176 for (int i
= 0; i
< GetSize(co
); i
++)
1177 ez
->SET(yy
[i
], ez
->OR(g
[i
], ez
->AND(p
[i
], i
? yy
[i
-1] : ci
[0])));
1181 std::vector
<int> undef_p
= importUndefSigSpec(cell
->getPort("\\P"), timestep
);
1182 std::vector
<int> undef_g
= importUndefSigSpec(cell
->getPort("\\G"), timestep
);
1183 std::vector
<int> undef_ci
= importUndefSigSpec(cell
->getPort("\\CI"), timestep
);
1184 std::vector
<int> undef_co
= importUndefSigSpec(cell
->getPort("\\CO"), timestep
);
1186 int undef_any_p
= ez
->expression(ezSAT::OpOr
, undef_p
);
1187 int undef_any_g
= ez
->expression(ezSAT::OpOr
, undef_g
);
1188 int undef_any_ci
= ez
->expression(ezSAT::OpOr
, undef_ci
);
1189 int undef_co_bit
= ez
->OR(undef_any_p
, undef_any_g
, undef_any_ci
);
1191 std::vector
<int> undef_co_bits(undef_co
.size(), undef_co_bit
);
1192 ez
->assume(ez
->vec_eq(undef_co_bits
, undef_co
));
1194 undefGating(co
, yy
, undef_co
);
1199 if (cell
->type
== "$alu")
1201 std::vector
<int> a
= importDefSigSpec(cell
->getPort("\\A"), timestep
);
1202 std::vector
<int> b
= importDefSigSpec(cell
->getPort("\\B"), timestep
);
1203 std::vector
<int> y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
1204 std::vector
<int> x
= importDefSigSpec(cell
->getPort("\\X"), timestep
);
1205 std::vector
<int> ci
= importDefSigSpec(cell
->getPort("\\CI"), timestep
);
1206 std::vector
<int> bi
= importDefSigSpec(cell
->getPort("\\BI"), timestep
);
1207 std::vector
<int> co
= importDefSigSpec(cell
->getPort("\\CO"), timestep
);
1209 extendSignalWidth(a
, b
, y
, cell
);
1210 extendSignalWidth(a
, b
, x
, cell
);
1211 extendSignalWidth(a
, b
, co
, cell
);
1213 std::vector
<int> def_y
= model_undef
? ez
->vec_var(y
.size()) : y
;
1214 std::vector
<int> def_x
= model_undef
? ez
->vec_var(x
.size()) : x
;
1215 std::vector
<int> def_co
= model_undef
? ez
->vec_var(co
.size()) : co
;
1217 log_assert(GetSize(y
) == GetSize(x
));
1218 log_assert(GetSize(y
) == GetSize(co
));
1219 log_assert(GetSize(ci
) == 1);
1220 log_assert(GetSize(bi
) == 1);
1222 for (int i
= 0; i
< GetSize(y
); i
++)
1224 int s1
= a
.at(i
), s2
= ez
->XOR(b
.at(i
), bi
.at(0)), s3
= i
? co
.at(i
-1) : ci
.at(0);
1225 ez
->SET(def_x
.at(i
), ez
->XOR(s1
, s2
));
1226 ez
->SET(def_y
.at(i
), ez
->XOR(def_x
.at(i
), s3
));
1227 ez
->SET(def_co
.at(i
), ez
->OR(ez
->AND(s1
, s2
), ez
->AND(s1
, s3
), ez
->AND(s2
, s3
)));
1232 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
1233 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort("\\B"), timestep
);
1234 std::vector
<int> undef_ci
= importUndefSigSpec(cell
->getPort("\\CI"), timestep
);
1235 std::vector
<int> undef_bi
= importUndefSigSpec(cell
->getPort("\\BI"), timestep
);
1237 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
1238 std::vector
<int> undef_x
= importUndefSigSpec(cell
->getPort("\\X"), timestep
);
1239 std::vector
<int> undef_co
= importUndefSigSpec(cell
->getPort("\\CO"), timestep
);
1241 extendSignalWidth(undef_a
, undef_b
, undef_y
, cell
);
1242 extendSignalWidth(undef_a
, undef_b
, undef_x
, cell
);
1243 extendSignalWidth(undef_a
, undef_b
, undef_co
, cell
);
1245 std::vector
<int> all_inputs_undef
;
1246 all_inputs_undef
.insert(all_inputs_undef
.end(), undef_a
.begin(), undef_a
.end());
1247 all_inputs_undef
.insert(all_inputs_undef
.end(), undef_b
.begin(), undef_b
.end());
1248 all_inputs_undef
.insert(all_inputs_undef
.end(), undef_ci
.begin(), undef_ci
.end());
1249 all_inputs_undef
.insert(all_inputs_undef
.end(), undef_bi
.begin(), undef_bi
.end());
1250 int undef_any
= ez
->expression(ezSAT::OpOr
, all_inputs_undef
);
1252 for (int i
= 0; i
< GetSize(undef_y
); i
++) {
1253 ez
->SET(undef_y
.at(i
), undef_any
);
1254 ez
->SET(undef_x
.at(i
), ez
->OR(undef_a
.at(i
), undef_b
.at(i
), undef_bi
.at(0)));
1255 ez
->SET(undef_co
.at(i
), undef_any
);
1258 undefGating(y
, def_y
, undef_y
);
1259 undefGating(x
, def_x
, undef_x
);
1260 undefGating(co
, def_co
, undef_co
);
1265 if (cell
->type
== "$slice")
1267 RTLIL::SigSpec a
= cell
->getPort("\\A");
1268 RTLIL::SigSpec y
= cell
->getPort("\\Y");
1269 ez
->assume(signals_eq(a
.extract(cell
->parameters
.at("\\OFFSET").as_int(), y
.size()), y
, timestep
));
1273 if (cell
->type
== "$concat")
1275 RTLIL::SigSpec a
= cell
->getPort("\\A");
1276 RTLIL::SigSpec b
= cell
->getPort("\\B");
1277 RTLIL::SigSpec y
= cell
->getPort("\\Y");
1279 RTLIL::SigSpec ab
= a
;
1282 ez
->assume(signals_eq(ab
, y
, timestep
));
1286 if (timestep
> 0 && cell
->type
.in("$ff", "$dff", "$_FF_", "$_DFF_N_", "$_DFF_P_"))
1290 initial_state
.add((*sigmap
)(cell
->getPort("\\Q")));
1294 std::vector
<int> d
= importDefSigSpec(cell
->getPort("\\D"), timestep
-1);
1295 std::vector
<int> q
= importDefSigSpec(cell
->getPort("\\Q"), timestep
);
1297 std::vector
<int> qq
= model_undef
? ez
->vec_var(q
.size()) : q
;
1298 ez
->assume(ez
->vec_eq(d
, qq
));
1302 std::vector
<int> undef_d
= importUndefSigSpec(cell
->getPort("\\D"), timestep
-1);
1303 std::vector
<int> undef_q
= importUndefSigSpec(cell
->getPort("\\Q"), timestep
);
1305 ez
->assume(ez
->vec_eq(undef_d
, undef_q
));
1306 undefGating(q
, qq
, undef_q
);
1312 if (cell
->type
== "$anyconst")
1317 std::vector
<int> d
= importDefSigSpec(cell
->getPort("\\Y"), timestep
-1);
1318 std::vector
<int> q
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
1320 std::vector
<int> qq
= model_undef
? ez
->vec_var(q
.size()) : q
;
1321 ez
->assume(ez
->vec_eq(d
, qq
));
1325 std::vector
<int> undef_d
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
-1);
1326 std::vector
<int> undef_q
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
1328 ez
->assume(ez
->vec_eq(undef_d
, undef_q
));
1329 undefGating(q
, qq
, undef_q
);
1334 if (cell
->type
== "$anyseq")
1339 if (cell
->type
== "$_BUF_" || cell
->type
== "$equiv")
1341 std::vector
<int> a
= importDefSigSpec(cell
->getPort("\\A"), timestep
);
1342 std::vector
<int> y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
1343 extendSignalWidthUnary(a
, y
, cell
);
1345 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
1346 ez
->assume(ez
->vec_eq(a
, yy
));
1349 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
1350 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
1351 extendSignalWidthUnary(undef_a
, undef_y
, cell
, false);
1352 ez
->assume(ez
->vec_eq(undef_a
, undef_y
));
1353 undefGating(y
, yy
, undef_y
);
1358 if (cell
->type
== "$initstate")
1360 auto key
= make_pair(prefix
, timestep
);
1361 if (initstates
.count(key
) == 0)
1362 initstates
[key
] = false;
1364 std::vector
<int> y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
1365 log_assert(GetSize(y
) == 1);
1366 ez
->SET(y
[0], initstates
[key
] ? ez
->CONST_TRUE
: ez
->CONST_FALSE
);
1369 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
1370 log_assert(GetSize(undef_y
) == 1);
1371 ez
->SET(undef_y
[0], ez
->CONST_FALSE
);
1377 if (cell
->type
== "$assert")
1379 std::string pf
= prefix
+ (timestep
== -1 ? "" : stringf("@%d:", timestep
));
1380 asserts_a
[pf
].append((*sigmap
)(cell
->getPort("\\A")));
1381 asserts_en
[pf
].append((*sigmap
)(cell
->getPort("\\EN")));
1385 if (cell
->type
== "$assume")
1387 std::string pf
= prefix
+ (timestep
== -1 ? "" : stringf("@%d:", timestep
));
1388 assumes_a
[pf
].append((*sigmap
)(cell
->getPort("\\A")));
1389 assumes_en
[pf
].append((*sigmap
)(cell
->getPort("\\EN")));
1393 // Unsupported internal cell types: $pow $lut
1394 // .. and all sequential cells except $dff and $_DFF_[NP]_