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_", "$_ANDNOT_", "$_ORNOT_",
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
== "$_ANDNOT_")
336 ez
->assume(ez
->vec_eq(ez
->vec_and(a
, ez
->vec_not(b
)), yy
));
337 if (cell
->type
== "$_ORNOT_")
338 ez
->assume(ez
->vec_eq(ez
->vec_or(a
, ez
->vec_not(b
)), yy
));
339 if (cell
->type
== "$add")
340 ez
->assume(ez
->vec_eq(ez
->vec_add(a
, b
), yy
));
341 if (cell
->type
== "$sub")
342 ez
->assume(ez
->vec_eq(ez
->vec_sub(a
, b
), yy
));
344 if (model_undef
&& !arith_undef_handled
)
346 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
347 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort("\\B"), timestep
);
348 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
349 extendSignalWidth(undef_a
, undef_b
, undef_y
, cell
, false);
351 if (cell
->type
.in("$and", "$_AND_", "$_NAND_")) {
352 std::vector
<int> a0
= ez
->vec_and(ez
->vec_not(a
), ez
->vec_not(undef_a
));
353 std::vector
<int> b0
= ez
->vec_and(ez
->vec_not(b
), ez
->vec_not(undef_b
));
354 std::vector
<int> yX
= ez
->vec_and(ez
->vec_or(undef_a
, undef_b
), ez
->vec_not(ez
->vec_or(a0
, b0
)));
355 ez
->assume(ez
->vec_eq(yX
, undef_y
));
357 else if (cell
->type
.in("$or", "$_OR_", "$_NOR_")) {
358 std::vector
<int> a1
= ez
->vec_and(a
, ez
->vec_not(undef_a
));
359 std::vector
<int> b1
= ez
->vec_and(b
, ez
->vec_not(undef_b
));
360 std::vector
<int> yX
= ez
->vec_and(ez
->vec_or(undef_a
, undef_b
), ez
->vec_not(ez
->vec_or(a1
, b1
)));
361 ez
->assume(ez
->vec_eq(yX
, undef_y
));
363 else if (cell
->type
.in("$xor", "$xnor", "$_XOR_", "$_XNOR_")) {
364 std::vector
<int> yX
= ez
->vec_or(undef_a
, undef_b
);
365 ez
->assume(ez
->vec_eq(yX
, undef_y
));
367 else if (cell
->type
== "$_ANDNOT_") {
368 std::vector
<int> a0
= ez
->vec_and(ez
->vec_not(a
), ez
->vec_not(undef_a
));
369 std::vector
<int> b1
= ez
->vec_and(b
, ez
->vec_not(undef_b
));
370 std::vector
<int> yX
= ez
->vec_and(ez
->vec_or(undef_a
, undef_b
), ez
->vec_not(ez
->vec_or(a0
, b1
)));
371 ez
->assume(ez
->vec_eq(yX
, undef_y
));
374 else if (cell
->type
== "$_ORNOT_") {
375 std::vector
<int> a1
= ez
->vec_and(a
, ez
->vec_not(undef_a
));
376 std::vector
<int> b0
= ez
->vec_and(ez
->vec_not(b
), ez
->vec_not(undef_b
));
377 std::vector
<int> yX
= ez
->vec_and(ez
->vec_or(undef_a
, undef_b
), ez
->vec_not(ez
->vec_or(a1
, b0
)));
378 ez
->assume(ez
->vec_eq(yX
, undef_y
));
383 undefGating(y
, yy
, undef_y
);
385 else if (model_undef
)
387 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
388 undefGating(y
, yy
, undef_y
);
393 if (cell
->type
.in("$_AOI3_", "$_OAI3_", "$_AOI4_", "$_OAI4_"))
395 bool aoi_mode
= cell
->type
.in("$_AOI3_", "$_AOI4_");
396 bool three_mode
= cell
->type
.in("$_AOI3_", "$_OAI3_");
398 int a
= importDefSigSpec(cell
->getPort("\\A"), timestep
).at(0);
399 int b
= importDefSigSpec(cell
->getPort("\\B"), timestep
).at(0);
400 int c
= importDefSigSpec(cell
->getPort("\\C"), timestep
).at(0);
401 int d
= three_mode
? (aoi_mode
? ez
->CONST_TRUE
: ez
->CONST_FALSE
) : importDefSigSpec(cell
->getPort("\\D"), timestep
).at(0);
402 int y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
).at(0);
403 int yy
= model_undef
? ez
->literal() : y
;
405 if (cell
->type
.in("$_AOI3_", "$_AOI4_"))
406 ez
->assume(ez
->IFF(ez
->NOT(ez
->OR(ez
->AND(a
, b
), ez
->AND(c
, d
))), yy
));
408 ez
->assume(ez
->IFF(ez
->NOT(ez
->AND(ez
->OR(a
, b
), ez
->OR(c
, d
))), yy
));
412 int undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
).at(0);
413 int undef_b
= importUndefSigSpec(cell
->getPort("\\B"), timestep
).at(0);
414 int undef_c
= importUndefSigSpec(cell
->getPort("\\C"), timestep
).at(0);
415 int undef_d
= three_mode
? ez
->CONST_FALSE
: importUndefSigSpec(cell
->getPort("\\D"), timestep
).at(0);
416 int undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
).at(0);
420 int a0
= ez
->AND(ez
->NOT(a
), ez
->NOT(undef_a
));
421 int b0
= ez
->AND(ez
->NOT(b
), ez
->NOT(undef_b
));
422 int c0
= ez
->AND(ez
->NOT(c
), ez
->NOT(undef_c
));
423 int d0
= ez
->AND(ez
->NOT(d
), ez
->NOT(undef_d
));
425 int ab
= ez
->AND(a
, b
), cd
= ez
->AND(c
, d
);
426 int undef_ab
= ez
->AND(ez
->OR(undef_a
, undef_b
), ez
->NOT(ez
->OR(a0
, b0
)));
427 int undef_cd
= ez
->AND(ez
->OR(undef_c
, undef_d
), ez
->NOT(ez
->OR(c0
, d0
)));
429 int ab1
= ez
->AND(ab
, ez
->NOT(undef_ab
));
430 int cd1
= ez
->AND(cd
, ez
->NOT(undef_cd
));
431 int yX
= ez
->AND(ez
->OR(undef_ab
, undef_cd
), ez
->NOT(ez
->OR(ab1
, cd1
)));
433 ez
->assume(ez
->IFF(yX
, undef_y
));
437 int a1
= ez
->AND(a
, ez
->NOT(undef_a
));
438 int b1
= ez
->AND(b
, ez
->NOT(undef_b
));
439 int c1
= ez
->AND(c
, ez
->NOT(undef_c
));
440 int d1
= ez
->AND(d
, ez
->NOT(undef_d
));
442 int ab
= ez
->OR(a
, b
), cd
= ez
->OR(c
, d
);
443 int undef_ab
= ez
->AND(ez
->OR(undef_a
, undef_b
), ez
->NOT(ez
->OR(a1
, b1
)));
444 int undef_cd
= ez
->AND(ez
->OR(undef_c
, undef_d
), ez
->NOT(ez
->OR(c1
, d1
)));
446 int ab0
= ez
->AND(ez
->NOT(ab
), ez
->NOT(undef_ab
));
447 int cd0
= ez
->AND(ez
->NOT(cd
), ez
->NOT(undef_cd
));
448 int yX
= ez
->AND(ez
->OR(undef_ab
, undef_cd
), ez
->NOT(ez
->OR(ab0
, cd0
)));
450 ez
->assume(ez
->IFF(yX
, undef_y
));
453 undefGating(y
, yy
, undef_y
);
459 if (cell
->type
== "$_NOT_" || cell
->type
== "$not")
461 std::vector
<int> a
= importDefSigSpec(cell
->getPort("\\A"), timestep
);
462 std::vector
<int> y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
463 extendSignalWidthUnary(a
, y
, cell
);
465 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
466 ez
->assume(ez
->vec_eq(ez
->vec_not(a
), yy
));
469 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
470 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
471 extendSignalWidthUnary(undef_a
, undef_y
, cell
, false);
472 ez
->assume(ez
->vec_eq(undef_a
, undef_y
));
473 undefGating(y
, yy
, undef_y
);
478 if (cell
->type
== "$_MUX_" || cell
->type
== "$mux" || cell
->type
== "$_NMUX_")
480 std::vector
<int> a
= importDefSigSpec(cell
->getPort("\\A"), timestep
);
481 std::vector
<int> b
= importDefSigSpec(cell
->getPort("\\B"), timestep
);
482 std::vector
<int> s
= importDefSigSpec(cell
->getPort("\\S"), timestep
);
483 std::vector
<int> y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
485 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
486 if (cell
->type
== "$_NMUX_")
487 ez
->assume(ez
->vec_eq(ez
->vec_not(ez
->vec_ite(s
.at(0), b
, a
)), yy
));
489 ez
->assume(ez
->vec_eq(ez
->vec_ite(s
.at(0), b
, a
), yy
));
493 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
494 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort("\\B"), timestep
);
495 std::vector
<int> undef_s
= importUndefSigSpec(cell
->getPort("\\S"), timestep
);
496 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
498 std::vector
<int> unequal_ab
= ez
->vec_not(ez
->vec_iff(a
, b
));
499 std::vector
<int> undef_ab
= ez
->vec_or(unequal_ab
, ez
->vec_or(undef_a
, undef_b
));
500 std::vector
<int> yX
= ez
->vec_ite(undef_s
.at(0), undef_ab
, ez
->vec_ite(s
.at(0), undef_b
, undef_a
));
501 ez
->assume(ez
->vec_eq(yX
, undef_y
));
502 undefGating(y
, yy
, undef_y
);
507 if (cell
->type
== "$pmux")
509 std::vector
<int> a
= importDefSigSpec(cell
->getPort("\\A"), timestep
);
510 std::vector
<int> b
= importDefSigSpec(cell
->getPort("\\B"), timestep
);
511 std::vector
<int> s
= importDefSigSpec(cell
->getPort("\\S"), timestep
);
512 std::vector
<int> y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
514 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
516 std::vector
<int> tmp
= a
;
517 for (size_t i
= 0; i
< s
.size(); i
++) {
518 std::vector
<int> part_of_b(b
.begin()+i
*a
.size(), b
.begin()+(i
+1)*a
.size());
519 tmp
= ez
->vec_ite(s
.at(i
), part_of_b
, tmp
);
521 ez
->assume(ez
->vec_eq(tmp
, yy
));
525 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
526 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort("\\B"), timestep
);
527 std::vector
<int> undef_s
= importUndefSigSpec(cell
->getPort("\\S"), timestep
);
528 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
530 int maybe_a
= ez
->CONST_TRUE
;
532 std::vector
<int> bits_set
= std::vector
<int>(undef_y
.size(), ez
->CONST_FALSE
);
533 std::vector
<int> bits_clr
= std::vector
<int>(undef_y
.size(), ez
->CONST_FALSE
);
535 for (size_t i
= 0; i
< s
.size(); i
++)
537 std::vector
<int> part_of_b(b
.begin()+i
*a
.size(), b
.begin()+(i
+1)*a
.size());
538 std::vector
<int> part_of_undef_b(undef_b
.begin()+i
*a
.size(), undef_b
.begin()+(i
+1)*a
.size());
540 int maybe_s
= ez
->OR(s
.at(i
), undef_s
.at(i
));
541 int sure_s
= ez
->AND(s
.at(i
), ez
->NOT(undef_s
.at(i
)));
543 maybe_a
= ez
->AND(maybe_a
, ez
->NOT(sure_s
));
545 bits_set
= ez
->vec_ite(maybe_s
, ez
->vec_or(bits_set
, ez
->vec_or(part_of_b
, part_of_undef_b
)), bits_set
);
546 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
);
549 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
);
550 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
);
552 ez
->assume(ez
->vec_eq(ez
->vec_not(ez
->vec_xor(bits_set
, bits_clr
)), undef_y
));
553 undefGating(y
, yy
, undef_y
);
558 if (cell
->type
== "$pos" || cell
->type
== "$neg")
560 std::vector
<int> a
= importDefSigSpec(cell
->getPort("\\A"), timestep
);
561 std::vector
<int> y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
562 extendSignalWidthUnary(a
, y
, cell
);
564 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
566 if (cell
->type
== "$pos") {
567 ez
->assume(ez
->vec_eq(a
, yy
));
569 std::vector
<int> zero(a
.size(), ez
->CONST_FALSE
);
570 ez
->assume(ez
->vec_eq(ez
->vec_sub(zero
, a
), yy
));
575 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
576 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
577 extendSignalWidthUnary(undef_a
, undef_y
, cell
);
579 if (cell
->type
== "$pos") {
580 ez
->assume(ez
->vec_eq(undef_a
, undef_y
));
582 int undef_any_a
= ez
->expression(ezSAT::OpOr
, undef_a
);
583 std::vector
<int> undef_y_bits(undef_y
.size(), undef_any_a
);
584 ez
->assume(ez
->vec_eq(undef_y_bits
, undef_y
));
587 undefGating(y
, yy
, undef_y
);
592 if (cell
->type
== "$reduce_and" || cell
->type
== "$reduce_or" || cell
->type
== "$reduce_xor" ||
593 cell
->type
== "$reduce_xnor" || cell
->type
== "$reduce_bool" || cell
->type
== "$logic_not")
595 std::vector
<int> a
= importDefSigSpec(cell
->getPort("\\A"), timestep
);
596 std::vector
<int> y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
598 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
600 if (cell
->type
== "$reduce_and")
601 ez
->SET(ez
->expression(ez
->OpAnd
, a
), yy
.at(0));
602 if (cell
->type
== "$reduce_or" || cell
->type
== "$reduce_bool")
603 ez
->SET(ez
->expression(ez
->OpOr
, a
), yy
.at(0));
604 if (cell
->type
== "$reduce_xor")
605 ez
->SET(ez
->expression(ez
->OpXor
, a
), yy
.at(0));
606 if (cell
->type
== "$reduce_xnor")
607 ez
->SET(ez
->NOT(ez
->expression(ez
->OpXor
, a
)), yy
.at(0));
608 if (cell
->type
== "$logic_not")
609 ez
->SET(ez
->NOT(ez
->expression(ez
->OpOr
, a
)), yy
.at(0));
610 for (size_t i
= 1; i
< y
.size(); i
++)
611 ez
->SET(ez
->CONST_FALSE
, yy
.at(i
));
615 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
616 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
617 int aX
= ez
->expression(ezSAT::OpOr
, undef_a
);
619 if (cell
->type
== "$reduce_and") {
620 int a0
= ez
->expression(ezSAT::OpOr
, ez
->vec_and(ez
->vec_not(a
), ez
->vec_not(undef_a
)));
621 ez
->assume(ez
->IFF(ez
->AND(ez
->NOT(a0
), aX
), undef_y
.at(0)));
623 else if (cell
->type
== "$reduce_or" || cell
->type
== "$reduce_bool" || cell
->type
== "$logic_not") {
624 int a1
= ez
->expression(ezSAT::OpOr
, ez
->vec_and(a
, ez
->vec_not(undef_a
)));
625 ez
->assume(ez
->IFF(ez
->AND(ez
->NOT(a1
), aX
), undef_y
.at(0)));
627 else if (cell
->type
== "$reduce_xor" || cell
->type
== "$reduce_xnor") {
628 ez
->assume(ez
->IFF(aX
, undef_y
.at(0)));
632 for (size_t i
= 1; i
< undef_y
.size(); i
++)
633 ez
->SET(ez
->CONST_FALSE
, undef_y
.at(i
));
635 undefGating(y
, yy
, undef_y
);
640 if (cell
->type
== "$logic_and" || cell
->type
== "$logic_or")
642 std::vector
<int> vec_a
= importDefSigSpec(cell
->getPort("\\A"), timestep
);
643 std::vector
<int> vec_b
= importDefSigSpec(cell
->getPort("\\B"), timestep
);
645 int a
= ez
->expression(ez
->OpOr
, vec_a
);
646 int b
= ez
->expression(ez
->OpOr
, vec_b
);
647 std::vector
<int> y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
649 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
651 if (cell
->type
== "$logic_and")
652 ez
->SET(ez
->expression(ez
->OpAnd
, a
, b
), yy
.at(0));
654 ez
->SET(ez
->expression(ez
->OpOr
, a
, b
), yy
.at(0));
655 for (size_t i
= 1; i
< y
.size(); i
++)
656 ez
->SET(ez
->CONST_FALSE
, yy
.at(i
));
660 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
661 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort("\\B"), timestep
);
662 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
664 int a0
= ez
->NOT(ez
->OR(ez
->expression(ezSAT::OpOr
, vec_a
), ez
->expression(ezSAT::OpOr
, undef_a
)));
665 int b0
= ez
->NOT(ez
->OR(ez
->expression(ezSAT::OpOr
, vec_b
), ez
->expression(ezSAT::OpOr
, undef_b
)));
666 int a1
= ez
->expression(ezSAT::OpOr
, ez
->vec_and(vec_a
, ez
->vec_not(undef_a
)));
667 int b1
= ez
->expression(ezSAT::OpOr
, ez
->vec_and(vec_b
, ez
->vec_not(undef_b
)));
668 int aX
= ez
->expression(ezSAT::OpOr
, undef_a
);
669 int bX
= ez
->expression(ezSAT::OpOr
, undef_b
);
671 if (cell
->type
== "$logic_and")
672 ez
->SET(ez
->AND(ez
->OR(aX
, bX
), ez
->NOT(ez
->AND(a1
, b1
)), ez
->NOT(a0
), ez
->NOT(b0
)), undef_y
.at(0));
673 else if (cell
->type
== "$logic_or")
674 ez
->SET(ez
->AND(ez
->OR(aX
, bX
), ez
->NOT(ez
->AND(a0
, b0
)), ez
->NOT(a1
), ez
->NOT(b1
)), undef_y
.at(0));
678 for (size_t i
= 1; i
< undef_y
.size(); i
++)
679 ez
->SET(ez
->CONST_FALSE
, undef_y
.at(i
));
681 undefGating(y
, yy
, undef_y
);
686 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")
688 bool is_signed
= cell
->parameters
["\\A_SIGNED"].as_bool() && cell
->parameters
["\\B_SIGNED"].as_bool();
689 std::vector
<int> a
= importDefSigSpec(cell
->getPort("\\A"), timestep
);
690 std::vector
<int> b
= importDefSigSpec(cell
->getPort("\\B"), timestep
);
691 std::vector
<int> y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
692 extendSignalWidth(a
, b
, cell
);
694 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
696 if (model_undef
&& (cell
->type
== "$eqx" || cell
->type
== "$nex")) {
697 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
698 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort("\\B"), timestep
);
699 extendSignalWidth(undef_a
, undef_b
, cell
, true);
700 a
= ez
->vec_or(a
, undef_a
);
701 b
= ez
->vec_or(b
, undef_b
);
704 if (cell
->type
== "$lt")
705 ez
->SET(is_signed
? ez
->vec_lt_signed(a
, b
) : ez
->vec_lt_unsigned(a
, b
), yy
.at(0));
706 if (cell
->type
== "$le")
707 ez
->SET(is_signed
? ez
->vec_le_signed(a
, b
) : ez
->vec_le_unsigned(a
, b
), yy
.at(0));
708 if (cell
->type
== "$eq" || cell
->type
== "$eqx")
709 ez
->SET(ez
->vec_eq(a
, b
), yy
.at(0));
710 if (cell
->type
== "$ne" || cell
->type
== "$nex")
711 ez
->SET(ez
->vec_ne(a
, b
), yy
.at(0));
712 if (cell
->type
== "$ge")
713 ez
->SET(is_signed
? ez
->vec_ge_signed(a
, b
) : ez
->vec_ge_unsigned(a
, b
), yy
.at(0));
714 if (cell
->type
== "$gt")
715 ez
->SET(is_signed
? ez
->vec_gt_signed(a
, b
) : ez
->vec_gt_unsigned(a
, b
), yy
.at(0));
716 for (size_t i
= 1; i
< y
.size(); i
++)
717 ez
->SET(ez
->CONST_FALSE
, yy
.at(i
));
719 if (model_undef
&& (cell
->type
== "$eqx" || cell
->type
== "$nex"))
721 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
722 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort("\\B"), timestep
);
723 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
724 extendSignalWidth(undef_a
, undef_b
, cell
, true);
726 if (cell
->type
== "$eqx")
727 yy
.at(0) = ez
->AND(yy
.at(0), ez
->vec_eq(undef_a
, undef_b
));
729 yy
.at(0) = ez
->OR(yy
.at(0), ez
->vec_ne(undef_a
, undef_b
));
731 for (size_t i
= 0; i
< y
.size(); i
++)
732 ez
->SET(ez
->CONST_FALSE
, undef_y
.at(i
));
734 ez
->assume(ez
->vec_eq(y
, yy
));
736 else if (model_undef
&& (cell
->type
== "$eq" || cell
->type
== "$ne"))
738 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
739 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort("\\B"), timestep
);
740 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
741 extendSignalWidth(undef_a
, undef_b
, cell
, true);
743 int undef_any_a
= ez
->expression(ezSAT::OpOr
, undef_a
);
744 int undef_any_b
= ez
->expression(ezSAT::OpOr
, undef_b
);
745 int undef_any
= ez
->OR(undef_any_a
, undef_any_b
);
747 std::vector
<int> masked_a_bits
= ez
->vec_or(a
, ez
->vec_or(undef_a
, undef_b
));
748 std::vector
<int> masked_b_bits
= ez
->vec_or(b
, ez
->vec_or(undef_a
, undef_b
));
750 int masked_ne
= ez
->vec_ne(masked_a_bits
, masked_b_bits
);
751 int undef_y_bit
= ez
->AND(undef_any
, ez
->NOT(masked_ne
));
753 for (size_t i
= 1; i
< undef_y
.size(); i
++)
754 ez
->SET(ez
->CONST_FALSE
, undef_y
.at(i
));
755 ez
->SET(undef_y_bit
, undef_y
.at(0));
757 undefGating(y
, yy
, undef_y
);
762 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
763 undefGating(y
, yy
, undef_y
);
765 log_assert(!model_undef
|| arith_undef_handled
);
770 if (cell
->type
== "$shl" || cell
->type
== "$shr" || cell
->type
== "$sshl" || cell
->type
== "$sshr" || cell
->type
== "$shift" || cell
->type
== "$shiftx")
772 std::vector
<int> a
= importDefSigSpec(cell
->getPort("\\A"), timestep
);
773 std::vector
<int> b
= importDefSigSpec(cell
->getPort("\\B"), timestep
);
774 std::vector
<int> y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
776 int extend_bit
= ez
->CONST_FALSE
;
778 if (!cell
->type
.in("$shift", "$shiftx") && cell
->parameters
["\\A_SIGNED"].as_bool())
779 extend_bit
= a
.back();
781 while (y
.size() < a
.size())
782 y
.push_back(ez
->literal());
783 while (y
.size() > a
.size())
784 a
.push_back(extend_bit
);
786 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
787 std::vector
<int> shifted_a
;
789 if (cell
->type
== "$shl" || cell
->type
== "$sshl")
790 shifted_a
= ez
->vec_shift_left(a
, b
, false, ez
->CONST_FALSE
, ez
->CONST_FALSE
);
792 if (cell
->type
== "$shr")
793 shifted_a
= ez
->vec_shift_right(a
, b
, false, ez
->CONST_FALSE
, ez
->CONST_FALSE
);
795 if (cell
->type
== "$sshr")
796 shifted_a
= ez
->vec_shift_right(a
, b
, false, cell
->parameters
["\\A_SIGNED"].as_bool() ? a
.back() : ez
->CONST_FALSE
, ez
->CONST_FALSE
);
798 if (cell
->type
== "$shift" || cell
->type
== "$shiftx")
799 shifted_a
= ez
->vec_shift_right(a
, b
, cell
->parameters
["\\B_SIGNED"].as_bool(), ez
->CONST_FALSE
, ez
->CONST_FALSE
);
801 ez
->assume(ez
->vec_eq(shifted_a
, yy
));
805 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
806 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort("\\B"), timestep
);
807 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
808 std::vector
<int> undef_a_shifted
;
810 extend_bit
= cell
->type
== "$shiftx" ? ez
->CONST_TRUE
: ez
->CONST_FALSE
;
811 if (!cell
->type
.in("$shift", "$shiftx") && cell
->parameters
["\\A_SIGNED"].as_bool())
812 extend_bit
= undef_a
.back();
814 while (undef_y
.size() < undef_a
.size())
815 undef_y
.push_back(ez
->literal());
816 while (undef_y
.size() > undef_a
.size())
817 undef_a
.push_back(extend_bit
);
819 if (cell
->type
== "$shl" || cell
->type
== "$sshl")
820 undef_a_shifted
= ez
->vec_shift_left(undef_a
, b
, false, ez
->CONST_FALSE
, ez
->CONST_FALSE
);
822 if (cell
->type
== "$shr")
823 undef_a_shifted
= ez
->vec_shift_right(undef_a
, b
, false, ez
->CONST_FALSE
, ez
->CONST_FALSE
);
825 if (cell
->type
== "$sshr")
826 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
);
828 if (cell
->type
== "$shift")
829 undef_a_shifted
= ez
->vec_shift_right(undef_a
, b
, cell
->parameters
["\\B_SIGNED"].as_bool(), ez
->CONST_FALSE
, ez
->CONST_FALSE
);
831 if (cell
->type
== "$shiftx")
832 undef_a_shifted
= ez
->vec_shift_right(undef_a
, b
, cell
->parameters
["\\B_SIGNED"].as_bool(), ez
->CONST_TRUE
, ez
->CONST_TRUE
);
834 int undef_any_b
= ez
->expression(ezSAT::OpOr
, undef_b
);
835 std::vector
<int> undef_all_y_bits(undef_y
.size(), undef_any_b
);
836 ez
->assume(ez
->vec_eq(ez
->vec_or(undef_a_shifted
, undef_all_y_bits
), undef_y
));
837 undefGating(y
, yy
, undef_y
);
842 if (cell
->type
== "$mul")
844 std::vector
<int> a
= importDefSigSpec(cell
->getPort("\\A"), timestep
);
845 std::vector
<int> b
= importDefSigSpec(cell
->getPort("\\B"), timestep
);
846 std::vector
<int> y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
847 extendSignalWidth(a
, b
, y
, cell
);
849 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
851 std::vector
<int> tmp(a
.size(), ez
->CONST_FALSE
);
852 for (int i
= 0; i
< int(a
.size()); i
++)
854 std::vector
<int> shifted_a(a
.size(), ez
->CONST_FALSE
);
855 for (int j
= i
; j
< int(a
.size()); j
++)
856 shifted_a
.at(j
) = a
.at(j
-i
);
857 tmp
= ez
->vec_ite(b
.at(i
), ez
->vec_add(tmp
, shifted_a
), tmp
);
859 ez
->assume(ez
->vec_eq(tmp
, yy
));
862 log_assert(arith_undef_handled
);
863 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
864 undefGating(y
, yy
, undef_y
);
869 if (cell
->type
== "$macc")
871 std::vector
<int> a
= importDefSigSpec(cell
->getPort("\\A"), timestep
);
872 std::vector
<int> b
= importDefSigSpec(cell
->getPort("\\B"), timestep
);
873 std::vector
<int> y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
876 macc
.from_cell(cell
);
878 std::vector
<int> tmp(GetSize(y
), ez
->CONST_FALSE
);
880 for (auto &port
: macc
.ports
)
882 std::vector
<int> in_a
= importDefSigSpec(port
.in_a
, timestep
);
883 std::vector
<int> in_b
= importDefSigSpec(port
.in_b
, timestep
);
885 while (GetSize(in_a
) < GetSize(y
))
886 in_a
.push_back(port
.is_signed
&& !in_a
.empty() ? in_a
.back() : ez
->CONST_FALSE
);
887 in_a
.resize(GetSize(y
));
891 while (GetSize(in_b
) < GetSize(y
))
892 in_b
.push_back(port
.is_signed
&& !in_b
.empty() ? in_b
.back() : ez
->CONST_FALSE
);
893 in_b
.resize(GetSize(y
));
895 for (int i
= 0; i
< GetSize(in_b
); i
++) {
896 std::vector
<int> shifted_a(in_a
.size(), ez
->CONST_FALSE
);
897 for (int j
= i
; j
< int(in_a
.size()); j
++)
898 shifted_a
.at(j
) = in_a
.at(j
-i
);
899 if (port
.do_subtract
)
900 tmp
= ez
->vec_ite(in_b
.at(i
), ez
->vec_sub(tmp
, shifted_a
), tmp
);
902 tmp
= ez
->vec_ite(in_b
.at(i
), ez
->vec_add(tmp
, shifted_a
), tmp
);
907 if (port
.do_subtract
)
908 tmp
= ez
->vec_sub(tmp
, in_a
);
910 tmp
= ez
->vec_add(tmp
, in_a
);
914 for (int i
= 0; i
< GetSize(b
); i
++) {
915 std::vector
<int> val(GetSize(y
), ez
->CONST_FALSE
);
917 tmp
= ez
->vec_add(tmp
, val
);
922 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
923 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort("\\B"), timestep
);
925 int undef_any_a
= ez
->expression(ezSAT::OpOr
, undef_a
);
926 int undef_any_b
= ez
->expression(ezSAT::OpOr
, undef_b
);
928 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
929 ez
->assume(ez
->vec_eq(undef_y
, std::vector
<int>(GetSize(y
), ez
->OR(undef_any_a
, undef_any_b
))));
931 undefGating(y
, tmp
, undef_y
);
934 ez
->assume(ez
->vec_eq(y
, tmp
));
939 if (cell
->type
== "$div" || cell
->type
== "$mod")
941 std::vector
<int> a
= importDefSigSpec(cell
->getPort("\\A"), timestep
);
942 std::vector
<int> b
= importDefSigSpec(cell
->getPort("\\B"), timestep
);
943 std::vector
<int> y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
944 extendSignalWidth(a
, b
, y
, cell
);
946 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
948 std::vector
<int> a_u
, b_u
;
949 if (cell
->parameters
["\\A_SIGNED"].as_bool() && cell
->parameters
["\\B_SIGNED"].as_bool()) {
950 a_u
= ez
->vec_ite(a
.back(), ez
->vec_neg(a
), a
);
951 b_u
= ez
->vec_ite(b
.back(), ez
->vec_neg(b
), b
);
957 std::vector
<int> chain_buf
= a_u
;
958 std::vector
<int> y_u(a_u
.size(), ez
->CONST_FALSE
);
959 for (int i
= int(a
.size())-1; i
>= 0; i
--)
961 chain_buf
.insert(chain_buf
.end(), chain_buf
.size(), ez
->CONST_FALSE
);
963 std::vector
<int> b_shl(i
, ez
->CONST_FALSE
);
964 b_shl
.insert(b_shl
.end(), b_u
.begin(), b_u
.end());
965 b_shl
.insert(b_shl
.end(), chain_buf
.size()-b_shl
.size(), ez
->CONST_FALSE
);
967 y_u
.at(i
) = ez
->vec_ge_unsigned(chain_buf
, b_shl
);
968 chain_buf
= ez
->vec_ite(y_u
.at(i
), ez
->vec_sub(chain_buf
, b_shl
), chain_buf
);
970 chain_buf
.erase(chain_buf
.begin() + a_u
.size(), chain_buf
.end());
973 std::vector
<int> y_tmp
= ignore_div_by_zero
? yy
: ez
->vec_var(y
.size());
974 if (cell
->type
== "$div") {
975 if (cell
->parameters
["\\A_SIGNED"].as_bool() && cell
->parameters
["\\B_SIGNED"].as_bool())
976 ez
->assume(ez
->vec_eq(y_tmp
, ez
->vec_ite(ez
->XOR(a
.back(), b
.back()), ez
->vec_neg(y_u
), y_u
)));
978 ez
->assume(ez
->vec_eq(y_tmp
, y_u
));
980 if (cell
->parameters
["\\A_SIGNED"].as_bool() && cell
->parameters
["\\B_SIGNED"].as_bool())
981 ez
->assume(ez
->vec_eq(y_tmp
, ez
->vec_ite(a
.back(), ez
->vec_neg(chain_buf
), chain_buf
)));
983 ez
->assume(ez
->vec_eq(y_tmp
, chain_buf
));
986 if (ignore_div_by_zero
) {
987 ez
->assume(ez
->expression(ezSAT::OpOr
, b
));
989 std::vector
<int> div_zero_result
;
990 if (cell
->type
== "$div") {
991 if (cell
->parameters
["\\A_SIGNED"].as_bool() && cell
->parameters
["\\B_SIGNED"].as_bool()) {
992 std::vector
<int> all_ones(y
.size(), ez
->CONST_TRUE
);
993 std::vector
<int> only_first_one(y
.size(), ez
->CONST_FALSE
);
994 only_first_one
.at(0) = ez
->CONST_TRUE
;
995 div_zero_result
= ez
->vec_ite(a
.back(), only_first_one
, all_ones
);
997 div_zero_result
.insert(div_zero_result
.end(), cell
->getPort("\\A").size(), ez
->CONST_TRUE
);
998 div_zero_result
.insert(div_zero_result
.end(), y
.size() - div_zero_result
.size(), ez
->CONST_FALSE
);
1001 int copy_a_bits
= min(cell
->getPort("\\A").size(), cell
->getPort("\\B").size());
1002 div_zero_result
.insert(div_zero_result
.end(), a
.begin(), a
.begin() + copy_a_bits
);
1003 if (cell
->parameters
["\\A_SIGNED"].as_bool() && cell
->parameters
["\\B_SIGNED"].as_bool())
1004 div_zero_result
.insert(div_zero_result
.end(), y
.size() - div_zero_result
.size(), div_zero_result
.back());
1006 div_zero_result
.insert(div_zero_result
.end(), y
.size() - div_zero_result
.size(), ez
->CONST_FALSE
);
1008 ez
->assume(ez
->vec_eq(yy
, ez
->vec_ite(ez
->expression(ezSAT::OpOr
, b
), y_tmp
, div_zero_result
)));
1012 log_assert(arith_undef_handled
);
1013 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
1014 undefGating(y
, yy
, undef_y
);
1019 if (cell
->type
== "$lut")
1021 std::vector
<int> a
= importDefSigSpec(cell
->getPort("\\A"), timestep
);
1022 std::vector
<int> y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
1024 std::vector
<int> lut
;
1025 for (auto bit
: cell
->getParam("\\LUT").bits
)
1026 lut
.push_back(bit
== State::S1
? ez
->CONST_TRUE
: ez
->CONST_FALSE
);
1027 while (GetSize(lut
) < (1 << GetSize(a
)))
1028 lut
.push_back(ez
->CONST_FALSE
);
1029 lut
.resize(1 << GetSize(a
));
1033 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
1034 std::vector
<int> t(lut
), u(GetSize(t
), ez
->CONST_FALSE
);
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());
1041 std::vector
<int> u0(u
.begin(), u
.begin() + GetSize(u
)/2);
1042 std::vector
<int> u1(u
.begin() + GetSize(u
)/2, u
.end());
1044 t
= ez
->vec_ite(a
[i
], t1
, t0
);
1045 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
));
1048 log_assert(GetSize(t
) == 1);
1049 log_assert(GetSize(u
) == 1);
1050 undefGating(y
, t
, u
);
1051 ez
->assume(ez
->vec_eq(importUndefSigSpec(cell
->getPort("\\Y"), timestep
), u
));
1055 std::vector
<int> t
= lut
;
1056 for (int i
= GetSize(a
)-1; i
>= 0; i
--)
1058 std::vector
<int> t0(t
.begin(), t
.begin() + GetSize(t
)/2);
1059 std::vector
<int> t1(t
.begin() + GetSize(t
)/2, t
.end());
1060 t
= ez
->vec_ite(a
[i
], t1
, t0
);
1063 log_assert(GetSize(t
) == 1);
1064 ez
->assume(ez
->vec_eq(y
, t
));
1069 if (cell
->type
== "$sop")
1071 std::vector
<int> a
= importDefSigSpec(cell
->getPort("\\A"), timestep
);
1072 int y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
).at(0);
1074 int width
= cell
->getParam("\\WIDTH").as_int();
1075 int depth
= cell
->getParam("\\DEPTH").as_int();
1077 vector
<State
> table_raw
= cell
->getParam("\\TABLE").bits
;
1078 while (GetSize(table_raw
) < 2*width
*depth
)
1079 table_raw
.push_back(State::S0
);
1081 vector
<vector
<int>> table(depth
);
1083 for (int i
= 0; i
< depth
; i
++)
1084 for (int j
= 0; j
< width
; j
++)
1086 bool pat0
= (table_raw
[2*width
*i
+ 2*j
+ 0] == State::S1
);
1087 bool pat1
= (table_raw
[2*width
*i
+ 2*j
+ 1] == State::S1
);
1090 table
.at(i
).push_back(0);
1091 else if (!pat0
&& pat1
)
1092 table
.at(i
).push_back(1);
1094 table
.at(i
).push_back(-1);
1099 std::vector
<int> products
, undef_products
;
1100 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
1101 int undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
).at(0);
1103 for (int i
= 0; i
< depth
; i
++)
1105 std::vector
<int> cmp_a
, cmp_ua
, cmp_b
;
1107 for (int j
= 0; j
< width
; j
++)
1108 if (table
.at(i
).at(j
) >= 0) {
1109 cmp_a
.push_back(a
.at(j
));
1110 cmp_ua
.push_back(undef_a
.at(j
));
1111 cmp_b
.push_back(table
.at(i
).at(j
) ? ez
->CONST_TRUE
: ez
->CONST_FALSE
);
1114 std::vector
<int> masked_a
= ez
->vec_or(cmp_a
, cmp_ua
);
1115 std::vector
<int> masked_b
= ez
->vec_or(cmp_b
, cmp_ua
);
1117 int masked_eq
= ez
->vec_eq(masked_a
, masked_b
);
1118 int any_undef
= ez
->expression(ezSAT::OpOr
, cmp_ua
);
1120 undef_products
.push_back(ez
->AND(any_undef
, masked_eq
));
1121 products
.push_back(ez
->AND(ez
->NOT(any_undef
), masked_eq
));
1124 int yy
= ez
->expression(ezSAT::OpOr
, products
);
1125 ez
->SET(undef_y
, ez
->AND(ez
->NOT(yy
), ez
->expression(ezSAT::OpOr
, undef_products
)));
1126 undefGating(y
, yy
, undef_y
);
1130 std::vector
<int> products
;
1132 for (int i
= 0; i
< depth
; i
++)
1134 std::vector
<int> cmp_a
, cmp_b
;
1136 for (int j
= 0; j
< width
; j
++)
1137 if (table
.at(i
).at(j
) >= 0) {
1138 cmp_a
.push_back(a
.at(j
));
1139 cmp_b
.push_back(table
.at(i
).at(j
) ? ez
->CONST_TRUE
: ez
->CONST_FALSE
);
1142 products
.push_back(ez
->vec_eq(cmp_a
, cmp_b
));
1145 ez
->SET(y
, ez
->expression(ezSAT::OpOr
, products
));
1151 if (cell
->type
== "$fa")
1153 std::vector
<int> a
= importDefSigSpec(cell
->getPort("\\A"), timestep
);
1154 std::vector
<int> b
= importDefSigSpec(cell
->getPort("\\B"), timestep
);
1155 std::vector
<int> c
= importDefSigSpec(cell
->getPort("\\C"), timestep
);
1156 std::vector
<int> y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
1157 std::vector
<int> x
= importDefSigSpec(cell
->getPort("\\X"), timestep
);
1159 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
1160 std::vector
<int> xx
= model_undef
? ez
->vec_var(x
.size()) : x
;
1162 std::vector
<int> t1
= ez
->vec_xor(a
, b
);
1163 ez
->assume(ez
->vec_eq(yy
, ez
->vec_xor(t1
, c
)));
1165 std::vector
<int> t2
= ez
->vec_and(a
, b
);
1166 std::vector
<int> t3
= ez
->vec_and(c
, t1
);
1167 ez
->assume(ez
->vec_eq(xx
, ez
->vec_or(t2
, t3
)));
1171 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
1172 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort("\\B"), timestep
);
1173 std::vector
<int> undef_c
= importUndefSigSpec(cell
->getPort("\\C"), timestep
);
1175 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
1176 std::vector
<int> undef_x
= importUndefSigSpec(cell
->getPort("\\X"), timestep
);
1178 ez
->assume(ez
->vec_eq(undef_y
, ez
->vec_or(ez
->vec_or(undef_a
, undef_b
), undef_c
)));
1179 ez
->assume(ez
->vec_eq(undef_x
, undef_y
));
1181 undefGating(y
, yy
, undef_y
);
1182 undefGating(x
, xx
, undef_x
);
1187 if (cell
->type
== "$lcu")
1189 std::vector
<int> p
= importDefSigSpec(cell
->getPort("\\P"), timestep
);
1190 std::vector
<int> g
= importDefSigSpec(cell
->getPort("\\G"), timestep
);
1191 std::vector
<int> ci
= importDefSigSpec(cell
->getPort("\\CI"), timestep
);
1192 std::vector
<int> co
= importDefSigSpec(cell
->getPort("\\CO"), timestep
);
1194 std::vector
<int> yy
= model_undef
? ez
->vec_var(co
.size()) : co
;
1196 for (int i
= 0; i
< GetSize(co
); i
++)
1197 ez
->SET(yy
[i
], ez
->OR(g
[i
], ez
->AND(p
[i
], i
? yy
[i
-1] : ci
[0])));
1201 std::vector
<int> undef_p
= importUndefSigSpec(cell
->getPort("\\P"), timestep
);
1202 std::vector
<int> undef_g
= importUndefSigSpec(cell
->getPort("\\G"), timestep
);
1203 std::vector
<int> undef_ci
= importUndefSigSpec(cell
->getPort("\\CI"), timestep
);
1204 std::vector
<int> undef_co
= importUndefSigSpec(cell
->getPort("\\CO"), timestep
);
1206 int undef_any_p
= ez
->expression(ezSAT::OpOr
, undef_p
);
1207 int undef_any_g
= ez
->expression(ezSAT::OpOr
, undef_g
);
1208 int undef_any_ci
= ez
->expression(ezSAT::OpOr
, undef_ci
);
1209 int undef_co_bit
= ez
->OR(undef_any_p
, undef_any_g
, undef_any_ci
);
1211 std::vector
<int> undef_co_bits(undef_co
.size(), undef_co_bit
);
1212 ez
->assume(ez
->vec_eq(undef_co_bits
, undef_co
));
1214 undefGating(co
, yy
, undef_co
);
1219 if (cell
->type
== "$alu")
1221 std::vector
<int> a
= importDefSigSpec(cell
->getPort("\\A"), timestep
);
1222 std::vector
<int> b
= importDefSigSpec(cell
->getPort("\\B"), timestep
);
1223 std::vector
<int> y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
1224 std::vector
<int> x
= importDefSigSpec(cell
->getPort("\\X"), timestep
);
1225 std::vector
<int> ci
= importDefSigSpec(cell
->getPort("\\CI"), timestep
);
1226 std::vector
<int> bi
= importDefSigSpec(cell
->getPort("\\BI"), timestep
);
1227 std::vector
<int> co
= importDefSigSpec(cell
->getPort("\\CO"), timestep
);
1229 extendSignalWidth(a
, b
, y
, cell
);
1230 extendSignalWidth(a
, b
, x
, cell
);
1231 extendSignalWidth(a
, b
, co
, cell
);
1233 std::vector
<int> def_y
= model_undef
? ez
->vec_var(y
.size()) : y
;
1234 std::vector
<int> def_x
= model_undef
? ez
->vec_var(x
.size()) : x
;
1235 std::vector
<int> def_co
= model_undef
? ez
->vec_var(co
.size()) : co
;
1237 log_assert(GetSize(y
) == GetSize(x
));
1238 log_assert(GetSize(y
) == GetSize(co
));
1239 log_assert(GetSize(ci
) == 1);
1240 log_assert(GetSize(bi
) == 1);
1242 for (int i
= 0; i
< GetSize(y
); i
++)
1244 int s1
= a
.at(i
), s2
= ez
->XOR(b
.at(i
), bi
.at(0)), s3
= i
? co
.at(i
-1) : ci
.at(0);
1245 ez
->SET(def_x
.at(i
), ez
->XOR(s1
, s2
));
1246 ez
->SET(def_y
.at(i
), ez
->XOR(def_x
.at(i
), s3
));
1247 ez
->SET(def_co
.at(i
), ez
->OR(ez
->AND(s1
, s2
), ez
->AND(s1
, s3
), ez
->AND(s2
, s3
)));
1252 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
1253 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort("\\B"), timestep
);
1254 std::vector
<int> undef_ci
= importUndefSigSpec(cell
->getPort("\\CI"), timestep
);
1255 std::vector
<int> undef_bi
= importUndefSigSpec(cell
->getPort("\\BI"), timestep
);
1257 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
1258 std::vector
<int> undef_x
= importUndefSigSpec(cell
->getPort("\\X"), timestep
);
1259 std::vector
<int> undef_co
= importUndefSigSpec(cell
->getPort("\\CO"), timestep
);
1261 extendSignalWidth(undef_a
, undef_b
, undef_y
, cell
);
1262 extendSignalWidth(undef_a
, undef_b
, undef_x
, cell
);
1263 extendSignalWidth(undef_a
, undef_b
, undef_co
, cell
);
1265 std::vector
<int> all_inputs_undef
;
1266 all_inputs_undef
.insert(all_inputs_undef
.end(), undef_a
.begin(), undef_a
.end());
1267 all_inputs_undef
.insert(all_inputs_undef
.end(), undef_b
.begin(), undef_b
.end());
1268 all_inputs_undef
.insert(all_inputs_undef
.end(), undef_ci
.begin(), undef_ci
.end());
1269 all_inputs_undef
.insert(all_inputs_undef
.end(), undef_bi
.begin(), undef_bi
.end());
1270 int undef_any
= ez
->expression(ezSAT::OpOr
, all_inputs_undef
);
1272 for (int i
= 0; i
< GetSize(undef_y
); i
++) {
1273 ez
->SET(undef_y
.at(i
), undef_any
);
1274 ez
->SET(undef_x
.at(i
), ez
->OR(undef_a
.at(i
), undef_b
.at(i
), undef_bi
.at(0)));
1275 ez
->SET(undef_co
.at(i
), undef_any
);
1278 undefGating(y
, def_y
, undef_y
);
1279 undefGating(x
, def_x
, undef_x
);
1280 undefGating(co
, def_co
, undef_co
);
1285 if (cell
->type
== "$slice")
1287 RTLIL::SigSpec a
= cell
->getPort("\\A");
1288 RTLIL::SigSpec y
= cell
->getPort("\\Y");
1289 ez
->assume(signals_eq(a
.extract(cell
->parameters
.at("\\OFFSET").as_int(), y
.size()), y
, timestep
));
1293 if (cell
->type
== "$concat")
1295 RTLIL::SigSpec a
= cell
->getPort("\\A");
1296 RTLIL::SigSpec b
= cell
->getPort("\\B");
1297 RTLIL::SigSpec y
= cell
->getPort("\\Y");
1299 RTLIL::SigSpec ab
= a
;
1302 ez
->assume(signals_eq(ab
, y
, timestep
));
1306 if (timestep
> 0 && cell
->type
.in("$ff", "$dff", "$_FF_", "$_DFF_N_", "$_DFF_P_"))
1310 initial_state
.add((*sigmap
)(cell
->getPort("\\Q")));
1314 std::vector
<int> d
= importDefSigSpec(cell
->getPort("\\D"), timestep
-1);
1315 std::vector
<int> q
= importDefSigSpec(cell
->getPort("\\Q"), timestep
);
1317 std::vector
<int> qq
= model_undef
? ez
->vec_var(q
.size()) : q
;
1318 ez
->assume(ez
->vec_eq(d
, qq
));
1322 std::vector
<int> undef_d
= importUndefSigSpec(cell
->getPort("\\D"), timestep
-1);
1323 std::vector
<int> undef_q
= importUndefSigSpec(cell
->getPort("\\Q"), timestep
);
1325 ez
->assume(ez
->vec_eq(undef_d
, undef_q
));
1326 undefGating(q
, qq
, undef_q
);
1332 if (cell
->type
== "$anyconst")
1337 std::vector
<int> d
= importDefSigSpec(cell
->getPort("\\Y"), timestep
-1);
1338 std::vector
<int> q
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
1340 std::vector
<int> qq
= model_undef
? ez
->vec_var(q
.size()) : q
;
1341 ez
->assume(ez
->vec_eq(d
, qq
));
1345 std::vector
<int> undef_d
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
-1);
1346 std::vector
<int> undef_q
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
1348 ez
->assume(ez
->vec_eq(undef_d
, undef_q
));
1349 undefGating(q
, qq
, undef_q
);
1354 if (cell
->type
== "$anyseq")
1359 if (cell
->type
== "$_BUF_" || cell
->type
== "$equiv")
1361 std::vector
<int> a
= importDefSigSpec(cell
->getPort("\\A"), timestep
);
1362 std::vector
<int> y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
1363 extendSignalWidthUnary(a
, y
, cell
);
1365 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
1366 ez
->assume(ez
->vec_eq(a
, yy
));
1369 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
1370 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
1371 extendSignalWidthUnary(undef_a
, undef_y
, cell
, false);
1372 ez
->assume(ez
->vec_eq(undef_a
, undef_y
));
1373 undefGating(y
, yy
, undef_y
);
1378 if (cell
->type
== "$initstate")
1380 auto key
= make_pair(prefix
, timestep
);
1381 if (initstates
.count(key
) == 0)
1382 initstates
[key
] = false;
1384 std::vector
<int> y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
1385 log_assert(GetSize(y
) == 1);
1386 ez
->SET(y
[0], initstates
[key
] ? ez
->CONST_TRUE
: ez
->CONST_FALSE
);
1389 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
1390 log_assert(GetSize(undef_y
) == 1);
1391 ez
->SET(undef_y
[0], ez
->CONST_FALSE
);
1397 if (cell
->type
== "$assert")
1399 std::string pf
= prefix
+ (timestep
== -1 ? "" : stringf("@%d:", timestep
));
1400 asserts_a
[pf
].append((*sigmap
)(cell
->getPort("\\A")));
1401 asserts_en
[pf
].append((*sigmap
)(cell
->getPort("\\EN")));
1405 if (cell
->type
== "$assume")
1407 std::string pf
= prefix
+ (timestep
== -1 ? "" : stringf("@%d:", timestep
));
1408 assumes_a
[pf
].append((*sigmap
)(cell
->getPort("\\A")));
1409 assumes_en
[pf
].append((*sigmap
)(cell
->getPort("\\EN")));
1413 // Unsupported internal cell types: $pow $lut
1414 // .. and all sequential cells except $dff and $_DFF_[NP]_