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(ID(A_SIGNED
)) > 0 && cell
->parameters
.count(ID(B_SIGNED
)) > 0)
228 is_signed
= cell
->parameters
[ID(A_SIGNED
)].as_bool() && cell
->parameters
[ID(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(ID(A_SIGNED
)) > 0 && cell
->parameters
[ID(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(ID($lt
), ID($le
), ID($ge
), ID($gt
));
282 if (model_undef
&& (cell
->type
.in(ID($add
), ID($sub
), ID($mul
), ID($div
), ID($mod
)) || is_arith_compare
))
284 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort(ID::A
), timestep
);
285 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort(ID::B
), timestep
);
286 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort(ID::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
.in(ID($div
), ID($mod
))) {
297 std::vector
<int> b
= importSigSpec(cell
->getPort(ID::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(ID($_AND_
), ID($_NAND_
), ID($_OR_
), ID($_NOR_
), ID($_XOR_
), ID($_XNOR_
), ID($_ANDNOT_
), ID($_ORNOT_
),
314 ID($
and), ID($
or), ID($
xor), ID($xnor
), ID($add
), ID($sub
)))
316 std::vector
<int> a
= importDefSigSpec(cell
->getPort(ID::A
), timestep
);
317 std::vector
<int> b
= importDefSigSpec(cell
->getPort(ID::B
), timestep
);
318 std::vector
<int> y
= importDefSigSpec(cell
->getPort(ID::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
.in(ID($
and), ID($_AND_
)))
324 ez
->assume(ez
->vec_eq(ez
->vec_and(a
, b
), yy
));
325 if (cell
->type
== ID($_NAND_
))
326 ez
->assume(ez
->vec_eq(ez
->vec_not(ez
->vec_and(a
, b
)), yy
));
327 if (cell
->type
.in(ID($
or), ID($_OR_
)))
328 ez
->assume(ez
->vec_eq(ez
->vec_or(a
, b
), yy
));
329 if (cell
->type
== ID($_NOR_
))
330 ez
->assume(ez
->vec_eq(ez
->vec_not(ez
->vec_or(a
, b
)), yy
));
331 if (cell
->type
.in(ID($
xor), ID($_XOR_
)))
332 ez
->assume(ez
->vec_eq(ez
->vec_xor(a
, b
), yy
));
333 if (cell
->type
.in(ID($xnor
), ID($_XNOR_
)))
334 ez
->assume(ez
->vec_eq(ez
->vec_not(ez
->vec_xor(a
, b
)), yy
));
335 if (cell
->type
== ID($_ANDNOT_
))
336 ez
->assume(ez
->vec_eq(ez
->vec_and(a
, ez
->vec_not(b
)), yy
));
337 if (cell
->type
== ID($_ORNOT_
))
338 ez
->assume(ez
->vec_eq(ez
->vec_or(a
, ez
->vec_not(b
)), yy
));
339 if (cell
->type
== ID($add
))
340 ez
->assume(ez
->vec_eq(ez
->vec_add(a
, b
), yy
));
341 if (cell
->type
== ID($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(ID::A
), timestep
);
347 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort(ID::B
), timestep
);
348 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort(ID::Y
), timestep
);
349 extendSignalWidth(undef_a
, undef_b
, undef_y
, cell
, false);
351 if (cell
->type
.in(ID($
and), ID($_AND_
), ID($_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(ID($
or), ID($_OR_
), ID($_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(ID($
xor), ID($xnor
), ID($_XOR_
), ID($_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
== ID($_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
== ID($_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(ID::Y
), timestep
);
388 undefGating(y
, yy
, undef_y
);
393 if (cell
->type
.in(ID($_AOI3_
), ID($_OAI3_
), ID($_AOI4_
), ID($_OAI4_
)))
395 bool aoi_mode
= cell
->type
.in(ID($_AOI3_
), ID($_AOI4_
));
396 bool three_mode
= cell
->type
.in(ID($_AOI3_
), ID($_OAI3_
));
398 int a
= importDefSigSpec(cell
->getPort(ID::A
), timestep
).at(0);
399 int b
= importDefSigSpec(cell
->getPort(ID::B
), timestep
).at(0);
400 int c
= importDefSigSpec(cell
->getPort(ID(C
)), timestep
).at(0);
401 int d
= three_mode
? (aoi_mode
? ez
->CONST_TRUE
: ez
->CONST_FALSE
) : importDefSigSpec(cell
->getPort(ID(D
)), timestep
).at(0);
402 int y
= importDefSigSpec(cell
->getPort(ID::Y
), timestep
).at(0);
403 int yy
= model_undef
? ez
->literal() : y
;
405 if (cell
->type
.in(ID($_AOI3_
), ID($_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(ID::A
), timestep
).at(0);
413 int undef_b
= importUndefSigSpec(cell
->getPort(ID::B
), timestep
).at(0);
414 int undef_c
= importUndefSigSpec(cell
->getPort(ID(C
)), timestep
).at(0);
415 int undef_d
= three_mode
? ez
->CONST_FALSE
: importUndefSigSpec(cell
->getPort(ID(D
)), timestep
).at(0);
416 int undef_y
= importUndefSigSpec(cell
->getPort(ID::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
.in(ID($_NOT_
), ID($
not)))
461 std::vector
<int> a
= importDefSigSpec(cell
->getPort(ID::A
), timestep
);
462 std::vector
<int> y
= importDefSigSpec(cell
->getPort(ID::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(ID::A
), timestep
);
470 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort(ID::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
.in(ID($_MUX_
), ID($mux
), ID($_NMUX_
)))
480 std::vector
<int> a
= importDefSigSpec(cell
->getPort(ID::A
), timestep
);
481 std::vector
<int> b
= importDefSigSpec(cell
->getPort(ID::B
), timestep
);
482 std::vector
<int> s
= importDefSigSpec(cell
->getPort(ID(S
)), timestep
);
483 std::vector
<int> y
= importDefSigSpec(cell
->getPort(ID::Y
), timestep
);
485 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
486 if (cell
->type
== ID($_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(ID::A
), timestep
);
494 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort(ID::B
), timestep
);
495 std::vector
<int> undef_s
= importUndefSigSpec(cell
->getPort(ID(S
)), timestep
);
496 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort(ID::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
== ID($pmux
))
509 std::vector
<int> a
= importDefSigSpec(cell
->getPort(ID::A
), timestep
);
510 std::vector
<int> b
= importDefSigSpec(cell
->getPort(ID::B
), timestep
);
511 std::vector
<int> s
= importDefSigSpec(cell
->getPort(ID(S
)), timestep
);
512 std::vector
<int> y
= importDefSigSpec(cell
->getPort(ID::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(ID::A
), timestep
);
526 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort(ID::B
), timestep
);
527 std::vector
<int> undef_s
= importUndefSigSpec(cell
->getPort(ID(S
)), timestep
);
528 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort(ID::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
.in(ID($pos
), ID($neg
)))
560 std::vector
<int> a
= importDefSigSpec(cell
->getPort(ID::A
), timestep
);
561 std::vector
<int> y
= importDefSigSpec(cell
->getPort(ID::Y
), timestep
);
562 extendSignalWidthUnary(a
, y
, cell
);
564 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
566 if (cell
->type
== ID($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(ID::A
), timestep
);
576 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort(ID::Y
), timestep
);
577 extendSignalWidthUnary(undef_a
, undef_y
, cell
);
579 if (cell
->type
== ID($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
.in(ID($reduce_and
), ID($reduce_or
), ID($reduce_xor
), ID($reduce_xnor
), ID($reduce_bool
), ID($logic_not
)))
594 std::vector
<int> a
= importDefSigSpec(cell
->getPort(ID::A
), timestep
);
595 std::vector
<int> y
= importDefSigSpec(cell
->getPort(ID::Y
), timestep
);
597 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
599 if (cell
->type
== ID($reduce_and
))
600 ez
->SET(ez
->expression(ez
->OpAnd
, a
), yy
.at(0));
601 if (cell
->type
.in(ID($reduce_or
), ID($reduce_bool
)))
602 ez
->SET(ez
->expression(ez
->OpOr
, a
), yy
.at(0));
603 if (cell
->type
== ID($reduce_xor
))
604 ez
->SET(ez
->expression(ez
->OpXor
, a
), yy
.at(0));
605 if (cell
->type
== ID($reduce_xnor
))
606 ez
->SET(ez
->NOT(ez
->expression(ez
->OpXor
, a
)), yy
.at(0));
607 if (cell
->type
== ID($logic_not
))
608 ez
->SET(ez
->NOT(ez
->expression(ez
->OpOr
, a
)), yy
.at(0));
609 for (size_t i
= 1; i
< y
.size(); i
++)
610 ez
->SET(ez
->CONST_FALSE
, yy
.at(i
));
614 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort(ID::A
), timestep
);
615 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort(ID::Y
), timestep
);
616 int aX
= ez
->expression(ezSAT::OpOr
, undef_a
);
618 if (cell
->type
== ID($reduce_and
)) {
619 int a0
= ez
->expression(ezSAT::OpOr
, ez
->vec_and(ez
->vec_not(a
), ez
->vec_not(undef_a
)));
620 ez
->assume(ez
->IFF(ez
->AND(ez
->NOT(a0
), aX
), undef_y
.at(0)));
622 else if (cell
->type
.in(ID($reduce_or
), ID($reduce_bool
), ID($logic_not
))) {
623 int a1
= ez
->expression(ezSAT::OpOr
, ez
->vec_and(a
, ez
->vec_not(undef_a
)));
624 ez
->assume(ez
->IFF(ez
->AND(ez
->NOT(a1
), aX
), undef_y
.at(0)));
626 else if (cell
->type
.in(ID($reduce_xor
), ID($reduce_xnor
))) {
627 ez
->assume(ez
->IFF(aX
, undef_y
.at(0)));
631 for (size_t i
= 1; i
< undef_y
.size(); i
++)
632 ez
->SET(ez
->CONST_FALSE
, undef_y
.at(i
));
634 undefGating(y
, yy
, undef_y
);
639 if (cell
->type
.in(ID($logic_and
), ID($logic_or
)))
641 std::vector
<int> vec_a
= importDefSigSpec(cell
->getPort(ID::A
), timestep
);
642 std::vector
<int> vec_b
= importDefSigSpec(cell
->getPort(ID::B
), timestep
);
644 int a
= ez
->expression(ez
->OpOr
, vec_a
);
645 int b
= ez
->expression(ez
->OpOr
, vec_b
);
646 std::vector
<int> y
= importDefSigSpec(cell
->getPort(ID::Y
), timestep
);
648 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
650 if (cell
->type
== ID($logic_and
))
651 ez
->SET(ez
->expression(ez
->OpAnd
, a
, b
), yy
.at(0));
653 ez
->SET(ez
->expression(ez
->OpOr
, a
, b
), yy
.at(0));
654 for (size_t i
= 1; i
< y
.size(); i
++)
655 ez
->SET(ez
->CONST_FALSE
, yy
.at(i
));
659 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort(ID::A
), timestep
);
660 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort(ID::B
), timestep
);
661 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort(ID::Y
), timestep
);
663 int a0
= ez
->NOT(ez
->OR(ez
->expression(ezSAT::OpOr
, vec_a
), ez
->expression(ezSAT::OpOr
, undef_a
)));
664 int b0
= ez
->NOT(ez
->OR(ez
->expression(ezSAT::OpOr
, vec_b
), ez
->expression(ezSAT::OpOr
, undef_b
)));
665 int a1
= ez
->expression(ezSAT::OpOr
, ez
->vec_and(vec_a
, ez
->vec_not(undef_a
)));
666 int b1
= ez
->expression(ezSAT::OpOr
, ez
->vec_and(vec_b
, ez
->vec_not(undef_b
)));
667 int aX
= ez
->expression(ezSAT::OpOr
, undef_a
);
668 int bX
= ez
->expression(ezSAT::OpOr
, undef_b
);
670 if (cell
->type
== ID($logic_and
))
671 ez
->SET(ez
->AND(ez
->OR(aX
, bX
), ez
->NOT(ez
->AND(a1
, b1
)), ez
->NOT(a0
), ez
->NOT(b0
)), undef_y
.at(0));
672 else if (cell
->type
== ID($logic_or
))
673 ez
->SET(ez
->AND(ez
->OR(aX
, bX
), ez
->NOT(ez
->AND(a0
, b0
)), ez
->NOT(a1
), ez
->NOT(b1
)), undef_y
.at(0));
677 for (size_t i
= 1; i
< undef_y
.size(); i
++)
678 ez
->SET(ez
->CONST_FALSE
, undef_y
.at(i
));
680 undefGating(y
, yy
, undef_y
);
685 if (cell
->type
.in(ID($lt
), ID($le
), ID($eq
), ID($ne
), ID($eqx
), ID($nex
), ID($ge
), ID($gt
)))
687 bool is_signed
= cell
->parameters
[ID(A_SIGNED
)].as_bool() && cell
->parameters
[ID(B_SIGNED
)].as_bool();
688 std::vector
<int> a
= importDefSigSpec(cell
->getPort(ID::A
), timestep
);
689 std::vector
<int> b
= importDefSigSpec(cell
->getPort(ID::B
), timestep
);
690 std::vector
<int> y
= importDefSigSpec(cell
->getPort(ID::Y
), timestep
);
691 extendSignalWidth(a
, b
, cell
);
693 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
695 if (model_undef
&& cell
->type
.in(ID($eqx
), ID($nex
))) {
696 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort(ID::A
), timestep
);
697 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort(ID::B
), timestep
);
698 extendSignalWidth(undef_a
, undef_b
, cell
, true);
699 a
= ez
->vec_or(a
, undef_a
);
700 b
= ez
->vec_or(b
, undef_b
);
703 if (cell
->type
== ID($lt
))
704 ez
->SET(is_signed
? ez
->vec_lt_signed(a
, b
) : ez
->vec_lt_unsigned(a
, b
), yy
.at(0));
705 if (cell
->type
== ID($le
))
706 ez
->SET(is_signed
? ez
->vec_le_signed(a
, b
) : ez
->vec_le_unsigned(a
, b
), yy
.at(0));
707 if (cell
->type
.in(ID($eq
), ID($eqx
)))
708 ez
->SET(ez
->vec_eq(a
, b
), yy
.at(0));
709 if (cell
->type
.in(ID($ne
), ID($nex
)))
710 ez
->SET(ez
->vec_ne(a
, b
), yy
.at(0));
711 if (cell
->type
== ID($ge
))
712 ez
->SET(is_signed
? ez
->vec_ge_signed(a
, b
) : ez
->vec_ge_unsigned(a
, b
), yy
.at(0));
713 if (cell
->type
== ID($gt
))
714 ez
->SET(is_signed
? ez
->vec_gt_signed(a
, b
) : ez
->vec_gt_unsigned(a
, b
), yy
.at(0));
715 for (size_t i
= 1; i
< y
.size(); i
++)
716 ez
->SET(ez
->CONST_FALSE
, yy
.at(i
));
718 if (model_undef
&& cell
->type
.in(ID($eqx
), ID($nex
)))
720 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort(ID::A
), timestep
);
721 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort(ID::B
), timestep
);
722 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort(ID::Y
), timestep
);
723 extendSignalWidth(undef_a
, undef_b
, cell
, true);
725 if (cell
->type
== ID($eqx
))
726 yy
.at(0) = ez
->AND(yy
.at(0), ez
->vec_eq(undef_a
, undef_b
));
728 yy
.at(0) = ez
->OR(yy
.at(0), ez
->vec_ne(undef_a
, undef_b
));
730 for (size_t i
= 0; i
< y
.size(); i
++)
731 ez
->SET(ez
->CONST_FALSE
, undef_y
.at(i
));
733 ez
->assume(ez
->vec_eq(y
, yy
));
735 else if (model_undef
&& cell
->type
.in(ID($eq
), ID($ne
)))
737 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort(ID::A
), timestep
);
738 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort(ID::B
), timestep
);
739 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort(ID::Y
), timestep
);
740 extendSignalWidth(undef_a
, undef_b
, cell
, true);
742 int undef_any_a
= ez
->expression(ezSAT::OpOr
, undef_a
);
743 int undef_any_b
= ez
->expression(ezSAT::OpOr
, undef_b
);
744 int undef_any
= ez
->OR(undef_any_a
, undef_any_b
);
746 std::vector
<int> masked_a_bits
= ez
->vec_or(a
, ez
->vec_or(undef_a
, undef_b
));
747 std::vector
<int> masked_b_bits
= ez
->vec_or(b
, ez
->vec_or(undef_a
, undef_b
));
749 int masked_ne
= ez
->vec_ne(masked_a_bits
, masked_b_bits
);
750 int undef_y_bit
= ez
->AND(undef_any
, ez
->NOT(masked_ne
));
752 for (size_t i
= 1; i
< undef_y
.size(); i
++)
753 ez
->SET(ez
->CONST_FALSE
, undef_y
.at(i
));
754 ez
->SET(undef_y_bit
, undef_y
.at(0));
756 undefGating(y
, yy
, undef_y
);
761 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort(ID::Y
), timestep
);
762 undefGating(y
, yy
, undef_y
);
764 log_assert(!model_undef
|| arith_undef_handled
);
769 if (cell
->type
.in(ID($shl
), ID($shr
), ID($sshl
), ID($sshr
), ID($shift
), ID($shiftx
)))
771 std::vector
<int> a
= importDefSigSpec(cell
->getPort(ID::A
), timestep
);
772 std::vector
<int> b
= importDefSigSpec(cell
->getPort(ID::B
), timestep
);
773 std::vector
<int> y
= importDefSigSpec(cell
->getPort(ID::Y
), timestep
);
775 int extend_bit
= ez
->CONST_FALSE
;
777 if (!cell
->type
.in(ID($shift
), ID($shiftx
)) && cell
->parameters
[ID(A_SIGNED
)].as_bool())
778 extend_bit
= a
.back();
780 while (y
.size() < a
.size())
781 y
.push_back(ez
->literal());
782 while (y
.size() > a
.size())
783 a
.push_back(extend_bit
);
785 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
786 std::vector
<int> shifted_a
;
788 if (cell
->type
.in( ID($shl
), ID($sshl
)))
789 shifted_a
= ez
->vec_shift_left(a
, b
, false, ez
->CONST_FALSE
, ez
->CONST_FALSE
);
791 if (cell
->type
== ID($shr
))
792 shifted_a
= ez
->vec_shift_right(a
, b
, false, ez
->CONST_FALSE
, ez
->CONST_FALSE
);
794 if (cell
->type
== ID($sshr
))
795 shifted_a
= ez
->vec_shift_right(a
, b
, false, cell
->parameters
[ID(A_SIGNED
)].as_bool() ? a
.back() : ez
->CONST_FALSE
, ez
->CONST_FALSE
);
797 if (cell
->type
.in(ID($shift
), ID($shiftx
)))
798 shifted_a
= ez
->vec_shift_right(a
, b
, cell
->parameters
[ID(B_SIGNED
)].as_bool(), ez
->CONST_FALSE
, ez
->CONST_FALSE
);
800 ez
->assume(ez
->vec_eq(shifted_a
, yy
));
804 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort(ID::A
), timestep
);
805 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort(ID::B
), timestep
);
806 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort(ID::Y
), timestep
);
807 std::vector
<int> undef_a_shifted
;
809 extend_bit
= cell
->type
== ID($shiftx
) ? ez
->CONST_TRUE
: ez
->CONST_FALSE
;
810 if (!cell
->type
.in(ID($shift
), ID($shiftx
)) && cell
->parameters
[ID(A_SIGNED
)].as_bool())
811 extend_bit
= undef_a
.back();
813 while (undef_y
.size() < undef_a
.size())
814 undef_y
.push_back(ez
->literal());
815 while (undef_y
.size() > undef_a
.size())
816 undef_a
.push_back(extend_bit
);
818 if (cell
->type
.in(ID($shl
), ID($sshl
)))
819 undef_a_shifted
= ez
->vec_shift_left(undef_a
, b
, false, ez
->CONST_FALSE
, ez
->CONST_FALSE
);
821 if (cell
->type
== ID($shr
))
822 undef_a_shifted
= ez
->vec_shift_right(undef_a
, b
, false, ez
->CONST_FALSE
, ez
->CONST_FALSE
);
824 if (cell
->type
== ID($sshr
))
825 undef_a_shifted
= ez
->vec_shift_right(undef_a
, b
, false, cell
->parameters
[ID(A_SIGNED
)].as_bool() ? undef_a
.back() : ez
->CONST_FALSE
, ez
->CONST_FALSE
);
827 if (cell
->type
== ID($shift
))
828 undef_a_shifted
= ez
->vec_shift_right(undef_a
, b
, cell
->parameters
[ID(B_SIGNED
)].as_bool(), ez
->CONST_FALSE
, ez
->CONST_FALSE
);
830 if (cell
->type
== ID($shiftx
))
831 undef_a_shifted
= ez
->vec_shift_right(undef_a
, b
, cell
->parameters
[ID(B_SIGNED
)].as_bool(), ez
->CONST_TRUE
, ez
->CONST_TRUE
);
833 int undef_any_b
= ez
->expression(ezSAT::OpOr
, undef_b
);
834 std::vector
<int> undef_all_y_bits(undef_y
.size(), undef_any_b
);
835 ez
->assume(ez
->vec_eq(ez
->vec_or(undef_a_shifted
, undef_all_y_bits
), undef_y
));
836 undefGating(y
, yy
, undef_y
);
841 if (cell
->type
== ID($mul
))
843 std::vector
<int> a
= importDefSigSpec(cell
->getPort(ID::A
), timestep
);
844 std::vector
<int> b
= importDefSigSpec(cell
->getPort(ID::B
), timestep
);
845 std::vector
<int> y
= importDefSigSpec(cell
->getPort(ID::Y
), timestep
);
846 extendSignalWidth(a
, b
, y
, cell
);
848 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
850 std::vector
<int> tmp(a
.size(), ez
->CONST_FALSE
);
851 for (int i
= 0; i
< int(a
.size()); i
++)
853 std::vector
<int> shifted_a(a
.size(), ez
->CONST_FALSE
);
854 for (int j
= i
; j
< int(a
.size()); j
++)
855 shifted_a
.at(j
) = a
.at(j
-i
);
856 tmp
= ez
->vec_ite(b
.at(i
), ez
->vec_add(tmp
, shifted_a
), tmp
);
858 ez
->assume(ez
->vec_eq(tmp
, yy
));
861 log_assert(arith_undef_handled
);
862 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort(ID::Y
), timestep
);
863 undefGating(y
, yy
, undef_y
);
868 if (cell
->type
== ID($macc
))
870 std::vector
<int> a
= importDefSigSpec(cell
->getPort(ID::A
), timestep
);
871 std::vector
<int> b
= importDefSigSpec(cell
->getPort(ID::B
), timestep
);
872 std::vector
<int> y
= importDefSigSpec(cell
->getPort(ID::Y
), timestep
);
875 macc
.from_cell(cell
);
877 std::vector
<int> tmp(GetSize(y
), ez
->CONST_FALSE
);
879 for (auto &port
: macc
.ports
)
881 std::vector
<int> in_a
= importDefSigSpec(port
.in_a
, timestep
);
882 std::vector
<int> in_b
= importDefSigSpec(port
.in_b
, timestep
);
884 while (GetSize(in_a
) < GetSize(y
))
885 in_a
.push_back(port
.is_signed
&& !in_a
.empty() ? in_a
.back() : ez
->CONST_FALSE
);
886 in_a
.resize(GetSize(y
));
890 while (GetSize(in_b
) < GetSize(y
))
891 in_b
.push_back(port
.is_signed
&& !in_b
.empty() ? in_b
.back() : ez
->CONST_FALSE
);
892 in_b
.resize(GetSize(y
));
894 for (int i
= 0; i
< GetSize(in_b
); i
++) {
895 std::vector
<int> shifted_a(in_a
.size(), ez
->CONST_FALSE
);
896 for (int j
= i
; j
< int(in_a
.size()); j
++)
897 shifted_a
.at(j
) = in_a
.at(j
-i
);
898 if (port
.do_subtract
)
899 tmp
= ez
->vec_ite(in_b
.at(i
), ez
->vec_sub(tmp
, shifted_a
), tmp
);
901 tmp
= ez
->vec_ite(in_b
.at(i
), ez
->vec_add(tmp
, shifted_a
), tmp
);
906 if (port
.do_subtract
)
907 tmp
= ez
->vec_sub(tmp
, in_a
);
909 tmp
= ez
->vec_add(tmp
, in_a
);
913 for (int i
= 0; i
< GetSize(b
); i
++) {
914 std::vector
<int> val(GetSize(y
), ez
->CONST_FALSE
);
916 tmp
= ez
->vec_add(tmp
, val
);
921 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort(ID::A
), timestep
);
922 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort(ID::B
), timestep
);
924 int undef_any_a
= ez
->expression(ezSAT::OpOr
, undef_a
);
925 int undef_any_b
= ez
->expression(ezSAT::OpOr
, undef_b
);
927 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort(ID::Y
), timestep
);
928 ez
->assume(ez
->vec_eq(undef_y
, std::vector
<int>(GetSize(y
), ez
->OR(undef_any_a
, undef_any_b
))));
930 undefGating(y
, tmp
, undef_y
);
933 ez
->assume(ez
->vec_eq(y
, tmp
));
938 if (cell
->type
.in(ID($div
), ID($mod
)))
940 std::vector
<int> a
= importDefSigSpec(cell
->getPort(ID::A
), timestep
);
941 std::vector
<int> b
= importDefSigSpec(cell
->getPort(ID::B
), timestep
);
942 std::vector
<int> y
= importDefSigSpec(cell
->getPort(ID::Y
), timestep
);
943 extendSignalWidth(a
, b
, y
, cell
);
945 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
947 std::vector
<int> a_u
, b_u
;
948 if (cell
->parameters
[ID(A_SIGNED
)].as_bool() && cell
->parameters
[ID(B_SIGNED
)].as_bool()) {
949 a_u
= ez
->vec_ite(a
.back(), ez
->vec_neg(a
), a
);
950 b_u
= ez
->vec_ite(b
.back(), ez
->vec_neg(b
), b
);
956 std::vector
<int> chain_buf
= a_u
;
957 std::vector
<int> y_u(a_u
.size(), ez
->CONST_FALSE
);
958 for (int i
= int(a
.size())-1; i
>= 0; i
--)
960 chain_buf
.insert(chain_buf
.end(), chain_buf
.size(), ez
->CONST_FALSE
);
962 std::vector
<int> b_shl(i
, ez
->CONST_FALSE
);
963 b_shl
.insert(b_shl
.end(), b_u
.begin(), b_u
.end());
964 b_shl
.insert(b_shl
.end(), chain_buf
.size()-b_shl
.size(), ez
->CONST_FALSE
);
966 y_u
.at(i
) = ez
->vec_ge_unsigned(chain_buf
, b_shl
);
967 chain_buf
= ez
->vec_ite(y_u
.at(i
), ez
->vec_sub(chain_buf
, b_shl
), chain_buf
);
969 chain_buf
.erase(chain_buf
.begin() + a_u
.size(), chain_buf
.end());
972 std::vector
<int> y_tmp
= ignore_div_by_zero
? yy
: ez
->vec_var(y
.size());
973 if (cell
->type
== ID($div
)) {
974 if (cell
->parameters
[ID(A_SIGNED
)].as_bool() && cell
->parameters
[ID(B_SIGNED
)].as_bool())
975 ez
->assume(ez
->vec_eq(y_tmp
, ez
->vec_ite(ez
->XOR(a
.back(), b
.back()), ez
->vec_neg(y_u
), y_u
)));
977 ez
->assume(ez
->vec_eq(y_tmp
, y_u
));
979 if (cell
->parameters
[ID(A_SIGNED
)].as_bool() && cell
->parameters
[ID(B_SIGNED
)].as_bool())
980 ez
->assume(ez
->vec_eq(y_tmp
, ez
->vec_ite(a
.back(), ez
->vec_neg(chain_buf
), chain_buf
)));
982 ez
->assume(ez
->vec_eq(y_tmp
, chain_buf
));
985 if (ignore_div_by_zero
) {
986 ez
->assume(ez
->expression(ezSAT::OpOr
, b
));
988 std::vector
<int> div_zero_result
;
989 if (cell
->type
== ID($div
)) {
990 if (cell
->parameters
[ID(A_SIGNED
)].as_bool() && cell
->parameters
[ID(B_SIGNED
)].as_bool()) {
991 std::vector
<int> all_ones(y
.size(), ez
->CONST_TRUE
);
992 std::vector
<int> only_first_one(y
.size(), ez
->CONST_FALSE
);
993 only_first_one
.at(0) = ez
->CONST_TRUE
;
994 div_zero_result
= ez
->vec_ite(a
.back(), only_first_one
, all_ones
);
996 div_zero_result
.insert(div_zero_result
.end(), cell
->getPort(ID::A
).size(), ez
->CONST_TRUE
);
997 div_zero_result
.insert(div_zero_result
.end(), y
.size() - div_zero_result
.size(), ez
->CONST_FALSE
);
1000 int copy_a_bits
= min(cell
->getPort(ID::A
).size(), cell
->getPort(ID::B
).size());
1001 div_zero_result
.insert(div_zero_result
.end(), a
.begin(), a
.begin() + copy_a_bits
);
1002 if (cell
->parameters
[ID(A_SIGNED
)].as_bool() && cell
->parameters
[ID(B_SIGNED
)].as_bool())
1003 div_zero_result
.insert(div_zero_result
.end(), y
.size() - div_zero_result
.size(), div_zero_result
.back());
1005 div_zero_result
.insert(div_zero_result
.end(), y
.size() - div_zero_result
.size(), ez
->CONST_FALSE
);
1007 ez
->assume(ez
->vec_eq(yy
, ez
->vec_ite(ez
->expression(ezSAT::OpOr
, b
), y_tmp
, div_zero_result
)));
1011 log_assert(arith_undef_handled
);
1012 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort(ID::Y
), timestep
);
1013 undefGating(y
, yy
, undef_y
);
1018 if (cell
->type
== ID($lut
))
1020 std::vector
<int> a
= importDefSigSpec(cell
->getPort(ID::A
), timestep
);
1021 std::vector
<int> y
= importDefSigSpec(cell
->getPort(ID::Y
), timestep
);
1023 std::vector
<int> lut
;
1024 for (auto bit
: cell
->getParam(ID(LUT
)).bits
)
1025 lut
.push_back(bit
== State::S1
? ez
->CONST_TRUE
: ez
->CONST_FALSE
);
1026 while (GetSize(lut
) < (1 << GetSize(a
)))
1027 lut
.push_back(ez
->CONST_FALSE
);
1028 lut
.resize(1 << GetSize(a
));
1032 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort(ID::A
), timestep
);
1033 std::vector
<int> t(lut
), u(GetSize(t
), ez
->CONST_FALSE
);
1035 for (int i
= GetSize(a
)-1; i
>= 0; i
--)
1037 std::vector
<int> t0(t
.begin(), t
.begin() + GetSize(t
)/2);
1038 std::vector
<int> t1(t
.begin() + GetSize(t
)/2, t
.end());
1040 std::vector
<int> u0(u
.begin(), u
.begin() + GetSize(u
)/2);
1041 std::vector
<int> u1(u
.begin() + GetSize(u
)/2, u
.end());
1043 t
= ez
->vec_ite(a
[i
], t1
, t0
);
1044 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
));
1047 log_assert(GetSize(t
) == 1);
1048 log_assert(GetSize(u
) == 1);
1049 undefGating(y
, t
, u
);
1050 ez
->assume(ez
->vec_eq(importUndefSigSpec(cell
->getPort(ID::Y
), timestep
), u
));
1054 std::vector
<int> t
= lut
;
1055 for (int i
= GetSize(a
)-1; i
>= 0; i
--)
1057 std::vector
<int> t0(t
.begin(), t
.begin() + GetSize(t
)/2);
1058 std::vector
<int> t1(t
.begin() + GetSize(t
)/2, t
.end());
1059 t
= ez
->vec_ite(a
[i
], t1
, t0
);
1062 log_assert(GetSize(t
) == 1);
1063 ez
->assume(ez
->vec_eq(y
, t
));
1068 if (cell
->type
== ID($sop
))
1070 std::vector
<int> a
= importDefSigSpec(cell
->getPort(ID::A
), timestep
);
1071 int y
= importDefSigSpec(cell
->getPort(ID::Y
), timestep
).at(0);
1073 int width
= cell
->getParam(ID(WIDTH
)).as_int();
1074 int depth
= cell
->getParam(ID(DEPTH
)).as_int();
1076 vector
<State
> table_raw
= cell
->getParam(ID(TABLE
)).bits
;
1077 while (GetSize(table_raw
) < 2*width
*depth
)
1078 table_raw
.push_back(State::S0
);
1080 vector
<vector
<int>> table(depth
);
1082 for (int i
= 0; i
< depth
; i
++)
1083 for (int j
= 0; j
< width
; j
++)
1085 bool pat0
= (table_raw
[2*width
*i
+ 2*j
+ 0] == State::S1
);
1086 bool pat1
= (table_raw
[2*width
*i
+ 2*j
+ 1] == State::S1
);
1089 table
.at(i
).push_back(0);
1090 else if (!pat0
&& pat1
)
1091 table
.at(i
).push_back(1);
1093 table
.at(i
).push_back(-1);
1098 std::vector
<int> products
, undef_products
;
1099 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort(ID::A
), timestep
);
1100 int undef_y
= importUndefSigSpec(cell
->getPort(ID::Y
), timestep
).at(0);
1102 for (int i
= 0; i
< depth
; i
++)
1104 std::vector
<int> cmp_a
, cmp_ua
, cmp_b
;
1106 for (int j
= 0; j
< width
; j
++)
1107 if (table
.at(i
).at(j
) >= 0) {
1108 cmp_a
.push_back(a
.at(j
));
1109 cmp_ua
.push_back(undef_a
.at(j
));
1110 cmp_b
.push_back(table
.at(i
).at(j
) ? ez
->CONST_TRUE
: ez
->CONST_FALSE
);
1113 std::vector
<int> masked_a
= ez
->vec_or(cmp_a
, cmp_ua
);
1114 std::vector
<int> masked_b
= ez
->vec_or(cmp_b
, cmp_ua
);
1116 int masked_eq
= ez
->vec_eq(masked_a
, masked_b
);
1117 int any_undef
= ez
->expression(ezSAT::OpOr
, cmp_ua
);
1119 undef_products
.push_back(ez
->AND(any_undef
, masked_eq
));
1120 products
.push_back(ez
->AND(ez
->NOT(any_undef
), masked_eq
));
1123 int yy
= ez
->expression(ezSAT::OpOr
, products
);
1124 ez
->SET(undef_y
, ez
->AND(ez
->NOT(yy
), ez
->expression(ezSAT::OpOr
, undef_products
)));
1125 undefGating(y
, yy
, undef_y
);
1129 std::vector
<int> products
;
1131 for (int i
= 0; i
< depth
; i
++)
1133 std::vector
<int> cmp_a
, cmp_b
;
1135 for (int j
= 0; j
< width
; j
++)
1136 if (table
.at(i
).at(j
) >= 0) {
1137 cmp_a
.push_back(a
.at(j
));
1138 cmp_b
.push_back(table
.at(i
).at(j
) ? ez
->CONST_TRUE
: ez
->CONST_FALSE
);
1141 products
.push_back(ez
->vec_eq(cmp_a
, cmp_b
));
1144 ez
->SET(y
, ez
->expression(ezSAT::OpOr
, products
));
1150 if (cell
->type
== ID($fa
))
1152 std::vector
<int> a
= importDefSigSpec(cell
->getPort(ID::A
), timestep
);
1153 std::vector
<int> b
= importDefSigSpec(cell
->getPort(ID::B
), timestep
);
1154 std::vector
<int> c
= importDefSigSpec(cell
->getPort(ID(C
)), timestep
);
1155 std::vector
<int> y
= importDefSigSpec(cell
->getPort(ID::Y
), timestep
);
1156 std::vector
<int> x
= importDefSigSpec(cell
->getPort(ID(X
)), timestep
);
1158 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
1159 std::vector
<int> xx
= model_undef
? ez
->vec_var(x
.size()) : x
;
1161 std::vector
<int> t1
= ez
->vec_xor(a
, b
);
1162 ez
->assume(ez
->vec_eq(yy
, ez
->vec_xor(t1
, c
)));
1164 std::vector
<int> t2
= ez
->vec_and(a
, b
);
1165 std::vector
<int> t3
= ez
->vec_and(c
, t1
);
1166 ez
->assume(ez
->vec_eq(xx
, ez
->vec_or(t2
, t3
)));
1170 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort(ID::A
), timestep
);
1171 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort(ID::B
), timestep
);
1172 std::vector
<int> undef_c
= importUndefSigSpec(cell
->getPort(ID(C
)), timestep
);
1174 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort(ID::Y
), timestep
);
1175 std::vector
<int> undef_x
= importUndefSigSpec(cell
->getPort(ID(X
)), timestep
);
1177 ez
->assume(ez
->vec_eq(undef_y
, ez
->vec_or(ez
->vec_or(undef_a
, undef_b
), undef_c
)));
1178 ez
->assume(ez
->vec_eq(undef_x
, undef_y
));
1180 undefGating(y
, yy
, undef_y
);
1181 undefGating(x
, xx
, undef_x
);
1186 if (cell
->type
== ID($lcu
))
1188 std::vector
<int> p
= importDefSigSpec(cell
->getPort(ID(P
)), timestep
);
1189 std::vector
<int> g
= importDefSigSpec(cell
->getPort(ID(G
)), timestep
);
1190 std::vector
<int> ci
= importDefSigSpec(cell
->getPort(ID(CI
)), timestep
);
1191 std::vector
<int> co
= importDefSigSpec(cell
->getPort(ID(CO
)), timestep
);
1193 std::vector
<int> yy
= model_undef
? ez
->vec_var(co
.size()) : co
;
1195 for (int i
= 0; i
< GetSize(co
); i
++)
1196 ez
->SET(yy
[i
], ez
->OR(g
[i
], ez
->AND(p
[i
], i
? yy
[i
-1] : ci
[0])));
1200 std::vector
<int> undef_p
= importUndefSigSpec(cell
->getPort(ID(P
)), timestep
);
1201 std::vector
<int> undef_g
= importUndefSigSpec(cell
->getPort(ID(G
)), timestep
);
1202 std::vector
<int> undef_ci
= importUndefSigSpec(cell
->getPort(ID(CI
)), timestep
);
1203 std::vector
<int> undef_co
= importUndefSigSpec(cell
->getPort(ID(CO
)), timestep
);
1205 int undef_any_p
= ez
->expression(ezSAT::OpOr
, undef_p
);
1206 int undef_any_g
= ez
->expression(ezSAT::OpOr
, undef_g
);
1207 int undef_any_ci
= ez
->expression(ezSAT::OpOr
, undef_ci
);
1208 int undef_co_bit
= ez
->OR(undef_any_p
, undef_any_g
, undef_any_ci
);
1210 std::vector
<int> undef_co_bits(undef_co
.size(), undef_co_bit
);
1211 ez
->assume(ez
->vec_eq(undef_co_bits
, undef_co
));
1213 undefGating(co
, yy
, undef_co
);
1218 if (cell
->type
== ID($alu
))
1220 std::vector
<int> a
= importDefSigSpec(cell
->getPort(ID::A
), timestep
);
1221 std::vector
<int> b
= importDefSigSpec(cell
->getPort(ID::B
), timestep
);
1222 std::vector
<int> y
= importDefSigSpec(cell
->getPort(ID::Y
), timestep
);
1223 std::vector
<int> x
= importDefSigSpec(cell
->getPort(ID(X
)), timestep
);
1224 std::vector
<int> ci
= importDefSigSpec(cell
->getPort(ID(CI
)), timestep
);
1225 std::vector
<int> bi
= importDefSigSpec(cell
->getPort(ID(BI
)), timestep
);
1226 std::vector
<int> co
= importDefSigSpec(cell
->getPort(ID(CO
)), timestep
);
1228 extendSignalWidth(a
, b
, y
, cell
);
1229 extendSignalWidth(a
, b
, x
, cell
);
1230 extendSignalWidth(a
, b
, co
, cell
);
1232 std::vector
<int> def_y
= model_undef
? ez
->vec_var(y
.size()) : y
;
1233 std::vector
<int> def_x
= model_undef
? ez
->vec_var(x
.size()) : x
;
1234 std::vector
<int> def_co
= model_undef
? ez
->vec_var(co
.size()) : co
;
1236 log_assert(GetSize(y
) == GetSize(x
));
1237 log_assert(GetSize(y
) == GetSize(co
));
1238 log_assert(GetSize(ci
) == 1);
1239 log_assert(GetSize(bi
) == 1);
1241 for (int i
= 0; i
< GetSize(y
); i
++)
1243 int s1
= a
.at(i
), s2
= ez
->XOR(b
.at(i
), bi
.at(0)), s3
= i
? co
.at(i
-1) : ci
.at(0);
1244 ez
->SET(def_x
.at(i
), ez
->XOR(s1
, s2
));
1245 ez
->SET(def_y
.at(i
), ez
->XOR(def_x
.at(i
), s3
));
1246 ez
->SET(def_co
.at(i
), ez
->OR(ez
->AND(s1
, s2
), ez
->AND(s1
, s3
), ez
->AND(s2
, s3
)));
1251 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort(ID::A
), timestep
);
1252 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort(ID::B
), timestep
);
1253 std::vector
<int> undef_ci
= importUndefSigSpec(cell
->getPort(ID(CI
)), timestep
);
1254 std::vector
<int> undef_bi
= importUndefSigSpec(cell
->getPort(ID(BI
)), timestep
);
1256 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort(ID::Y
), timestep
);
1257 std::vector
<int> undef_x
= importUndefSigSpec(cell
->getPort(ID(X
)), timestep
);
1258 std::vector
<int> undef_co
= importUndefSigSpec(cell
->getPort(ID(CO
)), timestep
);
1260 extendSignalWidth(undef_a
, undef_b
, undef_y
, cell
);
1261 extendSignalWidth(undef_a
, undef_b
, undef_x
, cell
);
1262 extendSignalWidth(undef_a
, undef_b
, undef_co
, cell
);
1264 std::vector
<int> all_inputs_undef
;
1265 all_inputs_undef
.insert(all_inputs_undef
.end(), undef_a
.begin(), undef_a
.end());
1266 all_inputs_undef
.insert(all_inputs_undef
.end(), undef_b
.begin(), undef_b
.end());
1267 all_inputs_undef
.insert(all_inputs_undef
.end(), undef_ci
.begin(), undef_ci
.end());
1268 all_inputs_undef
.insert(all_inputs_undef
.end(), undef_bi
.begin(), undef_bi
.end());
1269 int undef_any
= ez
->expression(ezSAT::OpOr
, all_inputs_undef
);
1271 for (int i
= 0; i
< GetSize(undef_y
); i
++) {
1272 ez
->SET(undef_y
.at(i
), undef_any
);
1273 ez
->SET(undef_x
.at(i
), ez
->OR(undef_a
.at(i
), undef_b
.at(i
), undef_bi
.at(0)));
1274 ez
->SET(undef_co
.at(i
), undef_any
);
1277 undefGating(y
, def_y
, undef_y
);
1278 undefGating(x
, def_x
, undef_x
);
1279 undefGating(co
, def_co
, undef_co
);
1284 if (cell
->type
== ID($slice
))
1286 RTLIL::SigSpec a
= cell
->getPort(ID::A
);
1287 RTLIL::SigSpec y
= cell
->getPort(ID::Y
);
1288 ez
->assume(signals_eq(a
.extract(cell
->parameters
.at(ID(OFFSET
)).as_int(), y
.size()), y
, timestep
));
1292 if (cell
->type
== ID($concat
))
1294 RTLIL::SigSpec a
= cell
->getPort(ID::A
);
1295 RTLIL::SigSpec b
= cell
->getPort(ID::B
);
1296 RTLIL::SigSpec y
= cell
->getPort(ID::Y
);
1298 RTLIL::SigSpec ab
= a
;
1301 ez
->assume(signals_eq(ab
, y
, timestep
));
1305 if (timestep
> 0 && cell
->type
.in(ID($ff
), ID($dff
), ID($_FF_
), ID($_DFF_N_
), ID($_DFF_P_
)))
1309 initial_state
.add((*sigmap
)(cell
->getPort(ID(Q
))));
1313 std::vector
<int> d
= importDefSigSpec(cell
->getPort(ID(D
)), timestep
-1);
1314 std::vector
<int> q
= importDefSigSpec(cell
->getPort(ID(Q
)), timestep
);
1316 std::vector
<int> qq
= model_undef
? ez
->vec_var(q
.size()) : q
;
1317 ez
->assume(ez
->vec_eq(d
, qq
));
1321 std::vector
<int> undef_d
= importUndefSigSpec(cell
->getPort(ID(D
)), timestep
-1);
1322 std::vector
<int> undef_q
= importUndefSigSpec(cell
->getPort(ID(Q
)), timestep
);
1324 ez
->assume(ez
->vec_eq(undef_d
, undef_q
));
1325 undefGating(q
, qq
, undef_q
);
1331 if (cell
->type
== ID($anyconst
))
1336 std::vector
<int> d
= importDefSigSpec(cell
->getPort(ID::Y
), timestep
-1);
1337 std::vector
<int> q
= importDefSigSpec(cell
->getPort(ID::Y
), timestep
);
1339 std::vector
<int> qq
= model_undef
? ez
->vec_var(q
.size()) : q
;
1340 ez
->assume(ez
->vec_eq(d
, qq
));
1344 std::vector
<int> undef_d
= importUndefSigSpec(cell
->getPort(ID::Y
), timestep
-1);
1345 std::vector
<int> undef_q
= importUndefSigSpec(cell
->getPort(ID::Y
), timestep
);
1347 ez
->assume(ez
->vec_eq(undef_d
, undef_q
));
1348 undefGating(q
, qq
, undef_q
);
1353 if (cell
->type
== ID($anyseq
))
1358 if (cell
->type
.in(ID($_BUF_
), ID($equiv
)))
1360 std::vector
<int> a
= importDefSigSpec(cell
->getPort(ID::A
), timestep
);
1361 std::vector
<int> y
= importDefSigSpec(cell
->getPort(ID::Y
), timestep
);
1362 extendSignalWidthUnary(a
, y
, cell
);
1364 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
1365 ez
->assume(ez
->vec_eq(a
, yy
));
1368 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort(ID::A
), timestep
);
1369 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort(ID::Y
), timestep
);
1370 extendSignalWidthUnary(undef_a
, undef_y
, cell
, false);
1371 ez
->assume(ez
->vec_eq(undef_a
, undef_y
));
1372 undefGating(y
, yy
, undef_y
);
1377 if (cell
->type
== ID($initstate
))
1379 auto key
= make_pair(prefix
, timestep
);
1380 if (initstates
.count(key
) == 0)
1381 initstates
[key
] = false;
1383 std::vector
<int> y
= importDefSigSpec(cell
->getPort(ID::Y
), timestep
);
1384 log_assert(GetSize(y
) == 1);
1385 ez
->SET(y
[0], initstates
[key
] ? ez
->CONST_TRUE
: ez
->CONST_FALSE
);
1388 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort(ID::Y
), timestep
);
1389 log_assert(GetSize(undef_y
) == 1);
1390 ez
->SET(undef_y
[0], ez
->CONST_FALSE
);
1396 if (cell
->type
== ID($
assert))
1398 std::string pf
= prefix
+ (timestep
== -1 ? "" : stringf("@%d:", timestep
));
1399 asserts_a
[pf
].append((*sigmap
)(cell
->getPort(ID::A
)));
1400 asserts_en
[pf
].append((*sigmap
)(cell
->getPort(ID(EN
))));
1404 if (cell
->type
== ID($assume
))
1406 std::string pf
= prefix
+ (timestep
== -1 ? "" : stringf("@%d:", timestep
));
1407 assumes_a
[pf
].append((*sigmap
)(cell
->getPort(ID::A
)));
1408 assumes_en
[pf
].append((*sigmap
)(cell
->getPort(ID(EN
))));
1412 // Unsupported internal cell types: $pow $lut
1413 // .. and all sequential cells except $dff and $_DFF_[NP]_