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")
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 ez
->assume(ez
->vec_eq(ez
->vec_ite(s
.at(0), b
, a
), yy
));
490 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
491 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort("\\B"), timestep
);
492 std::vector
<int> undef_s
= importUndefSigSpec(cell
->getPort("\\S"), timestep
);
493 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
495 std::vector
<int> unequal_ab
= ez
->vec_not(ez
->vec_iff(a
, b
));
496 std::vector
<int> undef_ab
= ez
->vec_or(unequal_ab
, ez
->vec_or(undef_a
, undef_b
));
497 std::vector
<int> yX
= ez
->vec_ite(undef_s
.at(0), undef_ab
, ez
->vec_ite(s
.at(0), undef_b
, undef_a
));
498 ez
->assume(ez
->vec_eq(yX
, undef_y
));
499 undefGating(y
, yy
, undef_y
);
504 if (cell
->type
== "$pmux")
506 std::vector
<int> a
= importDefSigSpec(cell
->getPort("\\A"), timestep
);
507 std::vector
<int> b
= importDefSigSpec(cell
->getPort("\\B"), timestep
);
508 std::vector
<int> s
= importDefSigSpec(cell
->getPort("\\S"), timestep
);
509 std::vector
<int> y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
511 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
513 std::vector
<int> tmp
= a
;
514 for (size_t i
= 0; i
< s
.size(); i
++) {
515 std::vector
<int> part_of_b(b
.begin()+i
*a
.size(), b
.begin()+(i
+1)*a
.size());
516 tmp
= ez
->vec_ite(s
.at(i
), part_of_b
, tmp
);
518 ez
->assume(ez
->vec_eq(tmp
, yy
));
522 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
523 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort("\\B"), timestep
);
524 std::vector
<int> undef_s
= importUndefSigSpec(cell
->getPort("\\S"), timestep
);
525 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
527 int maybe_a
= ez
->CONST_TRUE
;
529 std::vector
<int> bits_set
= std::vector
<int>(undef_y
.size(), ez
->CONST_FALSE
);
530 std::vector
<int> bits_clr
= std::vector
<int>(undef_y
.size(), ez
->CONST_FALSE
);
532 for (size_t i
= 0; i
< s
.size(); i
++)
534 std::vector
<int> part_of_b(b
.begin()+i
*a
.size(), b
.begin()+(i
+1)*a
.size());
535 std::vector
<int> part_of_undef_b(undef_b
.begin()+i
*a
.size(), undef_b
.begin()+(i
+1)*a
.size());
537 int maybe_s
= ez
->OR(s
.at(i
), undef_s
.at(i
));
538 int sure_s
= ez
->AND(s
.at(i
), ez
->NOT(undef_s
.at(i
)));
540 maybe_a
= ez
->AND(maybe_a
, ez
->NOT(sure_s
));
542 bits_set
= ez
->vec_ite(maybe_s
, ez
->vec_or(bits_set
, ez
->vec_or(part_of_b
, part_of_undef_b
)), bits_set
);
543 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
);
546 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
);
547 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
);
549 ez
->assume(ez
->vec_eq(ez
->vec_not(ez
->vec_xor(bits_set
, bits_clr
)), undef_y
));
550 undefGating(y
, yy
, undef_y
);
555 if (cell
->type
== "$pos" || cell
->type
== "$neg")
557 std::vector
<int> a
= importDefSigSpec(cell
->getPort("\\A"), timestep
);
558 std::vector
<int> y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
559 extendSignalWidthUnary(a
, y
, cell
);
561 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
563 if (cell
->type
== "$pos") {
564 ez
->assume(ez
->vec_eq(a
, yy
));
566 std::vector
<int> zero(a
.size(), ez
->CONST_FALSE
);
567 ez
->assume(ez
->vec_eq(ez
->vec_sub(zero
, a
), yy
));
572 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
573 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
574 extendSignalWidthUnary(undef_a
, undef_y
, cell
);
576 if (cell
->type
== "$pos") {
577 ez
->assume(ez
->vec_eq(undef_a
, undef_y
));
579 int undef_any_a
= ez
->expression(ezSAT::OpOr
, undef_a
);
580 std::vector
<int> undef_y_bits(undef_y
.size(), undef_any_a
);
581 ez
->assume(ez
->vec_eq(undef_y_bits
, undef_y
));
584 undefGating(y
, yy
, undef_y
);
589 if (cell
->type
== "$reduce_and" || cell
->type
== "$reduce_or" || cell
->type
== "$reduce_xor" ||
590 cell
->type
== "$reduce_xnor" || cell
->type
== "$reduce_bool" || cell
->type
== "$logic_not")
592 std::vector
<int> a
= importDefSigSpec(cell
->getPort("\\A"), timestep
);
593 std::vector
<int> y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
595 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
597 if (cell
->type
== "$reduce_and")
598 ez
->SET(ez
->expression(ez
->OpAnd
, a
), yy
.at(0));
599 if (cell
->type
== "$reduce_or" || cell
->type
== "$reduce_bool")
600 ez
->SET(ez
->expression(ez
->OpOr
, a
), yy
.at(0));
601 if (cell
->type
== "$reduce_xor")
602 ez
->SET(ez
->expression(ez
->OpXor
, a
), yy
.at(0));
603 if (cell
->type
== "$reduce_xnor")
604 ez
->SET(ez
->NOT(ez
->expression(ez
->OpXor
, a
)), yy
.at(0));
605 if (cell
->type
== "$logic_not")
606 ez
->SET(ez
->NOT(ez
->expression(ez
->OpOr
, a
)), yy
.at(0));
607 for (size_t i
= 1; i
< y
.size(); i
++)
608 ez
->SET(ez
->CONST_FALSE
, yy
.at(i
));
612 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
613 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
614 int aX
= ez
->expression(ezSAT::OpOr
, undef_a
);
616 if (cell
->type
== "$reduce_and") {
617 int a0
= ez
->expression(ezSAT::OpOr
, ez
->vec_and(ez
->vec_not(a
), ez
->vec_not(undef_a
)));
618 ez
->assume(ez
->IFF(ez
->AND(ez
->NOT(a0
), aX
), undef_y
.at(0)));
620 else if (cell
->type
== "$reduce_or" || cell
->type
== "$reduce_bool" || cell
->type
== "$logic_not") {
621 int a1
= ez
->expression(ezSAT::OpOr
, ez
->vec_and(a
, ez
->vec_not(undef_a
)));
622 ez
->assume(ez
->IFF(ez
->AND(ez
->NOT(a1
), aX
), undef_y
.at(0)));
624 else if (cell
->type
== "$reduce_xor" || cell
->type
== "$reduce_xnor") {
625 ez
->assume(ez
->IFF(aX
, undef_y
.at(0)));
629 for (size_t i
= 1; i
< undef_y
.size(); i
++)
630 ez
->SET(ez
->CONST_FALSE
, undef_y
.at(i
));
632 undefGating(y
, yy
, undef_y
);
637 if (cell
->type
== "$logic_and" || cell
->type
== "$logic_or")
639 std::vector
<int> vec_a
= importDefSigSpec(cell
->getPort("\\A"), timestep
);
640 std::vector
<int> vec_b
= importDefSigSpec(cell
->getPort("\\B"), timestep
);
642 int a
= ez
->expression(ez
->OpOr
, vec_a
);
643 int b
= ez
->expression(ez
->OpOr
, vec_b
);
644 std::vector
<int> y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
646 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
648 if (cell
->type
== "$logic_and")
649 ez
->SET(ez
->expression(ez
->OpAnd
, a
, b
), yy
.at(0));
651 ez
->SET(ez
->expression(ez
->OpOr
, a
, b
), yy
.at(0));
652 for (size_t i
= 1; i
< y
.size(); i
++)
653 ez
->SET(ez
->CONST_FALSE
, yy
.at(i
));
657 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
658 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort("\\B"), timestep
);
659 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
661 int a0
= ez
->NOT(ez
->OR(ez
->expression(ezSAT::OpOr
, vec_a
), ez
->expression(ezSAT::OpOr
, undef_a
)));
662 int b0
= ez
->NOT(ez
->OR(ez
->expression(ezSAT::OpOr
, vec_b
), ez
->expression(ezSAT::OpOr
, undef_b
)));
663 int a1
= ez
->expression(ezSAT::OpOr
, ez
->vec_and(vec_a
, ez
->vec_not(undef_a
)));
664 int b1
= ez
->expression(ezSAT::OpOr
, ez
->vec_and(vec_b
, ez
->vec_not(undef_b
)));
665 int aX
= ez
->expression(ezSAT::OpOr
, undef_a
);
666 int bX
= ez
->expression(ezSAT::OpOr
, undef_b
);
668 if (cell
->type
== "$logic_and")
669 ez
->SET(ez
->AND(ez
->OR(aX
, bX
), ez
->NOT(ez
->AND(a1
, b1
)), ez
->NOT(a0
), ez
->NOT(b0
)), undef_y
.at(0));
670 else if (cell
->type
== "$logic_or")
671 ez
->SET(ez
->AND(ez
->OR(aX
, bX
), ez
->NOT(ez
->AND(a0
, b0
)), ez
->NOT(a1
), ez
->NOT(b1
)), undef_y
.at(0));
675 for (size_t i
= 1; i
< undef_y
.size(); i
++)
676 ez
->SET(ez
->CONST_FALSE
, undef_y
.at(i
));
678 undefGating(y
, yy
, undef_y
);
683 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")
685 bool is_signed
= cell
->parameters
["\\A_SIGNED"].as_bool() && cell
->parameters
["\\B_SIGNED"].as_bool();
686 std::vector
<int> a
= importDefSigSpec(cell
->getPort("\\A"), timestep
);
687 std::vector
<int> b
= importDefSigSpec(cell
->getPort("\\B"), timestep
);
688 std::vector
<int> y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
689 extendSignalWidth(a
, b
, cell
);
691 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
693 if (model_undef
&& (cell
->type
== "$eqx" || cell
->type
== "$nex")) {
694 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
695 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort("\\B"), timestep
);
696 extendSignalWidth(undef_a
, undef_b
, cell
, true);
697 a
= ez
->vec_or(a
, undef_a
);
698 b
= ez
->vec_or(b
, undef_b
);
701 if (cell
->type
== "$lt")
702 ez
->SET(is_signed
? ez
->vec_lt_signed(a
, b
) : ez
->vec_lt_unsigned(a
, b
), yy
.at(0));
703 if (cell
->type
== "$le")
704 ez
->SET(is_signed
? ez
->vec_le_signed(a
, b
) : ez
->vec_le_unsigned(a
, b
), yy
.at(0));
705 if (cell
->type
== "$eq" || cell
->type
== "$eqx")
706 ez
->SET(ez
->vec_eq(a
, b
), yy
.at(0));
707 if (cell
->type
== "$ne" || cell
->type
== "$nex")
708 ez
->SET(ez
->vec_ne(a
, b
), yy
.at(0));
709 if (cell
->type
== "$ge")
710 ez
->SET(is_signed
? ez
->vec_ge_signed(a
, b
) : ez
->vec_ge_unsigned(a
, b
), yy
.at(0));
711 if (cell
->type
== "$gt")
712 ez
->SET(is_signed
? ez
->vec_gt_signed(a
, b
) : ez
->vec_gt_unsigned(a
, b
), yy
.at(0));
713 for (size_t i
= 1; i
< y
.size(); i
++)
714 ez
->SET(ez
->CONST_FALSE
, yy
.at(i
));
716 if (model_undef
&& (cell
->type
== "$eqx" || cell
->type
== "$nex"))
718 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
719 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort("\\B"), timestep
);
720 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
721 extendSignalWidth(undef_a
, undef_b
, cell
, true);
723 if (cell
->type
== "$eqx")
724 yy
.at(0) = ez
->AND(yy
.at(0), ez
->vec_eq(undef_a
, undef_b
));
726 yy
.at(0) = ez
->OR(yy
.at(0), ez
->vec_ne(undef_a
, undef_b
));
728 for (size_t i
= 0; i
< y
.size(); i
++)
729 ez
->SET(ez
->CONST_FALSE
, undef_y
.at(i
));
731 ez
->assume(ez
->vec_eq(y
, yy
));
733 else if (model_undef
&& (cell
->type
== "$eq" || cell
->type
== "$ne"))
735 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
736 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort("\\B"), timestep
);
737 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
738 extendSignalWidth(undef_a
, undef_b
, cell
, true);
740 int undef_any_a
= ez
->expression(ezSAT::OpOr
, undef_a
);
741 int undef_any_b
= ez
->expression(ezSAT::OpOr
, undef_b
);
742 int undef_any
= ez
->OR(undef_any_a
, undef_any_b
);
744 std::vector
<int> masked_a_bits
= ez
->vec_or(a
, ez
->vec_or(undef_a
, undef_b
));
745 std::vector
<int> masked_b_bits
= ez
->vec_or(b
, ez
->vec_or(undef_a
, undef_b
));
747 int masked_ne
= ez
->vec_ne(masked_a_bits
, masked_b_bits
);
748 int undef_y_bit
= ez
->AND(undef_any
, ez
->NOT(masked_ne
));
750 for (size_t i
= 1; i
< undef_y
.size(); i
++)
751 ez
->SET(ez
->CONST_FALSE
, undef_y
.at(i
));
752 ez
->SET(undef_y_bit
, undef_y
.at(0));
754 undefGating(y
, yy
, undef_y
);
759 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
760 undefGating(y
, yy
, undef_y
);
762 log_assert(!model_undef
|| arith_undef_handled
);
767 if (cell
->type
== "$shl" || cell
->type
== "$shr" || cell
->type
== "$sshl" || cell
->type
== "$sshr" || cell
->type
== "$shift" || cell
->type
== "$shiftx")
769 std::vector
<int> a
= importDefSigSpec(cell
->getPort("\\A"), timestep
);
770 std::vector
<int> b
= importDefSigSpec(cell
->getPort("\\B"), timestep
);
771 std::vector
<int> y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
773 int extend_bit
= ez
->CONST_FALSE
;
775 if (!cell
->type
.in("$shift", "$shiftx") && cell
->parameters
["\\A_SIGNED"].as_bool())
776 extend_bit
= a
.back();
778 while (y
.size() < a
.size())
779 y
.push_back(ez
->literal());
780 while (y
.size() > a
.size())
781 a
.push_back(extend_bit
);
783 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
784 std::vector
<int> shifted_a
;
786 if (cell
->type
== "$shl" || cell
->type
== "$sshl")
787 shifted_a
= ez
->vec_shift_left(a
, b
, false, ez
->CONST_FALSE
, ez
->CONST_FALSE
);
789 if (cell
->type
== "$shr")
790 shifted_a
= ez
->vec_shift_right(a
, b
, false, ez
->CONST_FALSE
, ez
->CONST_FALSE
);
792 if (cell
->type
== "$sshr")
793 shifted_a
= ez
->vec_shift_right(a
, b
, false, cell
->parameters
["\\A_SIGNED"].as_bool() ? a
.back() : ez
->CONST_FALSE
, ez
->CONST_FALSE
);
795 if (cell
->type
== "$shift" || cell
->type
== "$shiftx")
796 shifted_a
= ez
->vec_shift_right(a
, b
, cell
->parameters
["\\B_SIGNED"].as_bool(), ez
->CONST_FALSE
, ez
->CONST_FALSE
);
798 ez
->assume(ez
->vec_eq(shifted_a
, yy
));
802 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
803 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort("\\B"), timestep
);
804 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
805 std::vector
<int> undef_a_shifted
;
807 extend_bit
= cell
->type
== "$shiftx" ? ez
->CONST_TRUE
: ez
->CONST_FALSE
;
808 if (!cell
->type
.in("$shift", "$shiftx") && cell
->parameters
["\\A_SIGNED"].as_bool())
809 extend_bit
= undef_a
.back();
811 while (undef_y
.size() < undef_a
.size())
812 undef_y
.push_back(ez
->literal());
813 while (undef_y
.size() > undef_a
.size())
814 undef_a
.push_back(extend_bit
);
816 if (cell
->type
== "$shl" || cell
->type
== "$sshl")
817 undef_a_shifted
= ez
->vec_shift_left(undef_a
, b
, false, ez
->CONST_FALSE
, ez
->CONST_FALSE
);
819 if (cell
->type
== "$shr")
820 undef_a_shifted
= ez
->vec_shift_right(undef_a
, b
, false, ez
->CONST_FALSE
, ez
->CONST_FALSE
);
822 if (cell
->type
== "$sshr")
823 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
);
825 if (cell
->type
== "$shift")
826 undef_a_shifted
= ez
->vec_shift_right(undef_a
, b
, cell
->parameters
["\\B_SIGNED"].as_bool(), ez
->CONST_FALSE
, ez
->CONST_FALSE
);
828 if (cell
->type
== "$shiftx")
829 undef_a_shifted
= ez
->vec_shift_right(undef_a
, b
, cell
->parameters
["\\B_SIGNED"].as_bool(), ez
->CONST_TRUE
, ez
->CONST_TRUE
);
831 int undef_any_b
= ez
->expression(ezSAT::OpOr
, undef_b
);
832 std::vector
<int> undef_all_y_bits(undef_y
.size(), undef_any_b
);
833 ez
->assume(ez
->vec_eq(ez
->vec_or(undef_a_shifted
, undef_all_y_bits
), undef_y
));
834 undefGating(y
, yy
, undef_y
);
839 if (cell
->type
== "$mul")
841 std::vector
<int> a
= importDefSigSpec(cell
->getPort("\\A"), timestep
);
842 std::vector
<int> b
= importDefSigSpec(cell
->getPort("\\B"), timestep
);
843 std::vector
<int> y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
844 extendSignalWidth(a
, b
, y
, cell
);
846 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
848 std::vector
<int> tmp(a
.size(), ez
->CONST_FALSE
);
849 for (int i
= 0; i
< int(a
.size()); i
++)
851 std::vector
<int> shifted_a(a
.size(), ez
->CONST_FALSE
);
852 for (int j
= i
; j
< int(a
.size()); j
++)
853 shifted_a
.at(j
) = a
.at(j
-i
);
854 tmp
= ez
->vec_ite(b
.at(i
), ez
->vec_add(tmp
, shifted_a
), tmp
);
856 ez
->assume(ez
->vec_eq(tmp
, yy
));
859 log_assert(arith_undef_handled
);
860 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
861 undefGating(y
, yy
, undef_y
);
866 if (cell
->type
== "$macc")
868 std::vector
<int> a
= importDefSigSpec(cell
->getPort("\\A"), timestep
);
869 std::vector
<int> b
= importDefSigSpec(cell
->getPort("\\B"), timestep
);
870 std::vector
<int> y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
873 macc
.from_cell(cell
);
875 std::vector
<int> tmp(GetSize(y
), ez
->CONST_FALSE
);
877 for (auto &port
: macc
.ports
)
879 std::vector
<int> in_a
= importDefSigSpec(port
.in_a
, timestep
);
880 std::vector
<int> in_b
= importDefSigSpec(port
.in_b
, timestep
);
882 while (GetSize(in_a
) < GetSize(y
))
883 in_a
.push_back(port
.is_signed
&& !in_a
.empty() ? in_a
.back() : ez
->CONST_FALSE
);
884 in_a
.resize(GetSize(y
));
888 while (GetSize(in_b
) < GetSize(y
))
889 in_b
.push_back(port
.is_signed
&& !in_b
.empty() ? in_b
.back() : ez
->CONST_FALSE
);
890 in_b
.resize(GetSize(y
));
892 for (int i
= 0; i
< GetSize(in_b
); i
++) {
893 std::vector
<int> shifted_a(in_a
.size(), ez
->CONST_FALSE
);
894 for (int j
= i
; j
< int(in_a
.size()); j
++)
895 shifted_a
.at(j
) = in_a
.at(j
-i
);
896 if (port
.do_subtract
)
897 tmp
= ez
->vec_ite(in_b
.at(i
), ez
->vec_sub(tmp
, shifted_a
), tmp
);
899 tmp
= ez
->vec_ite(in_b
.at(i
), ez
->vec_add(tmp
, shifted_a
), tmp
);
904 if (port
.do_subtract
)
905 tmp
= ez
->vec_sub(tmp
, in_a
);
907 tmp
= ez
->vec_add(tmp
, in_a
);
911 for (int i
= 0; i
< GetSize(b
); i
++) {
912 std::vector
<int> val(GetSize(y
), ez
->CONST_FALSE
);
914 tmp
= ez
->vec_add(tmp
, val
);
919 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
920 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort("\\B"), timestep
);
922 int undef_any_a
= ez
->expression(ezSAT::OpOr
, undef_a
);
923 int undef_any_b
= ez
->expression(ezSAT::OpOr
, undef_b
);
925 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
926 ez
->assume(ez
->vec_eq(undef_y
, std::vector
<int>(GetSize(y
), ez
->OR(undef_any_a
, undef_any_b
))));
928 undefGating(y
, tmp
, undef_y
);
931 ez
->assume(ez
->vec_eq(y
, tmp
));
936 if (cell
->type
== "$div" || cell
->type
== "$mod")
938 std::vector
<int> a
= importDefSigSpec(cell
->getPort("\\A"), timestep
);
939 std::vector
<int> b
= importDefSigSpec(cell
->getPort("\\B"), timestep
);
940 std::vector
<int> y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
941 extendSignalWidth(a
, b
, y
, cell
);
943 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
945 std::vector
<int> a_u
, b_u
;
946 if (cell
->parameters
["\\A_SIGNED"].as_bool() && cell
->parameters
["\\B_SIGNED"].as_bool()) {
947 a_u
= ez
->vec_ite(a
.back(), ez
->vec_neg(a
), a
);
948 b_u
= ez
->vec_ite(b
.back(), ez
->vec_neg(b
), b
);
954 std::vector
<int> chain_buf
= a_u
;
955 std::vector
<int> y_u(a_u
.size(), ez
->CONST_FALSE
);
956 for (int i
= int(a
.size())-1; i
>= 0; i
--)
958 chain_buf
.insert(chain_buf
.end(), chain_buf
.size(), ez
->CONST_FALSE
);
960 std::vector
<int> b_shl(i
, ez
->CONST_FALSE
);
961 b_shl
.insert(b_shl
.end(), b_u
.begin(), b_u
.end());
962 b_shl
.insert(b_shl
.end(), chain_buf
.size()-b_shl
.size(), ez
->CONST_FALSE
);
964 y_u
.at(i
) = ez
->vec_ge_unsigned(chain_buf
, b_shl
);
965 chain_buf
= ez
->vec_ite(y_u
.at(i
), ez
->vec_sub(chain_buf
, b_shl
), chain_buf
);
967 chain_buf
.erase(chain_buf
.begin() + a_u
.size(), chain_buf
.end());
970 std::vector
<int> y_tmp
= ignore_div_by_zero
? yy
: ez
->vec_var(y
.size());
971 if (cell
->type
== "$div") {
972 if (cell
->parameters
["\\A_SIGNED"].as_bool() && cell
->parameters
["\\B_SIGNED"].as_bool())
973 ez
->assume(ez
->vec_eq(y_tmp
, ez
->vec_ite(ez
->XOR(a
.back(), b
.back()), ez
->vec_neg(y_u
), y_u
)));
975 ez
->assume(ez
->vec_eq(y_tmp
, y_u
));
977 if (cell
->parameters
["\\A_SIGNED"].as_bool() && cell
->parameters
["\\B_SIGNED"].as_bool())
978 ez
->assume(ez
->vec_eq(y_tmp
, ez
->vec_ite(a
.back(), ez
->vec_neg(chain_buf
), chain_buf
)));
980 ez
->assume(ez
->vec_eq(y_tmp
, chain_buf
));
983 if (ignore_div_by_zero
) {
984 ez
->assume(ez
->expression(ezSAT::OpOr
, b
));
986 std::vector
<int> div_zero_result
;
987 if (cell
->type
== "$div") {
988 if (cell
->parameters
["\\A_SIGNED"].as_bool() && cell
->parameters
["\\B_SIGNED"].as_bool()) {
989 std::vector
<int> all_ones(y
.size(), ez
->CONST_TRUE
);
990 std::vector
<int> only_first_one(y
.size(), ez
->CONST_FALSE
);
991 only_first_one
.at(0) = ez
->CONST_TRUE
;
992 div_zero_result
= ez
->vec_ite(a
.back(), only_first_one
, all_ones
);
994 div_zero_result
.insert(div_zero_result
.end(), cell
->getPort("\\A").size(), ez
->CONST_TRUE
);
995 div_zero_result
.insert(div_zero_result
.end(), y
.size() - div_zero_result
.size(), ez
->CONST_FALSE
);
998 int copy_a_bits
= min(cell
->getPort("\\A").size(), cell
->getPort("\\B").size());
999 div_zero_result
.insert(div_zero_result
.end(), a
.begin(), a
.begin() + copy_a_bits
);
1000 if (cell
->parameters
["\\A_SIGNED"].as_bool() && cell
->parameters
["\\B_SIGNED"].as_bool())
1001 div_zero_result
.insert(div_zero_result
.end(), y
.size() - div_zero_result
.size(), div_zero_result
.back());
1003 div_zero_result
.insert(div_zero_result
.end(), y
.size() - div_zero_result
.size(), ez
->CONST_FALSE
);
1005 ez
->assume(ez
->vec_eq(yy
, ez
->vec_ite(ez
->expression(ezSAT::OpOr
, b
), y_tmp
, div_zero_result
)));
1009 log_assert(arith_undef_handled
);
1010 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
1011 undefGating(y
, yy
, undef_y
);
1016 if (cell
->type
== "$lut")
1018 std::vector
<int> a
= importDefSigSpec(cell
->getPort("\\A"), timestep
);
1019 std::vector
<int> y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
1021 std::vector
<int> lut
;
1022 for (auto bit
: cell
->getParam("\\LUT").bits
)
1023 lut
.push_back(bit
== RTLIL::S1
? ez
->CONST_TRUE
: ez
->CONST_FALSE
);
1024 while (GetSize(lut
) < (1 << GetSize(a
)))
1025 lut
.push_back(ez
->CONST_FALSE
);
1026 lut
.resize(1 << GetSize(a
));
1030 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
1031 std::vector
<int> t(lut
), u(GetSize(t
), ez
->CONST_FALSE
);
1033 for (int i
= GetSize(a
)-1; i
>= 0; i
--)
1035 std::vector
<int> t0(t
.begin(), t
.begin() + GetSize(t
)/2);
1036 std::vector
<int> t1(t
.begin() + GetSize(t
)/2, t
.end());
1038 std::vector
<int> u0(u
.begin(), u
.begin() + GetSize(u
)/2);
1039 std::vector
<int> u1(u
.begin() + GetSize(u
)/2, u
.end());
1041 t
= ez
->vec_ite(a
[i
], t1
, t0
);
1042 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
));
1045 log_assert(GetSize(t
) == 1);
1046 log_assert(GetSize(u
) == 1);
1047 undefGating(y
, t
, u
);
1048 ez
->assume(ez
->vec_eq(importUndefSigSpec(cell
->getPort("\\Y"), timestep
), u
));
1052 std::vector
<int> t
= lut
;
1053 for (int i
= GetSize(a
)-1; i
>= 0; i
--)
1055 std::vector
<int> t0(t
.begin(), t
.begin() + GetSize(t
)/2);
1056 std::vector
<int> t1(t
.begin() + GetSize(t
)/2, t
.end());
1057 t
= ez
->vec_ite(a
[i
], t1
, t0
);
1060 log_assert(GetSize(t
) == 1);
1061 ez
->assume(ez
->vec_eq(y
, t
));
1066 if (cell
->type
== "$sop")
1068 std::vector
<int> a
= importDefSigSpec(cell
->getPort("\\A"), timestep
);
1069 int y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
).at(0);
1071 int width
= cell
->getParam("\\WIDTH").as_int();
1072 int depth
= cell
->getParam("\\DEPTH").as_int();
1074 vector
<State
> table_raw
= cell
->getParam("\\TABLE").bits
;
1075 while (GetSize(table_raw
) < 2*width
*depth
)
1076 table_raw
.push_back(State::S0
);
1078 vector
<vector
<int>> table(depth
);
1080 for (int i
= 0; i
< depth
; i
++)
1081 for (int j
= 0; j
< width
; j
++)
1083 bool pat0
= (table_raw
[2*width
*i
+ 2*j
+ 0] == State::S1
);
1084 bool pat1
= (table_raw
[2*width
*i
+ 2*j
+ 1] == State::S1
);
1087 table
.at(i
).push_back(0);
1088 else if (!pat0
&& pat1
)
1089 table
.at(i
).push_back(1);
1091 table
.at(i
).push_back(-1);
1096 std::vector
<int> products
, undef_products
;
1097 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
1098 int undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
).at(0);
1100 for (int i
= 0; i
< depth
; i
++)
1102 std::vector
<int> cmp_a
, cmp_ua
, cmp_b
;
1104 for (int j
= 0; j
< width
; j
++)
1105 if (table
.at(i
).at(j
) >= 0) {
1106 cmp_a
.push_back(a
.at(j
));
1107 cmp_ua
.push_back(undef_a
.at(j
));
1108 cmp_b
.push_back(table
.at(i
).at(j
) ? ez
->CONST_TRUE
: ez
->CONST_FALSE
);
1111 std::vector
<int> masked_a
= ez
->vec_or(cmp_a
, cmp_ua
);
1112 std::vector
<int> masked_b
= ez
->vec_or(cmp_b
, cmp_ua
);
1114 int masked_eq
= ez
->vec_eq(masked_a
, masked_b
);
1115 int any_undef
= ez
->expression(ezSAT::OpOr
, cmp_ua
);
1117 undef_products
.push_back(ez
->AND(any_undef
, masked_eq
));
1118 products
.push_back(ez
->AND(ez
->NOT(any_undef
), masked_eq
));
1121 int yy
= ez
->expression(ezSAT::OpOr
, products
);
1122 ez
->SET(undef_y
, ez
->AND(ez
->NOT(yy
), ez
->expression(ezSAT::OpOr
, undef_products
)));
1123 undefGating(y
, yy
, undef_y
);
1127 std::vector
<int> products
;
1129 for (int i
= 0; i
< depth
; i
++)
1131 std::vector
<int> cmp_a
, cmp_b
;
1133 for (int j
= 0; j
< width
; j
++)
1134 if (table
.at(i
).at(j
) >= 0) {
1135 cmp_a
.push_back(a
.at(j
));
1136 cmp_b
.push_back(table
.at(i
).at(j
) ? ez
->CONST_TRUE
: ez
->CONST_FALSE
);
1139 products
.push_back(ez
->vec_eq(cmp_a
, cmp_b
));
1142 ez
->SET(y
, ez
->expression(ezSAT::OpOr
, products
));
1148 if (cell
->type
== "$fa")
1150 std::vector
<int> a
= importDefSigSpec(cell
->getPort("\\A"), timestep
);
1151 std::vector
<int> b
= importDefSigSpec(cell
->getPort("\\B"), timestep
);
1152 std::vector
<int> c
= importDefSigSpec(cell
->getPort("\\C"), timestep
);
1153 std::vector
<int> y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
1154 std::vector
<int> x
= importDefSigSpec(cell
->getPort("\\X"), timestep
);
1156 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
1157 std::vector
<int> xx
= model_undef
? ez
->vec_var(x
.size()) : x
;
1159 std::vector
<int> t1
= ez
->vec_xor(a
, b
);
1160 ez
->assume(ez
->vec_eq(yy
, ez
->vec_xor(t1
, c
)));
1162 std::vector
<int> t2
= ez
->vec_and(a
, b
);
1163 std::vector
<int> t3
= ez
->vec_and(c
, t1
);
1164 ez
->assume(ez
->vec_eq(xx
, ez
->vec_or(t2
, t3
)));
1168 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
1169 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort("\\B"), timestep
);
1170 std::vector
<int> undef_c
= importUndefSigSpec(cell
->getPort("\\C"), timestep
);
1172 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
1173 std::vector
<int> undef_x
= importUndefSigSpec(cell
->getPort("\\X"), timestep
);
1175 ez
->assume(ez
->vec_eq(undef_y
, ez
->vec_or(ez
->vec_or(undef_a
, undef_b
), undef_c
)));
1176 ez
->assume(ez
->vec_eq(undef_x
, undef_y
));
1178 undefGating(y
, yy
, undef_y
);
1179 undefGating(x
, xx
, undef_x
);
1184 if (cell
->type
== "$lcu")
1186 std::vector
<int> p
= importDefSigSpec(cell
->getPort("\\P"), timestep
);
1187 std::vector
<int> g
= importDefSigSpec(cell
->getPort("\\G"), timestep
);
1188 std::vector
<int> ci
= importDefSigSpec(cell
->getPort("\\CI"), timestep
);
1189 std::vector
<int> co
= importDefSigSpec(cell
->getPort("\\CO"), timestep
);
1191 std::vector
<int> yy
= model_undef
? ez
->vec_var(co
.size()) : co
;
1193 for (int i
= 0; i
< GetSize(co
); i
++)
1194 ez
->SET(yy
[i
], ez
->OR(g
[i
], ez
->AND(p
[i
], i
? yy
[i
-1] : ci
[0])));
1198 std::vector
<int> undef_p
= importUndefSigSpec(cell
->getPort("\\P"), timestep
);
1199 std::vector
<int> undef_g
= importUndefSigSpec(cell
->getPort("\\G"), timestep
);
1200 std::vector
<int> undef_ci
= importUndefSigSpec(cell
->getPort("\\CI"), timestep
);
1201 std::vector
<int> undef_co
= importUndefSigSpec(cell
->getPort("\\CO"), timestep
);
1203 int undef_any_p
= ez
->expression(ezSAT::OpOr
, undef_p
);
1204 int undef_any_g
= ez
->expression(ezSAT::OpOr
, undef_g
);
1205 int undef_any_ci
= ez
->expression(ezSAT::OpOr
, undef_ci
);
1206 int undef_co_bit
= ez
->OR(undef_any_p
, undef_any_g
, undef_any_ci
);
1208 std::vector
<int> undef_co_bits(undef_co
.size(), undef_co_bit
);
1209 ez
->assume(ez
->vec_eq(undef_co_bits
, undef_co
));
1211 undefGating(co
, yy
, undef_co
);
1216 if (cell
->type
== "$alu")
1218 std::vector
<int> a
= importDefSigSpec(cell
->getPort("\\A"), timestep
);
1219 std::vector
<int> b
= importDefSigSpec(cell
->getPort("\\B"), timestep
);
1220 std::vector
<int> y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
1221 std::vector
<int> x
= importDefSigSpec(cell
->getPort("\\X"), timestep
);
1222 std::vector
<int> ci
= importDefSigSpec(cell
->getPort("\\CI"), timestep
);
1223 std::vector
<int> bi
= importDefSigSpec(cell
->getPort("\\BI"), timestep
);
1224 std::vector
<int> co
= importDefSigSpec(cell
->getPort("\\CO"), timestep
);
1226 extendSignalWidth(a
, b
, y
, cell
);
1227 extendSignalWidth(a
, b
, x
, cell
);
1228 extendSignalWidth(a
, b
, co
, cell
);
1230 std::vector
<int> def_y
= model_undef
? ez
->vec_var(y
.size()) : y
;
1231 std::vector
<int> def_x
= model_undef
? ez
->vec_var(x
.size()) : x
;
1232 std::vector
<int> def_co
= model_undef
? ez
->vec_var(co
.size()) : co
;
1234 log_assert(GetSize(y
) == GetSize(x
));
1235 log_assert(GetSize(y
) == GetSize(co
));
1236 log_assert(GetSize(ci
) == 1);
1237 log_assert(GetSize(bi
) == 1);
1239 for (int i
= 0; i
< GetSize(y
); i
++)
1241 int s1
= a
.at(i
), s2
= ez
->XOR(b
.at(i
), bi
.at(0)), s3
= i
? co
.at(i
-1) : ci
.at(0);
1242 ez
->SET(def_x
.at(i
), ez
->XOR(s1
, s2
));
1243 ez
->SET(def_y
.at(i
), ez
->XOR(def_x
.at(i
), s3
));
1244 ez
->SET(def_co
.at(i
), ez
->OR(ez
->AND(s1
, s2
), ez
->AND(s1
, s3
), ez
->AND(s2
, s3
)));
1249 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
1250 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort("\\B"), timestep
);
1251 std::vector
<int> undef_ci
= importUndefSigSpec(cell
->getPort("\\CI"), timestep
);
1252 std::vector
<int> undef_bi
= importUndefSigSpec(cell
->getPort("\\BI"), timestep
);
1254 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
1255 std::vector
<int> undef_x
= importUndefSigSpec(cell
->getPort("\\X"), timestep
);
1256 std::vector
<int> undef_co
= importUndefSigSpec(cell
->getPort("\\CO"), timestep
);
1258 extendSignalWidth(undef_a
, undef_b
, undef_y
, cell
);
1259 extendSignalWidth(undef_a
, undef_b
, undef_x
, cell
);
1260 extendSignalWidth(undef_a
, undef_b
, undef_co
, cell
);
1262 std::vector
<int> all_inputs_undef
;
1263 all_inputs_undef
.insert(all_inputs_undef
.end(), undef_a
.begin(), undef_a
.end());
1264 all_inputs_undef
.insert(all_inputs_undef
.end(), undef_b
.begin(), undef_b
.end());
1265 all_inputs_undef
.insert(all_inputs_undef
.end(), undef_ci
.begin(), undef_ci
.end());
1266 all_inputs_undef
.insert(all_inputs_undef
.end(), undef_bi
.begin(), undef_bi
.end());
1267 int undef_any
= ez
->expression(ezSAT::OpOr
, all_inputs_undef
);
1269 for (int i
= 0; i
< GetSize(undef_y
); i
++) {
1270 ez
->SET(undef_y
.at(i
), undef_any
);
1271 ez
->SET(undef_x
.at(i
), ez
->OR(undef_a
.at(i
), undef_b
.at(i
), undef_bi
.at(0)));
1272 ez
->SET(undef_co
.at(i
), undef_any
);
1275 undefGating(y
, def_y
, undef_y
);
1276 undefGating(x
, def_x
, undef_x
);
1277 undefGating(co
, def_co
, undef_co
);
1282 if (cell
->type
== "$slice")
1284 RTLIL::SigSpec a
= cell
->getPort("\\A");
1285 RTLIL::SigSpec y
= cell
->getPort("\\Y");
1286 ez
->assume(signals_eq(a
.extract(cell
->parameters
.at("\\OFFSET").as_int(), y
.size()), y
, timestep
));
1290 if (cell
->type
== "$concat")
1292 RTLIL::SigSpec a
= cell
->getPort("\\A");
1293 RTLIL::SigSpec b
= cell
->getPort("\\B");
1294 RTLIL::SigSpec y
= cell
->getPort("\\Y");
1296 RTLIL::SigSpec ab
= a
;
1299 ez
->assume(signals_eq(ab
, y
, timestep
));
1303 if (timestep
> 0 && cell
->type
.in("$ff", "$dff", "$_FF_", "$_DFF_N_", "$_DFF_P_"))
1307 initial_state
.add((*sigmap
)(cell
->getPort("\\Q")));
1311 std::vector
<int> d
= importDefSigSpec(cell
->getPort("\\D"), timestep
-1);
1312 std::vector
<int> q
= importDefSigSpec(cell
->getPort("\\Q"), timestep
);
1314 std::vector
<int> qq
= model_undef
? ez
->vec_var(q
.size()) : q
;
1315 ez
->assume(ez
->vec_eq(d
, qq
));
1319 std::vector
<int> undef_d
= importUndefSigSpec(cell
->getPort("\\D"), timestep
-1);
1320 std::vector
<int> undef_q
= importUndefSigSpec(cell
->getPort("\\Q"), timestep
);
1322 ez
->assume(ez
->vec_eq(undef_d
, undef_q
));
1323 undefGating(q
, qq
, undef_q
);
1329 if (cell
->type
== "$anyconst")
1334 std::vector
<int> d
= importDefSigSpec(cell
->getPort("\\Y"), timestep
-1);
1335 std::vector
<int> q
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
1337 std::vector
<int> qq
= model_undef
? ez
->vec_var(q
.size()) : q
;
1338 ez
->assume(ez
->vec_eq(d
, qq
));
1342 std::vector
<int> undef_d
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
-1);
1343 std::vector
<int> undef_q
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
1345 ez
->assume(ez
->vec_eq(undef_d
, undef_q
));
1346 undefGating(q
, qq
, undef_q
);
1351 if (cell
->type
== "$anyseq")
1356 if (cell
->type
== "$_BUF_" || cell
->type
== "$equiv")
1358 std::vector
<int> a
= importDefSigSpec(cell
->getPort("\\A"), timestep
);
1359 std::vector
<int> y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
1360 extendSignalWidthUnary(a
, y
, cell
);
1362 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
1363 ez
->assume(ez
->vec_eq(a
, yy
));
1366 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
1367 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
1368 extendSignalWidthUnary(undef_a
, undef_y
, cell
, false);
1369 ez
->assume(ez
->vec_eq(undef_a
, undef_y
));
1370 undefGating(y
, yy
, undef_y
);
1375 if (cell
->type
== "$initstate")
1377 auto key
= make_pair(prefix
, timestep
);
1378 if (initstates
.count(key
) == 0)
1379 initstates
[key
] = false;
1381 std::vector
<int> y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
1382 log_assert(GetSize(y
) == 1);
1383 ez
->SET(y
[0], initstates
[key
] ? ez
->CONST_TRUE
: ez
->CONST_FALSE
);
1386 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
1387 log_assert(GetSize(undef_y
) == 1);
1388 ez
->SET(undef_y
[0], ez
->CONST_FALSE
);
1394 if (cell
->type
== "$assert")
1396 std::string pf
= prefix
+ (timestep
== -1 ? "" : stringf("@%d:", timestep
));
1397 asserts_a
[pf
].append((*sigmap
)(cell
->getPort("\\A")));
1398 asserts_en
[pf
].append((*sigmap
)(cell
->getPort("\\EN")));
1402 if (cell
->type
== "$assume")
1404 std::string pf
= prefix
+ (timestep
== -1 ? "" : stringf("@%d:", timestep
));
1405 assumes_a
[pf
].append((*sigmap
)(cell
->getPort("\\A")));
1406 assumes_en
[pf
].append((*sigmap
)(cell
->getPort("\\EN")));
1410 // Unsupported internal cell types: $pow $lut
1411 // .. and all sequential cells except $dff and $_DFF_[NP]_