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_one_hot
= ez
->CONST_FALSE
;
511 int maybe_many_hot
= ez
->CONST_FALSE
;
513 int sure_one_hot
= ez
->CONST_FALSE
;
514 int sure_many_hot
= ez
->CONST_FALSE
;
516 std::vector
<int> bits_set
= std::vector
<int>(undef_y
.size(), ez
->CONST_FALSE
);
517 std::vector
<int> bits_clr
= std::vector
<int>(undef_y
.size(), ez
->CONST_FALSE
);
519 for (size_t i
= 0; i
< s
.size(); i
++)
521 std::vector
<int> part_of_b(b
.begin()+i
*a
.size(), b
.begin()+(i
+1)*a
.size());
522 std::vector
<int> part_of_undef_b(undef_b
.begin()+i
*a
.size(), undef_b
.begin()+(i
+1)*a
.size());
524 int maybe_s
= ez
->OR(s
.at(i
), undef_s
.at(i
));
525 int sure_s
= ez
->AND(s
.at(i
), ez
->NOT(undef_s
.at(i
)));
527 maybe_one_hot
= ez
->OR(maybe_one_hot
, maybe_s
);
528 maybe_many_hot
= ez
->OR(maybe_many_hot
, ez
->AND(maybe_one_hot
, maybe_s
));
530 sure_one_hot
= ez
->OR(sure_one_hot
, sure_s
);
531 sure_many_hot
= ez
->OR(sure_many_hot
, ez
->AND(sure_one_hot
, sure_s
));
533 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
);
534 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
);
537 int maybe_a
= ez
->NOT(maybe_one_hot
);
539 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
);
540 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
);
542 ez
->assume(ez
->vec_eq(ez
->vec_not(ez
->vec_xor(bits_set
, bits_clr
)), undef_y
));
543 undefGating(y
, yy
, undef_y
);
548 if (cell
->type
== "$pos" || cell
->type
== "$neg")
550 std::vector
<int> a
= importDefSigSpec(cell
->getPort("\\A"), timestep
);
551 std::vector
<int> y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
552 extendSignalWidthUnary(a
, y
, cell
);
554 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
556 if (cell
->type
== "$pos") {
557 ez
->assume(ez
->vec_eq(a
, yy
));
559 std::vector
<int> zero(a
.size(), ez
->CONST_FALSE
);
560 ez
->assume(ez
->vec_eq(ez
->vec_sub(zero
, a
), yy
));
565 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
566 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
567 extendSignalWidthUnary(undef_a
, undef_y
, cell
);
569 if (cell
->type
== "$pos") {
570 ez
->assume(ez
->vec_eq(undef_a
, undef_y
));
572 int undef_any_a
= ez
->expression(ezSAT::OpOr
, undef_a
);
573 std::vector
<int> undef_y_bits(undef_y
.size(), undef_any_a
);
574 ez
->assume(ez
->vec_eq(undef_y_bits
, undef_y
));
577 undefGating(y
, yy
, undef_y
);
582 if (cell
->type
== "$reduce_and" || cell
->type
== "$reduce_or" || cell
->type
== "$reduce_xor" ||
583 cell
->type
== "$reduce_xnor" || cell
->type
== "$reduce_bool" || cell
->type
== "$logic_not")
585 std::vector
<int> a
= importDefSigSpec(cell
->getPort("\\A"), timestep
);
586 std::vector
<int> y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
588 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
590 if (cell
->type
== "$reduce_and")
591 ez
->SET(ez
->expression(ez
->OpAnd
, a
), yy
.at(0));
592 if (cell
->type
== "$reduce_or" || cell
->type
== "$reduce_bool")
593 ez
->SET(ez
->expression(ez
->OpOr
, a
), yy
.at(0));
594 if (cell
->type
== "$reduce_xor")
595 ez
->SET(ez
->expression(ez
->OpXor
, a
), yy
.at(0));
596 if (cell
->type
== "$reduce_xnor")
597 ez
->SET(ez
->NOT(ez
->expression(ez
->OpXor
, a
)), yy
.at(0));
598 if (cell
->type
== "$logic_not")
599 ez
->SET(ez
->NOT(ez
->expression(ez
->OpOr
, a
)), yy
.at(0));
600 for (size_t i
= 1; i
< y
.size(); i
++)
601 ez
->SET(ez
->CONST_FALSE
, yy
.at(i
));
605 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
606 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
607 int aX
= ez
->expression(ezSAT::OpOr
, undef_a
);
609 if (cell
->type
== "$reduce_and") {
610 int a0
= ez
->expression(ezSAT::OpOr
, ez
->vec_and(ez
->vec_not(a
), ez
->vec_not(undef_a
)));
611 ez
->assume(ez
->IFF(ez
->AND(ez
->NOT(a0
), aX
), undef_y
.at(0)));
613 else if (cell
->type
== "$reduce_or" || cell
->type
== "$reduce_bool" || cell
->type
== "$logic_not") {
614 int a1
= ez
->expression(ezSAT::OpOr
, ez
->vec_and(a
, ez
->vec_not(undef_a
)));
615 ez
->assume(ez
->IFF(ez
->AND(ez
->NOT(a1
), aX
), undef_y
.at(0)));
617 else if (cell
->type
== "$reduce_xor" || cell
->type
== "$reduce_xnor") {
618 ez
->assume(ez
->IFF(aX
, undef_y
.at(0)));
622 for (size_t i
= 1; i
< undef_y
.size(); i
++)
623 ez
->SET(ez
->CONST_FALSE
, undef_y
.at(i
));
625 undefGating(y
, yy
, undef_y
);
630 if (cell
->type
== "$logic_and" || cell
->type
== "$logic_or")
632 std::vector
<int> vec_a
= importDefSigSpec(cell
->getPort("\\A"), timestep
);
633 std::vector
<int> vec_b
= importDefSigSpec(cell
->getPort("\\B"), timestep
);
635 int a
= ez
->expression(ez
->OpOr
, vec_a
);
636 int b
= ez
->expression(ez
->OpOr
, vec_b
);
637 std::vector
<int> y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
639 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
641 if (cell
->type
== "$logic_and")
642 ez
->SET(ez
->expression(ez
->OpAnd
, a
, b
), yy
.at(0));
644 ez
->SET(ez
->expression(ez
->OpOr
, a
, b
), yy
.at(0));
645 for (size_t i
= 1; i
< y
.size(); i
++)
646 ez
->SET(ez
->CONST_FALSE
, yy
.at(i
));
650 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
651 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort("\\B"), timestep
);
652 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
654 int a0
= ez
->NOT(ez
->OR(ez
->expression(ezSAT::OpOr
, vec_a
), ez
->expression(ezSAT::OpOr
, undef_a
)));
655 int b0
= ez
->NOT(ez
->OR(ez
->expression(ezSAT::OpOr
, vec_b
), ez
->expression(ezSAT::OpOr
, undef_b
)));
656 int a1
= ez
->expression(ezSAT::OpOr
, ez
->vec_and(vec_a
, ez
->vec_not(undef_a
)));
657 int b1
= ez
->expression(ezSAT::OpOr
, ez
->vec_and(vec_b
, ez
->vec_not(undef_b
)));
658 int aX
= ez
->expression(ezSAT::OpOr
, undef_a
);
659 int bX
= ez
->expression(ezSAT::OpOr
, undef_b
);
661 if (cell
->type
== "$logic_and")
662 ez
->SET(ez
->AND(ez
->OR(aX
, bX
), ez
->NOT(ez
->AND(a1
, b1
)), ez
->NOT(a0
), ez
->NOT(b0
)), undef_y
.at(0));
663 else if (cell
->type
== "$logic_or")
664 ez
->SET(ez
->AND(ez
->OR(aX
, bX
), ez
->NOT(ez
->AND(a0
, b0
)), ez
->NOT(a1
), ez
->NOT(b1
)), undef_y
.at(0));
668 for (size_t i
= 1; i
< undef_y
.size(); i
++)
669 ez
->SET(ez
->CONST_FALSE
, undef_y
.at(i
));
671 undefGating(y
, yy
, undef_y
);
676 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")
678 bool is_signed
= cell
->parameters
["\\A_SIGNED"].as_bool() && cell
->parameters
["\\B_SIGNED"].as_bool();
679 std::vector
<int> a
= importDefSigSpec(cell
->getPort("\\A"), timestep
);
680 std::vector
<int> b
= importDefSigSpec(cell
->getPort("\\B"), timestep
);
681 std::vector
<int> y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
682 extendSignalWidth(a
, b
, cell
);
684 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
686 if (model_undef
&& (cell
->type
== "$eqx" || cell
->type
== "$nex")) {
687 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
688 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort("\\B"), timestep
);
689 extendSignalWidth(undef_a
, undef_b
, cell
, true);
690 a
= ez
->vec_or(a
, undef_a
);
691 b
= ez
->vec_or(b
, undef_b
);
694 if (cell
->type
== "$lt")
695 ez
->SET(is_signed
? ez
->vec_lt_signed(a
, b
) : ez
->vec_lt_unsigned(a
, b
), yy
.at(0));
696 if (cell
->type
== "$le")
697 ez
->SET(is_signed
? ez
->vec_le_signed(a
, b
) : ez
->vec_le_unsigned(a
, b
), yy
.at(0));
698 if (cell
->type
== "$eq" || cell
->type
== "$eqx")
699 ez
->SET(ez
->vec_eq(a
, b
), yy
.at(0));
700 if (cell
->type
== "$ne" || cell
->type
== "$nex")
701 ez
->SET(ez
->vec_ne(a
, b
), yy
.at(0));
702 if (cell
->type
== "$ge")
703 ez
->SET(is_signed
? ez
->vec_ge_signed(a
, b
) : ez
->vec_ge_unsigned(a
, b
), yy
.at(0));
704 if (cell
->type
== "$gt")
705 ez
->SET(is_signed
? ez
->vec_gt_signed(a
, b
) : ez
->vec_gt_unsigned(a
, b
), yy
.at(0));
706 for (size_t i
= 1; i
< y
.size(); i
++)
707 ez
->SET(ez
->CONST_FALSE
, yy
.at(i
));
709 if (model_undef
&& (cell
->type
== "$eqx" || cell
->type
== "$nex"))
711 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
712 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort("\\B"), timestep
);
713 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
714 extendSignalWidth(undef_a
, undef_b
, cell
, true);
716 if (cell
->type
== "$eqx")
717 yy
.at(0) = ez
->AND(yy
.at(0), ez
->vec_eq(undef_a
, undef_b
));
719 yy
.at(0) = ez
->OR(yy
.at(0), ez
->vec_ne(undef_a
, undef_b
));
721 for (size_t i
= 0; i
< y
.size(); i
++)
722 ez
->SET(ez
->CONST_FALSE
, undef_y
.at(i
));
724 ez
->assume(ez
->vec_eq(y
, yy
));
726 else if (model_undef
&& (cell
->type
== "$eq" || cell
->type
== "$ne"))
728 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
729 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort("\\B"), timestep
);
730 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
731 extendSignalWidth(undef_a
, undef_b
, cell
, true);
733 int undef_any_a
= ez
->expression(ezSAT::OpOr
, undef_a
);
734 int undef_any_b
= ez
->expression(ezSAT::OpOr
, undef_b
);
735 int undef_any
= ez
->OR(undef_any_a
, undef_any_b
);
737 std::vector
<int> masked_a_bits
= ez
->vec_or(a
, ez
->vec_or(undef_a
, undef_b
));
738 std::vector
<int> masked_b_bits
= ez
->vec_or(b
, ez
->vec_or(undef_a
, undef_b
));
740 int masked_ne
= ez
->vec_ne(masked_a_bits
, masked_b_bits
);
741 int undef_y_bit
= ez
->AND(undef_any
, ez
->NOT(masked_ne
));
743 for (size_t i
= 1; i
< undef_y
.size(); i
++)
744 ez
->SET(ez
->CONST_FALSE
, undef_y
.at(i
));
745 ez
->SET(undef_y_bit
, undef_y
.at(0));
747 undefGating(y
, yy
, undef_y
);
752 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
753 undefGating(y
, yy
, undef_y
);
755 log_assert(!model_undef
|| arith_undef_handled
);
760 if (cell
->type
== "$shl" || cell
->type
== "$shr" || cell
->type
== "$sshl" || cell
->type
== "$sshr" || cell
->type
== "$shift" || cell
->type
== "$shiftx")
762 std::vector
<int> a
= importDefSigSpec(cell
->getPort("\\A"), timestep
);
763 std::vector
<int> b
= importDefSigSpec(cell
->getPort("\\B"), timestep
);
764 std::vector
<int> y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
766 int extend_bit
= ez
->CONST_FALSE
;
768 if (!cell
->type
.in("$shift", "$shiftx") && cell
->parameters
["\\A_SIGNED"].as_bool())
769 extend_bit
= a
.back();
771 while (y
.size() < a
.size())
772 y
.push_back(ez
->literal());
773 while (y
.size() > a
.size())
774 a
.push_back(extend_bit
);
776 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
777 std::vector
<int> shifted_a
;
779 if (cell
->type
== "$shl" || cell
->type
== "$sshl")
780 shifted_a
= ez
->vec_shift_left(a
, b
, false, ez
->CONST_FALSE
, ez
->CONST_FALSE
);
782 if (cell
->type
== "$shr")
783 shifted_a
= ez
->vec_shift_right(a
, b
, false, ez
->CONST_FALSE
, ez
->CONST_FALSE
);
785 if (cell
->type
== "$sshr")
786 shifted_a
= ez
->vec_shift_right(a
, b
, false, cell
->parameters
["\\A_SIGNED"].as_bool() ? a
.back() : ez
->CONST_FALSE
, ez
->CONST_FALSE
);
788 if (cell
->type
== "$shift" || cell
->type
== "$shiftx")
789 shifted_a
= ez
->vec_shift_right(a
, b
, cell
->parameters
["\\B_SIGNED"].as_bool(), ez
->CONST_FALSE
, ez
->CONST_FALSE
);
791 ez
->assume(ez
->vec_eq(shifted_a
, yy
));
795 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
796 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort("\\B"), timestep
);
797 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
798 std::vector
<int> undef_a_shifted
;
800 extend_bit
= cell
->type
== "$shiftx" ? ez
->CONST_TRUE
: ez
->CONST_FALSE
;
801 if (!cell
->type
.in("$shift", "$shiftx") && cell
->parameters
["\\A_SIGNED"].as_bool())
802 extend_bit
= undef_a
.back();
804 while (undef_y
.size() < undef_a
.size())
805 undef_y
.push_back(ez
->literal());
806 while (undef_y
.size() > undef_a
.size())
807 undef_a
.push_back(extend_bit
);
809 if (cell
->type
== "$shl" || cell
->type
== "$sshl")
810 undef_a_shifted
= ez
->vec_shift_left(undef_a
, b
, false, ez
->CONST_FALSE
, ez
->CONST_FALSE
);
812 if (cell
->type
== "$shr")
813 undef_a_shifted
= ez
->vec_shift_right(undef_a
, b
, false, ez
->CONST_FALSE
, ez
->CONST_FALSE
);
815 if (cell
->type
== "$sshr")
816 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
);
818 if (cell
->type
== "$shift")
819 undef_a_shifted
= ez
->vec_shift_right(undef_a
, b
, cell
->parameters
["\\B_SIGNED"].as_bool(), ez
->CONST_FALSE
, ez
->CONST_FALSE
);
821 if (cell
->type
== "$shiftx")
822 undef_a_shifted
= ez
->vec_shift_right(undef_a
, b
, cell
->parameters
["\\B_SIGNED"].as_bool(), ez
->CONST_TRUE
, ez
->CONST_TRUE
);
824 int undef_any_b
= ez
->expression(ezSAT::OpOr
, undef_b
);
825 std::vector
<int> undef_all_y_bits(undef_y
.size(), undef_any_b
);
826 ez
->assume(ez
->vec_eq(ez
->vec_or(undef_a_shifted
, undef_all_y_bits
), undef_y
));
827 undefGating(y
, yy
, undef_y
);
832 if (cell
->type
== "$mul")
834 std::vector
<int> a
= importDefSigSpec(cell
->getPort("\\A"), timestep
);
835 std::vector
<int> b
= importDefSigSpec(cell
->getPort("\\B"), timestep
);
836 std::vector
<int> y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
837 extendSignalWidth(a
, b
, y
, cell
);
839 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
841 std::vector
<int> tmp(a
.size(), ez
->CONST_FALSE
);
842 for (int i
= 0; i
< int(a
.size()); i
++)
844 std::vector
<int> shifted_a(a
.size(), ez
->CONST_FALSE
);
845 for (int j
= i
; j
< int(a
.size()); j
++)
846 shifted_a
.at(j
) = a
.at(j
-i
);
847 tmp
= ez
->vec_ite(b
.at(i
), ez
->vec_add(tmp
, shifted_a
), tmp
);
849 ez
->assume(ez
->vec_eq(tmp
, yy
));
852 log_assert(arith_undef_handled
);
853 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
854 undefGating(y
, yy
, undef_y
);
859 if (cell
->type
== "$macc")
861 std::vector
<int> a
= importDefSigSpec(cell
->getPort("\\A"), timestep
);
862 std::vector
<int> b
= importDefSigSpec(cell
->getPort("\\B"), timestep
);
863 std::vector
<int> y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
866 macc
.from_cell(cell
);
868 std::vector
<int> tmp(GetSize(y
), ez
->CONST_FALSE
);
870 for (auto &port
: macc
.ports
)
872 std::vector
<int> in_a
= importDefSigSpec(port
.in_a
, timestep
);
873 std::vector
<int> in_b
= importDefSigSpec(port
.in_b
, timestep
);
875 while (GetSize(in_a
) < GetSize(y
))
876 in_a
.push_back(port
.is_signed
&& !in_a
.empty() ? in_a
.back() : ez
->CONST_FALSE
);
877 in_a
.resize(GetSize(y
));
881 while (GetSize(in_b
) < GetSize(y
))
882 in_b
.push_back(port
.is_signed
&& !in_b
.empty() ? in_b
.back() : ez
->CONST_FALSE
);
883 in_b
.resize(GetSize(y
));
885 for (int i
= 0; i
< GetSize(in_b
); i
++) {
886 std::vector
<int> shifted_a(in_a
.size(), ez
->CONST_FALSE
);
887 for (int j
= i
; j
< int(in_a
.size()); j
++)
888 shifted_a
.at(j
) = in_a
.at(j
-i
);
889 if (port
.do_subtract
)
890 tmp
= ez
->vec_ite(in_b
.at(i
), ez
->vec_sub(tmp
, shifted_a
), tmp
);
892 tmp
= ez
->vec_ite(in_b
.at(i
), ez
->vec_add(tmp
, shifted_a
), tmp
);
897 if (port
.do_subtract
)
898 tmp
= ez
->vec_sub(tmp
, in_a
);
900 tmp
= ez
->vec_add(tmp
, in_a
);
904 for (int i
= 0; i
< GetSize(b
); i
++) {
905 std::vector
<int> val(GetSize(y
), ez
->CONST_FALSE
);
907 tmp
= ez
->vec_add(tmp
, val
);
912 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
913 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort("\\B"), timestep
);
915 int undef_any_a
= ez
->expression(ezSAT::OpOr
, undef_a
);
916 int undef_any_b
= ez
->expression(ezSAT::OpOr
, undef_b
);
918 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
919 ez
->assume(ez
->vec_eq(undef_y
, std::vector
<int>(GetSize(y
), ez
->OR(undef_any_a
, undef_any_b
))));
921 undefGating(y
, tmp
, undef_y
);
924 ez
->assume(ez
->vec_eq(y
, tmp
));
929 if (cell
->type
== "$div" || cell
->type
== "$mod")
931 std::vector
<int> a
= importDefSigSpec(cell
->getPort("\\A"), timestep
);
932 std::vector
<int> b
= importDefSigSpec(cell
->getPort("\\B"), timestep
);
933 std::vector
<int> y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
934 extendSignalWidth(a
, b
, y
, cell
);
936 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
938 std::vector
<int> a_u
, b_u
;
939 if (cell
->parameters
["\\A_SIGNED"].as_bool() && cell
->parameters
["\\B_SIGNED"].as_bool()) {
940 a_u
= ez
->vec_ite(a
.back(), ez
->vec_neg(a
), a
);
941 b_u
= ez
->vec_ite(b
.back(), ez
->vec_neg(b
), b
);
947 std::vector
<int> chain_buf
= a_u
;
948 std::vector
<int> y_u(a_u
.size(), ez
->CONST_FALSE
);
949 for (int i
= int(a
.size())-1; i
>= 0; i
--)
951 chain_buf
.insert(chain_buf
.end(), chain_buf
.size(), ez
->CONST_FALSE
);
953 std::vector
<int> b_shl(i
, ez
->CONST_FALSE
);
954 b_shl
.insert(b_shl
.end(), b_u
.begin(), b_u
.end());
955 b_shl
.insert(b_shl
.end(), chain_buf
.size()-b_shl
.size(), ez
->CONST_FALSE
);
957 y_u
.at(i
) = ez
->vec_ge_unsigned(chain_buf
, b_shl
);
958 chain_buf
= ez
->vec_ite(y_u
.at(i
), ez
->vec_sub(chain_buf
, b_shl
), chain_buf
);
960 chain_buf
.erase(chain_buf
.begin() + a_u
.size(), chain_buf
.end());
963 std::vector
<int> y_tmp
= ignore_div_by_zero
? yy
: ez
->vec_var(y
.size());
964 if (cell
->type
== "$div") {
965 if (cell
->parameters
["\\A_SIGNED"].as_bool() && cell
->parameters
["\\B_SIGNED"].as_bool())
966 ez
->assume(ez
->vec_eq(y_tmp
, ez
->vec_ite(ez
->XOR(a
.back(), b
.back()), ez
->vec_neg(y_u
), y_u
)));
968 ez
->assume(ez
->vec_eq(y_tmp
, y_u
));
970 if (cell
->parameters
["\\A_SIGNED"].as_bool() && cell
->parameters
["\\B_SIGNED"].as_bool())
971 ez
->assume(ez
->vec_eq(y_tmp
, ez
->vec_ite(a
.back(), ez
->vec_neg(chain_buf
), chain_buf
)));
973 ez
->assume(ez
->vec_eq(y_tmp
, chain_buf
));
976 if (ignore_div_by_zero
) {
977 ez
->assume(ez
->expression(ezSAT::OpOr
, b
));
979 std::vector
<int> div_zero_result
;
980 if (cell
->type
== "$div") {
981 if (cell
->parameters
["\\A_SIGNED"].as_bool() && cell
->parameters
["\\B_SIGNED"].as_bool()) {
982 std::vector
<int> all_ones(y
.size(), ez
->CONST_TRUE
);
983 std::vector
<int> only_first_one(y
.size(), ez
->CONST_FALSE
);
984 only_first_one
.at(0) = ez
->CONST_TRUE
;
985 div_zero_result
= ez
->vec_ite(a
.back(), only_first_one
, all_ones
);
987 div_zero_result
.insert(div_zero_result
.end(), cell
->getPort("\\A").size(), ez
->CONST_TRUE
);
988 div_zero_result
.insert(div_zero_result
.end(), y
.size() - div_zero_result
.size(), ez
->CONST_FALSE
);
991 int copy_a_bits
= min(cell
->getPort("\\A").size(), cell
->getPort("\\B").size());
992 div_zero_result
.insert(div_zero_result
.end(), a
.begin(), a
.begin() + copy_a_bits
);
993 if (cell
->parameters
["\\A_SIGNED"].as_bool() && cell
->parameters
["\\B_SIGNED"].as_bool())
994 div_zero_result
.insert(div_zero_result
.end(), y
.size() - div_zero_result
.size(), div_zero_result
.back());
996 div_zero_result
.insert(div_zero_result
.end(), y
.size() - div_zero_result
.size(), ez
->CONST_FALSE
);
998 ez
->assume(ez
->vec_eq(yy
, ez
->vec_ite(ez
->expression(ezSAT::OpOr
, b
), y_tmp
, div_zero_result
)));
1002 log_assert(arith_undef_handled
);
1003 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
1004 undefGating(y
, yy
, undef_y
);
1009 if (cell
->type
== "$lut")
1011 std::vector
<int> a
= importDefSigSpec(cell
->getPort("\\A"), timestep
);
1012 std::vector
<int> y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
1014 std::vector
<int> lut
;
1015 for (auto bit
: cell
->getParam("\\LUT").bits
)
1016 lut
.push_back(bit
== RTLIL::S1
? ez
->CONST_TRUE
: ez
->CONST_FALSE
);
1017 while (GetSize(lut
) < (1 << GetSize(a
)))
1018 lut
.push_back(ez
->CONST_FALSE
);
1019 lut
.resize(1 << GetSize(a
));
1023 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
1024 std::vector
<int> t(lut
), u(GetSize(t
), ez
->CONST_FALSE
);
1026 for (int i
= GetSize(a
)-1; i
>= 0; i
--)
1028 std::vector
<int> t0(t
.begin(), t
.begin() + GetSize(t
)/2);
1029 std::vector
<int> t1(t
.begin() + GetSize(t
)/2, t
.end());
1031 std::vector
<int> u0(u
.begin(), u
.begin() + GetSize(u
)/2);
1032 std::vector
<int> u1(u
.begin() + GetSize(u
)/2, u
.end());
1034 t
= ez
->vec_ite(a
[i
], t1
, t0
);
1035 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
));
1038 log_assert(GetSize(t
) == 1);
1039 log_assert(GetSize(u
) == 1);
1040 undefGating(y
, t
, u
);
1041 ez
->assume(ez
->vec_eq(importUndefSigSpec(cell
->getPort("\\Y"), timestep
), u
));
1045 std::vector
<int> t
= lut
;
1046 for (int i
= GetSize(a
)-1; i
>= 0; i
--)
1048 std::vector
<int> t0(t
.begin(), t
.begin() + GetSize(t
)/2);
1049 std::vector
<int> t1(t
.begin() + GetSize(t
)/2, t
.end());
1050 t
= ez
->vec_ite(a
[i
], t1
, t0
);
1053 log_assert(GetSize(t
) == 1);
1054 ez
->assume(ez
->vec_eq(y
, t
));
1059 if (cell
->type
== "$sop")
1061 std::vector
<int> a
= importDefSigSpec(cell
->getPort("\\A"), timestep
);
1062 int y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
).at(0);
1064 int width
= cell
->getParam("\\WIDTH").as_int();
1065 int depth
= cell
->getParam("\\DEPTH").as_int();
1067 vector
<State
> table_raw
= cell
->getParam("\\TABLE").bits
;
1068 while (GetSize(table_raw
) < 2*width
*depth
)
1069 table_raw
.push_back(State::S0
);
1071 vector
<vector
<int>> table(depth
);
1073 for (int i
= 0; i
< depth
; i
++)
1074 for (int j
= 0; j
< width
; j
++)
1076 bool pat0
= (table_raw
[2*width
*i
+ 2*j
+ 0] == State::S1
);
1077 bool pat1
= (table_raw
[2*width
*i
+ 2*j
+ 1] == State::S1
);
1080 table
.at(i
).push_back(0);
1081 else if (!pat0
&& pat1
)
1082 table
.at(i
).push_back(1);
1084 table
.at(i
).push_back(-1);
1089 std::vector
<int> products
, undef_products
;
1090 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
1091 int undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
).at(0);
1093 for (int i
= 0; i
< depth
; i
++)
1095 std::vector
<int> cmp_a
, cmp_ua
, cmp_b
;
1097 for (int j
= 0; j
< width
; j
++)
1098 if (table
.at(i
).at(j
) >= 0) {
1099 cmp_a
.push_back(a
.at(j
));
1100 cmp_ua
.push_back(undef_a
.at(j
));
1101 cmp_b
.push_back(table
.at(i
).at(j
) ? ez
->CONST_TRUE
: ez
->CONST_FALSE
);
1104 std::vector
<int> masked_a
= ez
->vec_or(cmp_a
, cmp_ua
);
1105 std::vector
<int> masked_b
= ez
->vec_or(cmp_b
, cmp_ua
);
1107 int masked_eq
= ez
->vec_eq(masked_a
, masked_b
);
1108 int any_undef
= ez
->expression(ezSAT::OpOr
, cmp_ua
);
1110 undef_products
.push_back(ez
->AND(any_undef
, masked_eq
));
1111 products
.push_back(ez
->AND(ez
->NOT(any_undef
), masked_eq
));
1114 int yy
= ez
->expression(ezSAT::OpOr
, products
);
1115 ez
->SET(undef_y
, ez
->AND(ez
->NOT(yy
), ez
->expression(ezSAT::OpOr
, undef_products
)));
1116 undefGating(y
, yy
, undef_y
);
1120 std::vector
<int> products
;
1122 for (int i
= 0; i
< depth
; i
++)
1124 std::vector
<int> cmp_a
, cmp_b
;
1126 for (int j
= 0; j
< width
; j
++)
1127 if (table
.at(i
).at(j
) >= 0) {
1128 cmp_a
.push_back(a
.at(j
));
1129 cmp_b
.push_back(table
.at(i
).at(j
) ? ez
->CONST_TRUE
: ez
->CONST_FALSE
);
1132 products
.push_back(ez
->vec_eq(cmp_a
, cmp_b
));
1135 ez
->SET(y
, ez
->expression(ezSAT::OpOr
, products
));
1141 if (cell
->type
== "$fa")
1143 std::vector
<int> a
= importDefSigSpec(cell
->getPort("\\A"), timestep
);
1144 std::vector
<int> b
= importDefSigSpec(cell
->getPort("\\B"), timestep
);
1145 std::vector
<int> c
= importDefSigSpec(cell
->getPort("\\C"), timestep
);
1146 std::vector
<int> y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
1147 std::vector
<int> x
= importDefSigSpec(cell
->getPort("\\X"), timestep
);
1149 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
1150 std::vector
<int> xx
= model_undef
? ez
->vec_var(x
.size()) : x
;
1152 std::vector
<int> t1
= ez
->vec_xor(a
, b
);
1153 ez
->assume(ez
->vec_eq(yy
, ez
->vec_xor(t1
, c
)));
1155 std::vector
<int> t2
= ez
->vec_and(a
, b
);
1156 std::vector
<int> t3
= ez
->vec_and(c
, t1
);
1157 ez
->assume(ez
->vec_eq(xx
, ez
->vec_or(t2
, t3
)));
1161 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
1162 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort("\\B"), timestep
);
1163 std::vector
<int> undef_c
= importUndefSigSpec(cell
->getPort("\\C"), timestep
);
1165 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
1166 std::vector
<int> undef_x
= importUndefSigSpec(cell
->getPort("\\X"), timestep
);
1168 ez
->assume(ez
->vec_eq(undef_y
, ez
->vec_or(ez
->vec_or(undef_a
, undef_b
), undef_c
)));
1169 ez
->assume(ez
->vec_eq(undef_x
, undef_y
));
1171 undefGating(y
, yy
, undef_y
);
1172 undefGating(x
, xx
, undef_x
);
1177 if (cell
->type
== "$lcu")
1179 std::vector
<int> p
= importDefSigSpec(cell
->getPort("\\P"), timestep
);
1180 std::vector
<int> g
= importDefSigSpec(cell
->getPort("\\G"), timestep
);
1181 std::vector
<int> ci
= importDefSigSpec(cell
->getPort("\\CI"), timestep
);
1182 std::vector
<int> co
= importDefSigSpec(cell
->getPort("\\CO"), timestep
);
1184 std::vector
<int> yy
= model_undef
? ez
->vec_var(co
.size()) : co
;
1186 for (int i
= 0; i
< GetSize(co
); i
++)
1187 ez
->SET(yy
[i
], ez
->OR(g
[i
], ez
->AND(p
[i
], i
? yy
[i
-1] : ci
[0])));
1191 std::vector
<int> undef_p
= importUndefSigSpec(cell
->getPort("\\P"), timestep
);
1192 std::vector
<int> undef_g
= importUndefSigSpec(cell
->getPort("\\G"), timestep
);
1193 std::vector
<int> undef_ci
= importUndefSigSpec(cell
->getPort("\\CI"), timestep
);
1194 std::vector
<int> undef_co
= importUndefSigSpec(cell
->getPort("\\CO"), timestep
);
1196 int undef_any_p
= ez
->expression(ezSAT::OpOr
, undef_p
);
1197 int undef_any_g
= ez
->expression(ezSAT::OpOr
, undef_g
);
1198 int undef_any_ci
= ez
->expression(ezSAT::OpOr
, undef_ci
);
1199 int undef_co_bit
= ez
->OR(undef_any_p
, undef_any_g
, undef_any_ci
);
1201 std::vector
<int> undef_co_bits(undef_co
.size(), undef_co_bit
);
1202 ez
->assume(ez
->vec_eq(undef_co_bits
, undef_co
));
1204 undefGating(co
, yy
, undef_co
);
1209 if (cell
->type
== "$alu")
1211 std::vector
<int> a
= importDefSigSpec(cell
->getPort("\\A"), timestep
);
1212 std::vector
<int> b
= importDefSigSpec(cell
->getPort("\\B"), timestep
);
1213 std::vector
<int> y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
1214 std::vector
<int> x
= importDefSigSpec(cell
->getPort("\\X"), timestep
);
1215 std::vector
<int> ci
= importDefSigSpec(cell
->getPort("\\CI"), timestep
);
1216 std::vector
<int> bi
= importDefSigSpec(cell
->getPort("\\BI"), timestep
);
1217 std::vector
<int> co
= importDefSigSpec(cell
->getPort("\\CO"), timestep
);
1219 extendSignalWidth(a
, b
, y
, cell
);
1220 extendSignalWidth(a
, b
, x
, cell
);
1221 extendSignalWidth(a
, b
, co
, cell
);
1223 std::vector
<int> def_y
= model_undef
? ez
->vec_var(y
.size()) : y
;
1224 std::vector
<int> def_x
= model_undef
? ez
->vec_var(x
.size()) : x
;
1225 std::vector
<int> def_co
= model_undef
? ez
->vec_var(co
.size()) : co
;
1227 log_assert(GetSize(y
) == GetSize(x
));
1228 log_assert(GetSize(y
) == GetSize(co
));
1229 log_assert(GetSize(ci
) == 1);
1230 log_assert(GetSize(bi
) == 1);
1232 for (int i
= 0; i
< GetSize(y
); i
++)
1234 int s1
= a
.at(i
), s2
= ez
->XOR(b
.at(i
), bi
.at(0)), s3
= i
? co
.at(i
-1) : ci
.at(0);
1235 ez
->SET(def_x
.at(i
), ez
->XOR(s1
, s2
));
1236 ez
->SET(def_y
.at(i
), ez
->XOR(def_x
.at(i
), s3
));
1237 ez
->SET(def_co
.at(i
), ez
->OR(ez
->AND(s1
, s2
), ez
->AND(s1
, s3
), ez
->AND(s2
, s3
)));
1242 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
1243 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort("\\B"), timestep
);
1244 std::vector
<int> undef_ci
= importUndefSigSpec(cell
->getPort("\\CI"), timestep
);
1245 std::vector
<int> undef_bi
= importUndefSigSpec(cell
->getPort("\\BI"), timestep
);
1247 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
1248 std::vector
<int> undef_x
= importUndefSigSpec(cell
->getPort("\\X"), timestep
);
1249 std::vector
<int> undef_co
= importUndefSigSpec(cell
->getPort("\\CO"), timestep
);
1251 extendSignalWidth(undef_a
, undef_b
, undef_y
, cell
);
1252 extendSignalWidth(undef_a
, undef_b
, undef_x
, cell
);
1253 extendSignalWidth(undef_a
, undef_b
, undef_co
, cell
);
1255 std::vector
<int> all_inputs_undef
;
1256 all_inputs_undef
.insert(all_inputs_undef
.end(), undef_a
.begin(), undef_a
.end());
1257 all_inputs_undef
.insert(all_inputs_undef
.end(), undef_b
.begin(), undef_b
.end());
1258 all_inputs_undef
.insert(all_inputs_undef
.end(), undef_ci
.begin(), undef_ci
.end());
1259 all_inputs_undef
.insert(all_inputs_undef
.end(), undef_bi
.begin(), undef_bi
.end());
1260 int undef_any
= ez
->expression(ezSAT::OpOr
, all_inputs_undef
);
1262 for (int i
= 0; i
< GetSize(undef_y
); i
++) {
1263 ez
->SET(undef_y
.at(i
), undef_any
);
1264 ez
->SET(undef_x
.at(i
), ez
->OR(undef_a
.at(i
), undef_b
.at(i
), undef_bi
.at(0)));
1265 ez
->SET(undef_co
.at(i
), undef_any
);
1268 undefGating(y
, def_y
, undef_y
);
1269 undefGating(x
, def_x
, undef_x
);
1270 undefGating(co
, def_co
, undef_co
);
1275 if (cell
->type
== "$slice")
1277 RTLIL::SigSpec a
= cell
->getPort("\\A");
1278 RTLIL::SigSpec y
= cell
->getPort("\\Y");
1279 ez
->assume(signals_eq(a
.extract(cell
->parameters
.at("\\OFFSET").as_int(), y
.size()), y
, timestep
));
1283 if (cell
->type
== "$concat")
1285 RTLIL::SigSpec a
= cell
->getPort("\\A");
1286 RTLIL::SigSpec b
= cell
->getPort("\\B");
1287 RTLIL::SigSpec y
= cell
->getPort("\\Y");
1289 RTLIL::SigSpec ab
= a
;
1292 ez
->assume(signals_eq(ab
, y
, timestep
));
1296 if (timestep
> 0 && cell
->type
.in("$ff", "$dff", "$_FF_", "$_DFF_N_", "$_DFF_P_"))
1300 initial_state
.add((*sigmap
)(cell
->getPort("\\Q")));
1304 std::vector
<int> d
= importDefSigSpec(cell
->getPort("\\D"), timestep
-1);
1305 std::vector
<int> q
= importDefSigSpec(cell
->getPort("\\Q"), timestep
);
1307 std::vector
<int> qq
= model_undef
? ez
->vec_var(q
.size()) : q
;
1308 ez
->assume(ez
->vec_eq(d
, qq
));
1312 std::vector
<int> undef_d
= importUndefSigSpec(cell
->getPort("\\D"), timestep
-1);
1313 std::vector
<int> undef_q
= importUndefSigSpec(cell
->getPort("\\Q"), timestep
);
1315 ez
->assume(ez
->vec_eq(undef_d
, undef_q
));
1316 undefGating(q
, qq
, undef_q
);
1322 if (cell
->type
== "$anyconst")
1327 std::vector
<int> d
= importDefSigSpec(cell
->getPort("\\Y"), timestep
-1);
1328 std::vector
<int> q
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
1330 std::vector
<int> qq
= model_undef
? ez
->vec_var(q
.size()) : q
;
1331 ez
->assume(ez
->vec_eq(d
, qq
));
1335 std::vector
<int> undef_d
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
-1);
1336 std::vector
<int> undef_q
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
1338 ez
->assume(ez
->vec_eq(undef_d
, undef_q
));
1339 undefGating(q
, qq
, undef_q
);
1344 if (cell
->type
== "$anyseq")
1349 if (cell
->type
== "$_BUF_" || cell
->type
== "$equiv")
1351 std::vector
<int> a
= importDefSigSpec(cell
->getPort("\\A"), timestep
);
1352 std::vector
<int> y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
1353 extendSignalWidthUnary(a
, y
, cell
);
1355 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
1356 ez
->assume(ez
->vec_eq(a
, yy
));
1359 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
1360 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
1361 extendSignalWidthUnary(undef_a
, undef_y
, cell
, false);
1362 ez
->assume(ez
->vec_eq(undef_a
, undef_y
));
1363 undefGating(y
, yy
, undef_y
);
1368 if (cell
->type
== "$initstate")
1370 auto key
= make_pair(prefix
, timestep
);
1371 if (initstates
.count(key
) == 0)
1372 initstates
[key
] = false;
1374 std::vector
<int> y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
1375 log_assert(GetSize(y
) == 1);
1376 ez
->SET(y
[0], initstates
[key
] ? ez
->CONST_TRUE
: ez
->CONST_FALSE
);
1379 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
1380 log_assert(GetSize(undef_y
) == 1);
1381 ez
->SET(undef_y
[0], ez
->CONST_FALSE
);
1387 if (cell
->type
== "$assert")
1389 std::string pf
= prefix
+ (timestep
== -1 ? "" : stringf("@%d:", timestep
));
1390 asserts_a
[pf
].append((*sigmap
)(cell
->getPort("\\A")));
1391 asserts_en
[pf
].append((*sigmap
)(cell
->getPort("\\EN")));
1395 if (cell
->type
== "$assume")
1397 std::string pf
= prefix
+ (timestep
== -1 ? "" : stringf("@%d:", timestep
));
1398 assumes_a
[pf
].append((*sigmap
)(cell
->getPort("\\A")));
1399 assumes_en
[pf
].append((*sigmap
)(cell
->getPort("\\EN")));
1403 // Unsupported internal cell types: $pow $lut
1404 // .. and all sequential cells except $dff and $_DFF_[NP]_