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 bool ignore_div_by_zero
;
76 SatGen(ezSAT
*ez
, SigMap
*sigmap
, std::string prefix
= std::string()) :
77 ez(ez
), sigmap(sigmap
), prefix(prefix
), ignore_div_by_zero(false), model_undef(false)
81 void setContext(SigMap
*sigmap
, std::string prefix
= std::string())
83 this->sigmap
= sigmap
;
84 this->prefix
= prefix
;
87 std::vector
<int> importSigSpecWorker(RTLIL::SigSpec sig
, std::string
&pf
, bool undef_mode
, bool dup_undef
)
89 log_assert(!undef_mode
|| model_undef
);
93 vec
.reserve(GetSize(sig
));
96 if (bit
.wire
== NULL
) {
97 if (model_undef
&& dup_undef
&& bit
== RTLIL::State::Sx
)
98 vec
.push_back(ez
->frozen_literal());
100 vec
.push_back(bit
== (undef_mode
? RTLIL::State::Sx
: RTLIL::State::S1
) ? ez
->CONST_TRUE
: ez
->CONST_FALSE
);
102 std::string name
= pf
+ (bit
.wire
->width
== 1 ? stringf("%s", log_id(bit
.wire
)) : stringf("%s [%d]", log_id(bit
.wire
->name
), bit
.offset
));
103 vec
.push_back(ez
->frozen_literal(name
));
104 imported_signals
[pf
][bit
] = vec
.back();
109 std::vector
<int> importSigSpec(RTLIL::SigSpec sig
, int timestep
= -1)
111 log_assert(timestep
!= 0);
112 std::string pf
= prefix
+ (timestep
== -1 ? "" : stringf("@%d:", timestep
));
113 return importSigSpecWorker(sig
, pf
, false, false);
116 std::vector
<int> importDefSigSpec(RTLIL::SigSpec sig
, int timestep
= -1)
118 log_assert(timestep
!= 0);
119 std::string pf
= prefix
+ (timestep
== -1 ? "" : stringf("@%d:", timestep
));
120 return importSigSpecWorker(sig
, pf
, false, true);
123 std::vector
<int> importUndefSigSpec(RTLIL::SigSpec sig
, int timestep
= -1)
125 log_assert(timestep
!= 0);
126 std::string pf
= "undef:" + prefix
+ (timestep
== -1 ? "" : stringf("@%d:", timestep
));
127 return importSigSpecWorker(sig
, pf
, true, false);
130 int importSigBit(RTLIL::SigBit bit
, int timestep
= -1)
132 log_assert(timestep
!= 0);
133 std::string pf
= prefix
+ (timestep
== -1 ? "" : stringf("@%d:", timestep
));
134 return importSigSpecWorker(bit
, pf
, false, false).front();
137 int importDefSigBit(RTLIL::SigBit bit
, int timestep
= -1)
139 log_assert(timestep
!= 0);
140 std::string pf
= prefix
+ (timestep
== -1 ? "" : stringf("@%d:", timestep
));
141 return importSigSpecWorker(bit
, pf
, false, true).front();
144 int importUndefSigBit(RTLIL::SigBit bit
, int timestep
= -1)
146 log_assert(timestep
!= 0);
147 std::string pf
= "undef:" + prefix
+ (timestep
== -1 ? "" : stringf("@%d:", timestep
));
148 return importSigSpecWorker(bit
, pf
, true, false).front();
151 bool importedSigBit(RTLIL::SigBit bit
, int timestep
= -1)
153 log_assert(timestep
!= 0);
154 std::string pf
= prefix
+ (timestep
== -1 ? "" : stringf("@%d:", timestep
));
155 return imported_signals
[pf
].count(bit
) != 0;
158 void getAsserts(RTLIL::SigSpec
&sig_a
, RTLIL::SigSpec
&sig_en
, int timestep
= -1)
160 std::string pf
= prefix
+ (timestep
== -1 ? "" : stringf("@%d:", timestep
));
161 sig_a
= asserts_a
[pf
];
162 sig_en
= asserts_en
[pf
];
165 void getAssumes(RTLIL::SigSpec
&sig_a
, RTLIL::SigSpec
&sig_en
, int timestep
= -1)
167 std::string pf
= prefix
+ (timestep
== -1 ? "" : stringf("@%d:", timestep
));
168 sig_a
= assumes_a
[pf
];
169 sig_en
= assumes_en
[pf
];
172 int importAsserts(int timestep
= -1)
174 std::vector
<int> check_bits
, enable_bits
;
175 std::string pf
= prefix
+ (timestep
== -1 ? "" : stringf("@%d:", timestep
));
177 check_bits
= ez
->vec_and(ez
->vec_not(importUndefSigSpec(asserts_a
[pf
], timestep
)), importDefSigSpec(asserts_a
[pf
], timestep
));
178 enable_bits
= ez
->vec_and(ez
->vec_not(importUndefSigSpec(asserts_en
[pf
], timestep
)), importDefSigSpec(asserts_en
[pf
], timestep
));
180 check_bits
= importDefSigSpec(asserts_a
[pf
], timestep
);
181 enable_bits
= importDefSigSpec(asserts_en
[pf
], timestep
);
183 return ez
->vec_reduce_and(ez
->vec_or(check_bits
, ez
->vec_not(enable_bits
)));
186 int importAssumes(int timestep
= -1)
188 std::vector
<int> check_bits
, enable_bits
;
189 std::string pf
= prefix
+ (timestep
== -1 ? "" : stringf("@%d:", timestep
));
191 check_bits
= ez
->vec_and(ez
->vec_not(importUndefSigSpec(assumes_a
[pf
], timestep
)), importDefSigSpec(assumes_a
[pf
], timestep
));
192 enable_bits
= ez
->vec_and(ez
->vec_not(importUndefSigSpec(assumes_en
[pf
], timestep
)), importDefSigSpec(assumes_en
[pf
], timestep
));
194 check_bits
= importDefSigSpec(assumes_a
[pf
], timestep
);
195 enable_bits
= importDefSigSpec(assumes_en
[pf
], timestep
);
197 return ez
->vec_reduce_and(ez
->vec_or(check_bits
, ez
->vec_not(enable_bits
)));
200 int signals_eq(RTLIL::SigSpec lhs
, RTLIL::SigSpec rhs
, int timestep_lhs
= -1, int timestep_rhs
= -1)
202 if (timestep_rhs
< 0)
203 timestep_rhs
= timestep_lhs
;
205 log_assert(lhs
.size() == rhs
.size());
207 std::vector
<int> vec_lhs
= importSigSpec(lhs
, timestep_lhs
);
208 std::vector
<int> vec_rhs
= importSigSpec(rhs
, timestep_rhs
);
211 return ez
->vec_eq(vec_lhs
, vec_rhs
);
213 std::vector
<int> undef_lhs
= importUndefSigSpec(lhs
, timestep_lhs
);
214 std::vector
<int> undef_rhs
= importUndefSigSpec(rhs
, timestep_rhs
);
216 std::vector
<int> eq_bits
;
217 for (int i
= 0; i
< lhs
.size(); i
++)
218 eq_bits
.push_back(ez
->AND(ez
->IFF(undef_lhs
.at(i
), undef_rhs
.at(i
)),
219 ez
->IFF(ez
->OR(vec_lhs
.at(i
), undef_lhs
.at(i
)), ez
->OR(vec_rhs
.at(i
), undef_rhs
.at(i
)))));
220 return ez
->expression(ezSAT::OpAnd
, eq_bits
);
223 void extendSignalWidth(std::vector
<int> &vec_a
, std::vector
<int> &vec_b
, RTLIL::Cell
*cell
, size_t y_width
= 0, bool forced_signed
= false)
225 bool is_signed
= forced_signed
;
226 if (!forced_signed
&& cell
->parameters
.count("\\A_SIGNED") > 0 && cell
->parameters
.count("\\B_SIGNED") > 0)
227 is_signed
= cell
->parameters
["\\A_SIGNED"].as_bool() && cell
->parameters
["\\B_SIGNED"].as_bool();
228 while (vec_a
.size() < vec_b
.size() || vec_a
.size() < y_width
)
229 vec_a
.push_back(is_signed
&& vec_a
.size() > 0 ? vec_a
.back() : ez
->CONST_FALSE
);
230 while (vec_b
.size() < vec_a
.size() || vec_b
.size() < y_width
)
231 vec_b
.push_back(is_signed
&& vec_b
.size() > 0 ? vec_b
.back() : ez
->CONST_FALSE
);
234 void extendSignalWidth(std::vector
<int> &vec_a
, std::vector
<int> &vec_b
, std::vector
<int> &vec_y
, RTLIL::Cell
*cell
, bool forced_signed
= false)
236 extendSignalWidth(vec_a
, vec_b
, cell
, vec_y
.size(), forced_signed
);
237 while (vec_y
.size() < vec_a
.size())
238 vec_y
.push_back(ez
->literal());
241 void extendSignalWidthUnary(std::vector
<int> &vec_a
, std::vector
<int> &vec_y
, RTLIL::Cell
*cell
, bool forced_signed
= false)
243 bool is_signed
= forced_signed
|| (cell
->parameters
.count("\\A_SIGNED") > 0 && cell
->parameters
["\\A_SIGNED"].as_bool());
244 while (vec_a
.size() < vec_y
.size())
245 vec_a
.push_back(is_signed
&& vec_a
.size() > 0 ? vec_a
.back() : ez
->CONST_FALSE
);
246 while (vec_y
.size() < vec_a
.size())
247 vec_y
.push_back(ez
->literal());
250 void undefGating(std::vector
<int> &vec_y
, std::vector
<int> &vec_yy
, std::vector
<int> &vec_undef
)
252 log_assert(model_undef
);
253 log_assert(vec_y
.size() == vec_yy
.size());
254 if (vec_y
.size() > vec_undef
.size()) {
255 std::vector
<int> trunc_y(vec_y
.begin(), vec_y
.begin() + vec_undef
.size());
256 std::vector
<int> trunc_yy(vec_yy
.begin(), vec_yy
.begin() + vec_undef
.size());
257 ez
->assume(ez
->expression(ezSAT::OpAnd
, ez
->vec_or(vec_undef
, ez
->vec_iff(trunc_y
, trunc_yy
))));
259 log_assert(vec_y
.size() == vec_undef
.size());
260 ez
->assume(ez
->expression(ezSAT::OpAnd
, ez
->vec_or(vec_undef
, ez
->vec_iff(vec_y
, vec_yy
))));
264 void undefGating(int y
, int yy
, int undef
)
266 ez
->assume(ez
->OR(undef
, ez
->IFF(y
, yy
)));
269 bool importCell(RTLIL::Cell
*cell
, int timestep
= -1)
271 bool arith_undef_handled
= false;
272 bool is_arith_compare
= cell
->type
.in("$lt", "$le", "$ge", "$gt");
274 if (model_undef
&& (cell
->type
.in("$add", "$sub", "$mul", "$div", "$mod") || is_arith_compare
))
276 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
277 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort("\\B"), timestep
);
278 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
279 if (is_arith_compare
)
280 extendSignalWidth(undef_a
, undef_b
, cell
, true);
282 extendSignalWidth(undef_a
, undef_b
, undef_y
, cell
, true);
284 int undef_any_a
= ez
->expression(ezSAT::OpOr
, undef_a
);
285 int undef_any_b
= ez
->expression(ezSAT::OpOr
, undef_b
);
286 int undef_y_bit
= ez
->OR(undef_any_a
, undef_any_b
);
288 if (cell
->type
== "$div" || cell
->type
== "$mod") {
289 std::vector
<int> b
= importSigSpec(cell
->getPort("\\B"), timestep
);
290 undef_y_bit
= ez
->OR(undef_y_bit
, ez
->NOT(ez
->expression(ezSAT::OpOr
, b
)));
293 if (is_arith_compare
) {
294 for (size_t i
= 1; i
< undef_y
.size(); i
++)
295 ez
->SET(ez
->CONST_FALSE
, undef_y
.at(i
));
296 ez
->SET(undef_y_bit
, undef_y
.at(0));
298 std::vector
<int> undef_y_bits(undef_y
.size(), undef_y_bit
);
299 ez
->assume(ez
->vec_eq(undef_y_bits
, undef_y
));
302 arith_undef_handled
= true;
305 if (cell
->type
.in("$_AND_", "$_NAND_", "$_OR_", "$_NOR_", "$_XOR_", "$_XNOR_",
306 "$and", "$or", "$xor", "$xnor", "$add", "$sub"))
308 std::vector
<int> a
= importDefSigSpec(cell
->getPort("\\A"), timestep
);
309 std::vector
<int> b
= importDefSigSpec(cell
->getPort("\\B"), timestep
);
310 std::vector
<int> y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
311 extendSignalWidth(a
, b
, y
, cell
);
313 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
315 if (cell
->type
== "$and" || cell
->type
== "$_AND_")
316 ez
->assume(ez
->vec_eq(ez
->vec_and(a
, b
), yy
));
317 if (cell
->type
== "$_NAND_")
318 ez
->assume(ez
->vec_eq(ez
->vec_not(ez
->vec_and(a
, b
)), yy
));
319 if (cell
->type
== "$or" || cell
->type
== "$_OR_")
320 ez
->assume(ez
->vec_eq(ez
->vec_or(a
, b
), yy
));
321 if (cell
->type
== "$_NOR_")
322 ez
->assume(ez
->vec_eq(ez
->vec_not(ez
->vec_or(a
, b
)), yy
));
323 if (cell
->type
== "$xor" || cell
->type
== "$_XOR_")
324 ez
->assume(ez
->vec_eq(ez
->vec_xor(a
, b
), yy
));
325 if (cell
->type
== "$xnor" || cell
->type
== "$_XNOR_")
326 ez
->assume(ez
->vec_eq(ez
->vec_not(ez
->vec_xor(a
, b
)), yy
));
327 if (cell
->type
== "$add")
328 ez
->assume(ez
->vec_eq(ez
->vec_add(a
, b
), yy
));
329 if (cell
->type
== "$sub")
330 ez
->assume(ez
->vec_eq(ez
->vec_sub(a
, b
), yy
));
332 if (model_undef
&& !arith_undef_handled
)
334 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
335 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort("\\B"), timestep
);
336 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
337 extendSignalWidth(undef_a
, undef_b
, undef_y
, cell
, false);
339 if (cell
->type
.in("$and", "$_AND_", "$_NAND_")) {
340 std::vector
<int> a0
= ez
->vec_and(ez
->vec_not(a
), ez
->vec_not(undef_a
));
341 std::vector
<int> b0
= ez
->vec_and(ez
->vec_not(b
), ez
->vec_not(undef_b
));
342 std::vector
<int> yX
= ez
->vec_and(ez
->vec_or(undef_a
, undef_b
), ez
->vec_not(ez
->vec_or(a0
, b0
)));
343 ez
->assume(ez
->vec_eq(yX
, undef_y
));
345 else if (cell
->type
.in("$or", "$_OR_", "$_NOR_")) {
346 std::vector
<int> a1
= ez
->vec_and(a
, ez
->vec_not(undef_a
));
347 std::vector
<int> b1
= ez
->vec_and(b
, ez
->vec_not(undef_b
));
348 std::vector
<int> yX
= ez
->vec_and(ez
->vec_or(undef_a
, undef_b
), ez
->vec_not(ez
->vec_or(a1
, b1
)));
349 ez
->assume(ez
->vec_eq(yX
, undef_y
));
351 else if (cell
->type
.in("$xor", "$xnor", "$_XOR_", "$_XNOR_")) {
352 std::vector
<int> yX
= ez
->vec_or(undef_a
, undef_b
);
353 ez
->assume(ez
->vec_eq(yX
, undef_y
));
358 undefGating(y
, yy
, undef_y
);
360 else if (model_undef
)
362 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
363 undefGating(y
, yy
, undef_y
);
368 if (cell
->type
.in("$_AOI3_", "$_OAI3_", "$_AOI4_", "$_OAI4_"))
370 bool aoi_mode
= cell
->type
.in("$_AOI3_", "$_AOI4_");
371 bool three_mode
= cell
->type
.in("$_AOI3_", "$_OAI3_");
373 int a
= importDefSigSpec(cell
->getPort("\\A"), timestep
).at(0);
374 int b
= importDefSigSpec(cell
->getPort("\\B"), timestep
).at(0);
375 int c
= importDefSigSpec(cell
->getPort("\\C"), timestep
).at(0);
376 int d
= three_mode
? (aoi_mode
? ez
->CONST_TRUE
: ez
->CONST_FALSE
) : importDefSigSpec(cell
->getPort("\\D"), timestep
).at(0);
377 int y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
).at(0);
378 int yy
= model_undef
? ez
->literal() : y
;
380 if (cell
->type
.in("$_AOI3_", "$_AOI4_"))
381 ez
->assume(ez
->IFF(ez
->NOT(ez
->OR(ez
->AND(a
, b
), ez
->AND(c
, d
))), yy
));
383 ez
->assume(ez
->IFF(ez
->NOT(ez
->AND(ez
->OR(a
, b
), ez
->OR(c
, d
))), yy
));
387 int undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
).at(0);
388 int undef_b
= importUndefSigSpec(cell
->getPort("\\B"), timestep
).at(0);
389 int undef_c
= importUndefSigSpec(cell
->getPort("\\C"), timestep
).at(0);
390 int undef_d
= three_mode
? ez
->CONST_FALSE
: importUndefSigSpec(cell
->getPort("\\D"), timestep
).at(0);
391 int undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
).at(0);
395 int a0
= ez
->AND(ez
->NOT(a
), ez
->NOT(undef_a
));
396 int b0
= ez
->AND(ez
->NOT(b
), ez
->NOT(undef_b
));
397 int c0
= ez
->AND(ez
->NOT(c
), ez
->NOT(undef_c
));
398 int d0
= ez
->AND(ez
->NOT(d
), ez
->NOT(undef_d
));
400 int ab
= ez
->AND(a
, b
), cd
= ez
->AND(c
, d
);
401 int undef_ab
= ez
->AND(ez
->OR(undef_a
, undef_b
), ez
->NOT(ez
->OR(a0
, b0
)));
402 int undef_cd
= ez
->AND(ez
->OR(undef_c
, undef_d
), ez
->NOT(ez
->OR(c0
, d0
)));
404 int ab1
= ez
->AND(ab
, ez
->NOT(undef_ab
));
405 int cd1
= ez
->AND(cd
, ez
->NOT(undef_cd
));
406 int yX
= ez
->AND(ez
->OR(undef_ab
, undef_cd
), ez
->NOT(ez
->OR(ab1
, cd1
)));
408 ez
->assume(ez
->IFF(yX
, undef_y
));
412 int a1
= ez
->AND(a
, ez
->NOT(undef_a
));
413 int b1
= ez
->AND(b
, ez
->NOT(undef_b
));
414 int c1
= ez
->AND(c
, ez
->NOT(undef_c
));
415 int d1
= ez
->AND(d
, ez
->NOT(undef_d
));
417 int ab
= ez
->OR(a
, b
), cd
= ez
->OR(c
, d
);
418 int undef_ab
= ez
->AND(ez
->OR(undef_a
, undef_b
), ez
->NOT(ez
->OR(a1
, b1
)));
419 int undef_cd
= ez
->AND(ez
->OR(undef_c
, undef_d
), ez
->NOT(ez
->OR(c1
, d1
)));
421 int ab0
= ez
->AND(ez
->NOT(ab
), ez
->NOT(undef_ab
));
422 int cd0
= ez
->AND(ez
->NOT(cd
), ez
->NOT(undef_cd
));
423 int yX
= ez
->AND(ez
->OR(undef_ab
, undef_cd
), ez
->NOT(ez
->OR(ab0
, cd0
)));
425 ez
->assume(ez
->IFF(yX
, undef_y
));
428 undefGating(y
, yy
, undef_y
);
434 if (cell
->type
== "$_NOT_" || cell
->type
== "$not")
436 std::vector
<int> a
= importDefSigSpec(cell
->getPort("\\A"), timestep
);
437 std::vector
<int> y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
438 extendSignalWidthUnary(a
, y
, cell
);
440 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
441 ez
->assume(ez
->vec_eq(ez
->vec_not(a
), yy
));
444 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
445 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
446 extendSignalWidthUnary(undef_a
, undef_y
, cell
, false);
447 ez
->assume(ez
->vec_eq(undef_a
, undef_y
));
448 undefGating(y
, yy
, undef_y
);
453 if (cell
->type
== "$_MUX_" || cell
->type
== "$mux")
455 std::vector
<int> a
= importDefSigSpec(cell
->getPort("\\A"), timestep
);
456 std::vector
<int> b
= importDefSigSpec(cell
->getPort("\\B"), timestep
);
457 std::vector
<int> s
= importDefSigSpec(cell
->getPort("\\S"), timestep
);
458 std::vector
<int> y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
460 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
461 ez
->assume(ez
->vec_eq(ez
->vec_ite(s
.at(0), b
, a
), yy
));
465 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
466 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort("\\B"), timestep
);
467 std::vector
<int> undef_s
= importUndefSigSpec(cell
->getPort("\\S"), timestep
);
468 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
470 std::vector
<int> unequal_ab
= ez
->vec_not(ez
->vec_iff(a
, b
));
471 std::vector
<int> undef_ab
= ez
->vec_or(unequal_ab
, ez
->vec_or(undef_a
, undef_b
));
472 std::vector
<int> yX
= ez
->vec_ite(undef_s
.at(0), undef_ab
, ez
->vec_ite(s
.at(0), undef_b
, undef_a
));
473 ez
->assume(ez
->vec_eq(yX
, undef_y
));
474 undefGating(y
, yy
, undef_y
);
479 if (cell
->type
== "$pmux")
481 std::vector
<int> a
= importDefSigSpec(cell
->getPort("\\A"), timestep
);
482 std::vector
<int> b
= importDefSigSpec(cell
->getPort("\\B"), timestep
);
483 std::vector
<int> s
= importDefSigSpec(cell
->getPort("\\S"), timestep
);
484 std::vector
<int> y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
486 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
488 std::vector
<int> tmp
= a
;
489 for (size_t i
= 0; i
< s
.size(); i
++) {
490 std::vector
<int> part_of_b(b
.begin()+i
*a
.size(), b
.begin()+(i
+1)*a
.size());
491 tmp
= ez
->vec_ite(s
.at(i
), part_of_b
, tmp
);
493 ez
->assume(ez
->vec_eq(tmp
, yy
));
497 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
498 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort("\\B"), timestep
);
499 std::vector
<int> undef_s
= importUndefSigSpec(cell
->getPort("\\S"), timestep
);
500 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
502 int maybe_one_hot
= ez
->CONST_FALSE
;
503 int maybe_many_hot
= ez
->CONST_FALSE
;
505 int sure_one_hot
= ez
->CONST_FALSE
;
506 int sure_many_hot
= ez
->CONST_FALSE
;
508 std::vector
<int> bits_set
= std::vector
<int>(undef_y
.size(), ez
->CONST_FALSE
);
509 std::vector
<int> bits_clr
= std::vector
<int>(undef_y
.size(), ez
->CONST_FALSE
);
511 for (size_t i
= 0; i
< s
.size(); i
++)
513 std::vector
<int> part_of_b(b
.begin()+i
*a
.size(), b
.begin()+(i
+1)*a
.size());
514 std::vector
<int> part_of_undef_b(undef_b
.begin()+i
*a
.size(), undef_b
.begin()+(i
+1)*a
.size());
516 int maybe_s
= ez
->OR(s
.at(i
), undef_s
.at(i
));
517 int sure_s
= ez
->AND(s
.at(i
), ez
->NOT(undef_s
.at(i
)));
519 maybe_one_hot
= ez
->OR(maybe_one_hot
, maybe_s
);
520 maybe_many_hot
= ez
->OR(maybe_many_hot
, ez
->AND(maybe_one_hot
, maybe_s
));
522 sure_one_hot
= ez
->OR(sure_one_hot
, sure_s
);
523 sure_many_hot
= ez
->OR(sure_many_hot
, ez
->AND(sure_one_hot
, sure_s
));
525 bits_set
= ez
->vec_ite(maybe_s
, ez
->vec_or(bits_set
, ez
->vec_or(bits_set
, ez
->vec_or(part_of_b
, part_of_undef_b
))), bits_set
);
526 bits_clr
= ez
->vec_ite(maybe_s
, ez
->vec_or(bits_clr
, ez
->vec_or(bits_clr
, ez
->vec_or(ez
->vec_not(part_of_b
), part_of_undef_b
))), bits_clr
);
529 int maybe_a
= ez
->NOT(maybe_one_hot
);
531 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
);
532 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
);
534 ez
->assume(ez
->vec_eq(ez
->vec_not(ez
->vec_xor(bits_set
, bits_clr
)), undef_y
));
535 undefGating(y
, yy
, undef_y
);
540 if (cell
->type
== "$pos" || cell
->type
== "$neg")
542 std::vector
<int> a
= importDefSigSpec(cell
->getPort("\\A"), timestep
);
543 std::vector
<int> y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
544 extendSignalWidthUnary(a
, y
, cell
);
546 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
548 if (cell
->type
== "$pos") {
549 ez
->assume(ez
->vec_eq(a
, yy
));
551 std::vector
<int> zero(a
.size(), ez
->CONST_FALSE
);
552 ez
->assume(ez
->vec_eq(ez
->vec_sub(zero
, a
), yy
));
557 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
558 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
559 extendSignalWidthUnary(undef_a
, undef_y
, cell
);
561 if (cell
->type
== "$pos") {
562 ez
->assume(ez
->vec_eq(undef_a
, undef_y
));
564 int undef_any_a
= ez
->expression(ezSAT::OpOr
, undef_a
);
565 std::vector
<int> undef_y_bits(undef_y
.size(), undef_any_a
);
566 ez
->assume(ez
->vec_eq(undef_y_bits
, undef_y
));
569 undefGating(y
, yy
, undef_y
);
574 if (cell
->type
== "$reduce_and" || cell
->type
== "$reduce_or" || cell
->type
== "$reduce_xor" ||
575 cell
->type
== "$reduce_xnor" || cell
->type
== "$reduce_bool" || cell
->type
== "$logic_not")
577 std::vector
<int> a
= importDefSigSpec(cell
->getPort("\\A"), timestep
);
578 std::vector
<int> y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
580 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
582 if (cell
->type
== "$reduce_and")
583 ez
->SET(ez
->expression(ez
->OpAnd
, a
), yy
.at(0));
584 if (cell
->type
== "$reduce_or" || cell
->type
== "$reduce_bool")
585 ez
->SET(ez
->expression(ez
->OpOr
, a
), yy
.at(0));
586 if (cell
->type
== "$reduce_xor")
587 ez
->SET(ez
->expression(ez
->OpXor
, a
), yy
.at(0));
588 if (cell
->type
== "$reduce_xnor")
589 ez
->SET(ez
->NOT(ez
->expression(ez
->OpXor
, a
)), yy
.at(0));
590 if (cell
->type
== "$logic_not")
591 ez
->SET(ez
->NOT(ez
->expression(ez
->OpOr
, a
)), yy
.at(0));
592 for (size_t i
= 1; i
< y
.size(); i
++)
593 ez
->SET(ez
->CONST_FALSE
, yy
.at(i
));
597 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
598 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
599 int aX
= ez
->expression(ezSAT::OpOr
, undef_a
);
601 if (cell
->type
== "$reduce_and") {
602 int a0
= ez
->expression(ezSAT::OpOr
, ez
->vec_and(ez
->vec_not(a
), ez
->vec_not(undef_a
)));
603 ez
->assume(ez
->IFF(ez
->AND(ez
->NOT(a0
), aX
), undef_y
.at(0)));
605 else if (cell
->type
== "$reduce_or" || cell
->type
== "$reduce_bool" || cell
->type
== "$logic_not") {
606 int a1
= ez
->expression(ezSAT::OpOr
, ez
->vec_and(a
, ez
->vec_not(undef_a
)));
607 ez
->assume(ez
->IFF(ez
->AND(ez
->NOT(a1
), aX
), undef_y
.at(0)));
609 else if (cell
->type
== "$reduce_xor" || cell
->type
== "$reduce_xnor") {
610 ez
->assume(ez
->IFF(aX
, undef_y
.at(0)));
614 for (size_t i
= 1; i
< undef_y
.size(); i
++)
615 ez
->SET(ez
->CONST_FALSE
, undef_y
.at(i
));
617 undefGating(y
, yy
, undef_y
);
622 if (cell
->type
== "$logic_and" || cell
->type
== "$logic_or")
624 std::vector
<int> vec_a
= importDefSigSpec(cell
->getPort("\\A"), timestep
);
625 std::vector
<int> vec_b
= importDefSigSpec(cell
->getPort("\\B"), timestep
);
627 int a
= ez
->expression(ez
->OpOr
, vec_a
);
628 int b
= ez
->expression(ez
->OpOr
, vec_b
);
629 std::vector
<int> y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
631 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
633 if (cell
->type
== "$logic_and")
634 ez
->SET(ez
->expression(ez
->OpAnd
, a
, b
), yy
.at(0));
636 ez
->SET(ez
->expression(ez
->OpOr
, a
, b
), yy
.at(0));
637 for (size_t i
= 1; i
< y
.size(); i
++)
638 ez
->SET(ez
->CONST_FALSE
, yy
.at(i
));
642 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
643 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort("\\B"), timestep
);
644 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
646 int a0
= ez
->NOT(ez
->OR(ez
->expression(ezSAT::OpOr
, vec_a
), ez
->expression(ezSAT::OpOr
, undef_a
)));
647 int b0
= ez
->NOT(ez
->OR(ez
->expression(ezSAT::OpOr
, vec_b
), ez
->expression(ezSAT::OpOr
, undef_b
)));
648 int a1
= ez
->expression(ezSAT::OpOr
, ez
->vec_and(vec_a
, ez
->vec_not(undef_a
)));
649 int b1
= ez
->expression(ezSAT::OpOr
, ez
->vec_and(vec_b
, ez
->vec_not(undef_b
)));
650 int aX
= ez
->expression(ezSAT::OpOr
, undef_a
);
651 int bX
= ez
->expression(ezSAT::OpOr
, undef_b
);
653 if (cell
->type
== "$logic_and")
654 ez
->SET(ez
->AND(ez
->OR(aX
, bX
), ez
->NOT(ez
->AND(a1
, b1
)), ez
->NOT(a0
), ez
->NOT(b0
)), undef_y
.at(0));
655 else if (cell
->type
== "$logic_or")
656 ez
->SET(ez
->AND(ez
->OR(aX
, bX
), ez
->NOT(ez
->AND(a0
, b0
)), ez
->NOT(a1
), ez
->NOT(b1
)), undef_y
.at(0));
660 for (size_t i
= 1; i
< undef_y
.size(); i
++)
661 ez
->SET(ez
->CONST_FALSE
, undef_y
.at(i
));
663 undefGating(y
, yy
, undef_y
);
668 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")
670 bool is_signed
= cell
->parameters
["\\A_SIGNED"].as_bool() && cell
->parameters
["\\B_SIGNED"].as_bool();
671 std::vector
<int> a
= importDefSigSpec(cell
->getPort("\\A"), timestep
);
672 std::vector
<int> b
= importDefSigSpec(cell
->getPort("\\B"), timestep
);
673 std::vector
<int> y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
674 extendSignalWidth(a
, b
, cell
);
676 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
678 if (model_undef
&& (cell
->type
== "$eqx" || cell
->type
== "$nex")) {
679 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
680 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort("\\B"), timestep
);
681 extendSignalWidth(undef_a
, undef_b
, cell
, true);
682 a
= ez
->vec_or(a
, undef_a
);
683 b
= ez
->vec_or(b
, undef_b
);
686 if (cell
->type
== "$lt")
687 ez
->SET(is_signed
? ez
->vec_lt_signed(a
, b
) : ez
->vec_lt_unsigned(a
, b
), yy
.at(0));
688 if (cell
->type
== "$le")
689 ez
->SET(is_signed
? ez
->vec_le_signed(a
, b
) : ez
->vec_le_unsigned(a
, b
), yy
.at(0));
690 if (cell
->type
== "$eq" || cell
->type
== "$eqx")
691 ez
->SET(ez
->vec_eq(a
, b
), yy
.at(0));
692 if (cell
->type
== "$ne" || cell
->type
== "$nex")
693 ez
->SET(ez
->vec_ne(a
, b
), yy
.at(0));
694 if (cell
->type
== "$ge")
695 ez
->SET(is_signed
? ez
->vec_ge_signed(a
, b
) : ez
->vec_ge_unsigned(a
, b
), yy
.at(0));
696 if (cell
->type
== "$gt")
697 ez
->SET(is_signed
? ez
->vec_gt_signed(a
, b
) : ez
->vec_gt_unsigned(a
, b
), yy
.at(0));
698 for (size_t i
= 1; i
< y
.size(); i
++)
699 ez
->SET(ez
->CONST_FALSE
, yy
.at(i
));
701 if (model_undef
&& (cell
->type
== "$eqx" || cell
->type
== "$nex"))
703 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
704 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort("\\B"), timestep
);
705 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
706 extendSignalWidth(undef_a
, undef_b
, cell
, true);
708 if (cell
->type
== "$eqx")
709 yy
.at(0) = ez
->AND(yy
.at(0), ez
->vec_eq(undef_a
, undef_b
));
711 yy
.at(0) = ez
->OR(yy
.at(0), ez
->vec_ne(undef_a
, undef_b
));
713 for (size_t i
= 0; i
< y
.size(); i
++)
714 ez
->SET(ez
->CONST_FALSE
, undef_y
.at(i
));
716 ez
->assume(ez
->vec_eq(y
, yy
));
718 else if (model_undef
&& (cell
->type
== "$eq" || cell
->type
== "$ne"))
720 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
721 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort("\\B"), timestep
);
722 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
723 extendSignalWidth(undef_a
, undef_b
, cell
, true);
725 int undef_any_a
= ez
->expression(ezSAT::OpOr
, undef_a
);
726 int undef_any_b
= ez
->expression(ezSAT::OpOr
, undef_b
);
727 int undef_any
= ez
->OR(undef_any_a
, undef_any_b
);
729 std::vector
<int> masked_a_bits
= ez
->vec_or(a
, ez
->vec_or(undef_a
, undef_b
));
730 std::vector
<int> masked_b_bits
= ez
->vec_or(b
, ez
->vec_or(undef_a
, undef_b
));
732 int masked_ne
= ez
->vec_ne(masked_a_bits
, masked_b_bits
);
733 int undef_y_bit
= ez
->AND(undef_any
, ez
->NOT(masked_ne
));
735 for (size_t i
= 1; i
< undef_y
.size(); i
++)
736 ez
->SET(ez
->CONST_FALSE
, undef_y
.at(i
));
737 ez
->SET(undef_y_bit
, undef_y
.at(0));
739 undefGating(y
, yy
, undef_y
);
744 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
745 undefGating(y
, yy
, undef_y
);
747 log_assert(!model_undef
|| arith_undef_handled
);
752 if (cell
->type
== "$shl" || cell
->type
== "$shr" || cell
->type
== "$sshl" || cell
->type
== "$sshr" || cell
->type
== "$shift" || cell
->type
== "$shiftx")
754 std::vector
<int> a
= importDefSigSpec(cell
->getPort("\\A"), timestep
);
755 std::vector
<int> b
= importDefSigSpec(cell
->getPort("\\B"), timestep
);
756 std::vector
<int> y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
758 int extend_bit
= ez
->CONST_FALSE
;
760 if (!cell
->type
.in("$shift", "$shiftx") && cell
->parameters
["\\A_SIGNED"].as_bool())
761 extend_bit
= a
.back();
763 while (y
.size() < a
.size())
764 y
.push_back(ez
->literal());
765 while (y
.size() > a
.size())
766 a
.push_back(extend_bit
);
768 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
769 std::vector
<int> shifted_a
;
771 if (cell
->type
== "$shl" || cell
->type
== "$sshl")
772 shifted_a
= ez
->vec_shift_left(a
, b
, false, ez
->CONST_FALSE
, ez
->CONST_FALSE
);
774 if (cell
->type
== "$shr")
775 shifted_a
= ez
->vec_shift_right(a
, b
, false, ez
->CONST_FALSE
, ez
->CONST_FALSE
);
777 if (cell
->type
== "$sshr")
778 shifted_a
= ez
->vec_shift_right(a
, b
, false, cell
->parameters
["\\A_SIGNED"].as_bool() ? a
.back() : ez
->CONST_FALSE
, ez
->CONST_FALSE
);
780 if (cell
->type
== "$shift" || cell
->type
== "$shiftx")
781 shifted_a
= ez
->vec_shift_right(a
, b
, cell
->parameters
["\\B_SIGNED"].as_bool(), ez
->CONST_FALSE
, ez
->CONST_FALSE
);
783 ez
->assume(ez
->vec_eq(shifted_a
, yy
));
787 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
788 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort("\\B"), timestep
);
789 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
790 std::vector
<int> undef_a_shifted
;
792 extend_bit
= cell
->type
== "$shiftx" ? ez
->CONST_TRUE
: ez
->CONST_FALSE
;
793 if (!cell
->type
.in("$shift", "$shiftx") && cell
->parameters
["\\A_SIGNED"].as_bool())
794 extend_bit
= undef_a
.back();
796 while (undef_y
.size() < undef_a
.size())
797 undef_y
.push_back(ez
->literal());
798 while (undef_y
.size() > undef_a
.size())
799 undef_a
.push_back(extend_bit
);
801 if (cell
->type
== "$shl" || cell
->type
== "$sshl")
802 undef_a_shifted
= ez
->vec_shift_left(undef_a
, b
, false, ez
->CONST_FALSE
, ez
->CONST_FALSE
);
804 if (cell
->type
== "$shr")
805 undef_a_shifted
= ez
->vec_shift_right(undef_a
, b
, false, ez
->CONST_FALSE
, ez
->CONST_FALSE
);
807 if (cell
->type
== "$sshr")
808 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
);
810 if (cell
->type
== "$shift")
811 undef_a_shifted
= ez
->vec_shift_right(undef_a
, b
, cell
->parameters
["\\B_SIGNED"].as_bool(), ez
->CONST_FALSE
, ez
->CONST_FALSE
);
813 if (cell
->type
== "$shiftx")
814 undef_a_shifted
= ez
->vec_shift_right(undef_a
, b
, cell
->parameters
["\\B_SIGNED"].as_bool(), ez
->CONST_TRUE
, ez
->CONST_TRUE
);
816 int undef_any_b
= ez
->expression(ezSAT::OpOr
, undef_b
);
817 std::vector
<int> undef_all_y_bits(undef_y
.size(), undef_any_b
);
818 ez
->assume(ez
->vec_eq(ez
->vec_or(undef_a_shifted
, undef_all_y_bits
), undef_y
));
819 undefGating(y
, yy
, undef_y
);
824 if (cell
->type
== "$mul")
826 std::vector
<int> a
= importDefSigSpec(cell
->getPort("\\A"), timestep
);
827 std::vector
<int> b
= importDefSigSpec(cell
->getPort("\\B"), timestep
);
828 std::vector
<int> y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
829 extendSignalWidth(a
, b
, y
, cell
);
831 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
833 std::vector
<int> tmp(a
.size(), ez
->CONST_FALSE
);
834 for (int i
= 0; i
< int(a
.size()); i
++)
836 std::vector
<int> shifted_a(a
.size(), ez
->CONST_FALSE
);
837 for (int j
= i
; j
< int(a
.size()); j
++)
838 shifted_a
.at(j
) = a
.at(j
-i
);
839 tmp
= ez
->vec_ite(b
.at(i
), ez
->vec_add(tmp
, shifted_a
), tmp
);
841 ez
->assume(ez
->vec_eq(tmp
, yy
));
844 log_assert(arith_undef_handled
);
845 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
846 undefGating(y
, yy
, undef_y
);
851 if (cell
->type
== "$macc")
853 std::vector
<int> a
= importDefSigSpec(cell
->getPort("\\A"), timestep
);
854 std::vector
<int> b
= importDefSigSpec(cell
->getPort("\\B"), timestep
);
855 std::vector
<int> y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
858 macc
.from_cell(cell
);
860 std::vector
<int> tmp(GetSize(y
), ez
->CONST_FALSE
);
862 for (auto &port
: macc
.ports
)
864 std::vector
<int> in_a
= importDefSigSpec(port
.in_a
, timestep
);
865 std::vector
<int> in_b
= importDefSigSpec(port
.in_b
, timestep
);
867 while (GetSize(in_a
) < GetSize(y
))
868 in_a
.push_back(port
.is_signed
&& !in_a
.empty() ? in_a
.back() : ez
->CONST_FALSE
);
869 in_a
.resize(GetSize(y
));
873 while (GetSize(in_b
) < GetSize(y
))
874 in_b
.push_back(port
.is_signed
&& !in_b
.empty() ? in_b
.back() : ez
->CONST_FALSE
);
875 in_b
.resize(GetSize(y
));
877 for (int i
= 0; i
< GetSize(in_b
); i
++) {
878 std::vector
<int> shifted_a(in_a
.size(), ez
->CONST_FALSE
);
879 for (int j
= i
; j
< int(in_a
.size()); j
++)
880 shifted_a
.at(j
) = in_a
.at(j
-i
);
881 if (port
.do_subtract
)
882 tmp
= ez
->vec_ite(in_b
.at(i
), ez
->vec_sub(tmp
, shifted_a
), tmp
);
884 tmp
= ez
->vec_ite(in_b
.at(i
), ez
->vec_add(tmp
, shifted_a
), tmp
);
889 if (port
.do_subtract
)
890 tmp
= ez
->vec_sub(tmp
, in_a
);
892 tmp
= ez
->vec_add(tmp
, in_a
);
896 for (int i
= 0; i
< GetSize(b
); i
++) {
897 std::vector
<int> val(GetSize(y
), ez
->CONST_FALSE
);
899 tmp
= ez
->vec_add(tmp
, val
);
904 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
905 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort("\\B"), timestep
);
907 int undef_any_a
= ez
->expression(ezSAT::OpOr
, undef_a
);
908 int undef_any_b
= ez
->expression(ezSAT::OpOr
, undef_b
);
910 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
911 ez
->assume(ez
->vec_eq(undef_y
, std::vector
<int>(GetSize(y
), ez
->OR(undef_any_a
, undef_any_b
))));
913 undefGating(y
, tmp
, undef_y
);
916 ez
->assume(ez
->vec_eq(y
, tmp
));
921 if (cell
->type
== "$div" || cell
->type
== "$mod")
923 std::vector
<int> a
= importDefSigSpec(cell
->getPort("\\A"), timestep
);
924 std::vector
<int> b
= importDefSigSpec(cell
->getPort("\\B"), timestep
);
925 std::vector
<int> y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
926 extendSignalWidth(a
, b
, y
, cell
);
928 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
930 std::vector
<int> a_u
, b_u
;
931 if (cell
->parameters
["\\A_SIGNED"].as_bool() && cell
->parameters
["\\B_SIGNED"].as_bool()) {
932 a_u
= ez
->vec_ite(a
.back(), ez
->vec_neg(a
), a
);
933 b_u
= ez
->vec_ite(b
.back(), ez
->vec_neg(b
), b
);
939 std::vector
<int> chain_buf
= a_u
;
940 std::vector
<int> y_u(a_u
.size(), ez
->CONST_FALSE
);
941 for (int i
= int(a
.size())-1; i
>= 0; i
--)
943 chain_buf
.insert(chain_buf
.end(), chain_buf
.size(), ez
->CONST_FALSE
);
945 std::vector
<int> b_shl(i
, ez
->CONST_FALSE
);
946 b_shl
.insert(b_shl
.end(), b_u
.begin(), b_u
.end());
947 b_shl
.insert(b_shl
.end(), chain_buf
.size()-b_shl
.size(), ez
->CONST_FALSE
);
949 y_u
.at(i
) = ez
->vec_ge_unsigned(chain_buf
, b_shl
);
950 chain_buf
= ez
->vec_ite(y_u
.at(i
), ez
->vec_sub(chain_buf
, b_shl
), chain_buf
);
952 chain_buf
.erase(chain_buf
.begin() + a_u
.size(), chain_buf
.end());
955 std::vector
<int> y_tmp
= ignore_div_by_zero
? yy
: ez
->vec_var(y
.size());
956 if (cell
->type
== "$div") {
957 if (cell
->parameters
["\\A_SIGNED"].as_bool() && cell
->parameters
["\\B_SIGNED"].as_bool())
958 ez
->assume(ez
->vec_eq(y_tmp
, ez
->vec_ite(ez
->XOR(a
.back(), b
.back()), ez
->vec_neg(y_u
), y_u
)));
960 ez
->assume(ez
->vec_eq(y_tmp
, y_u
));
962 if (cell
->parameters
["\\A_SIGNED"].as_bool() && cell
->parameters
["\\B_SIGNED"].as_bool())
963 ez
->assume(ez
->vec_eq(y_tmp
, ez
->vec_ite(a
.back(), ez
->vec_neg(chain_buf
), chain_buf
)));
965 ez
->assume(ez
->vec_eq(y_tmp
, chain_buf
));
968 if (ignore_div_by_zero
) {
969 ez
->assume(ez
->expression(ezSAT::OpOr
, b
));
971 std::vector
<int> div_zero_result
;
972 if (cell
->type
== "$div") {
973 if (cell
->parameters
["\\A_SIGNED"].as_bool() && cell
->parameters
["\\B_SIGNED"].as_bool()) {
974 std::vector
<int> all_ones(y
.size(), ez
->CONST_TRUE
);
975 std::vector
<int> only_first_one(y
.size(), ez
->CONST_FALSE
);
976 only_first_one
.at(0) = ez
->CONST_TRUE
;
977 div_zero_result
= ez
->vec_ite(a
.back(), only_first_one
, all_ones
);
979 div_zero_result
.insert(div_zero_result
.end(), cell
->getPort("\\A").size(), ez
->CONST_TRUE
);
980 div_zero_result
.insert(div_zero_result
.end(), y
.size() - div_zero_result
.size(), ez
->CONST_FALSE
);
983 int copy_a_bits
= std::min(cell
->getPort("\\A").size(), cell
->getPort("\\B").size());
984 div_zero_result
.insert(div_zero_result
.end(), a
.begin(), a
.begin() + copy_a_bits
);
985 if (cell
->parameters
["\\A_SIGNED"].as_bool() && cell
->parameters
["\\B_SIGNED"].as_bool())
986 div_zero_result
.insert(div_zero_result
.end(), y
.size() - div_zero_result
.size(), div_zero_result
.back());
988 div_zero_result
.insert(div_zero_result
.end(), y
.size() - div_zero_result
.size(), ez
->CONST_FALSE
);
990 ez
->assume(ez
->vec_eq(yy
, ez
->vec_ite(ez
->expression(ezSAT::OpOr
, b
), y_tmp
, div_zero_result
)));
994 log_assert(arith_undef_handled
);
995 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
996 undefGating(y
, yy
, undef_y
);
1001 if (cell
->type
== "$lut")
1003 std::vector
<int> a
= importDefSigSpec(cell
->getPort("\\A"), timestep
);
1004 std::vector
<int> y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
1006 std::vector
<int> lut
;
1007 for (auto bit
: cell
->getParam("\\LUT").bits
)
1008 lut
.push_back(bit
== RTLIL::S1
? ez
->CONST_TRUE
: ez
->CONST_FALSE
);
1009 while (GetSize(lut
) < (1 << GetSize(a
)))
1010 lut
.push_back(ez
->CONST_FALSE
);
1011 lut
.resize(1 << GetSize(a
));
1015 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
1016 std::vector
<int> t(lut
), u(GetSize(t
), ez
->CONST_FALSE
);
1018 for (int i
= GetSize(a
)-1; i
>= 0; i
--)
1020 std::vector
<int> t0(t
.begin(), t
.begin() + GetSize(t
)/2);
1021 std::vector
<int> t1(t
.begin() + GetSize(t
)/2, t
.end());
1023 std::vector
<int> u0(u
.begin(), u
.begin() + GetSize(u
)/2);
1024 std::vector
<int> u1(u
.begin() + GetSize(u
)/2, u
.end());
1026 t
= ez
->vec_ite(a
[i
], t1
, t0
);
1027 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
));
1030 log_assert(GetSize(t
) == 1);
1031 log_assert(GetSize(u
) == 1);
1032 undefGating(y
, t
, u
);
1033 ez
->assume(ez
->vec_eq(importUndefSigSpec(cell
->getPort("\\Y"), timestep
), u
));
1037 std::vector
<int> t
= lut
;
1038 for (int i
= GetSize(a
)-1; i
>= 0; i
--)
1040 std::vector
<int> t0(t
.begin(), t
.begin() + GetSize(t
)/2);
1041 std::vector
<int> t1(t
.begin() + GetSize(t
)/2, t
.end());
1042 t
= ez
->vec_ite(a
[i
], t1
, t0
);
1045 log_assert(GetSize(t
) == 1);
1046 ez
->assume(ez
->vec_eq(y
, t
));
1051 if (cell
->type
== "$fa")
1053 std::vector
<int> a
= importDefSigSpec(cell
->getPort("\\A"), timestep
);
1054 std::vector
<int> b
= importDefSigSpec(cell
->getPort("\\B"), timestep
);
1055 std::vector
<int> c
= importDefSigSpec(cell
->getPort("\\C"), timestep
);
1056 std::vector
<int> y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
1057 std::vector
<int> x
= importDefSigSpec(cell
->getPort("\\X"), timestep
);
1059 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
1060 std::vector
<int> xx
= model_undef
? ez
->vec_var(x
.size()) : x
;
1062 std::vector
<int> t1
= ez
->vec_xor(a
, b
);
1063 ez
->assume(ez
->vec_eq(yy
, ez
->vec_xor(t1
, c
)));
1065 std::vector
<int> t2
= ez
->vec_and(a
, b
);
1066 std::vector
<int> t3
= ez
->vec_and(c
, t1
);
1067 ez
->assume(ez
->vec_eq(xx
, ez
->vec_or(t2
, t3
)));
1071 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
1072 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort("\\B"), timestep
);
1073 std::vector
<int> undef_c
= importUndefSigSpec(cell
->getPort("\\C"), timestep
);
1075 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
1076 std::vector
<int> undef_x
= importUndefSigSpec(cell
->getPort("\\X"), timestep
);
1078 ez
->assume(ez
->vec_eq(undef_y
, ez
->vec_or(ez
->vec_or(undef_a
, undef_b
), undef_c
)));
1079 ez
->assume(ez
->vec_eq(undef_x
, undef_y
));
1081 undefGating(y
, yy
, undef_y
);
1082 undefGating(x
, xx
, undef_x
);
1087 if (cell
->type
== "$lcu")
1089 std::vector
<int> p
= importDefSigSpec(cell
->getPort("\\P"), timestep
);
1090 std::vector
<int> g
= importDefSigSpec(cell
->getPort("\\G"), timestep
);
1091 std::vector
<int> ci
= importDefSigSpec(cell
->getPort("\\CI"), timestep
);
1092 std::vector
<int> co
= importDefSigSpec(cell
->getPort("\\CO"), timestep
);
1094 std::vector
<int> yy
= model_undef
? ez
->vec_var(co
.size()) : co
;
1096 for (int i
= 0; i
< GetSize(co
); i
++)
1097 ez
->SET(yy
[i
], ez
->OR(g
[i
], ez
->AND(p
[i
], i
? yy
[i
-1] : ci
[0])));
1101 std::vector
<int> undef_p
= importUndefSigSpec(cell
->getPort("\\P"), timestep
);
1102 std::vector
<int> undef_g
= importUndefSigSpec(cell
->getPort("\\G"), timestep
);
1103 std::vector
<int> undef_ci
= importUndefSigSpec(cell
->getPort("\\CI"), timestep
);
1104 std::vector
<int> undef_co
= importUndefSigSpec(cell
->getPort("\\CO"), timestep
);
1106 int undef_any_p
= ez
->expression(ezSAT::OpOr
, undef_p
);
1107 int undef_any_g
= ez
->expression(ezSAT::OpOr
, undef_g
);
1108 int undef_any_ci
= ez
->expression(ezSAT::OpOr
, undef_ci
);
1109 int undef_co_bit
= ez
->OR(undef_any_p
, undef_any_g
, undef_any_ci
);
1111 std::vector
<int> undef_co_bits(undef_co
.size(), undef_co_bit
);
1112 ez
->assume(ez
->vec_eq(undef_co_bits
, undef_co
));
1114 undefGating(co
, yy
, undef_co
);
1119 if (cell
->type
== "$alu")
1121 std::vector
<int> a
= importDefSigSpec(cell
->getPort("\\A"), timestep
);
1122 std::vector
<int> b
= importDefSigSpec(cell
->getPort("\\B"), timestep
);
1123 std::vector
<int> y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
1124 std::vector
<int> x
= importDefSigSpec(cell
->getPort("\\X"), timestep
);
1125 std::vector
<int> ci
= importDefSigSpec(cell
->getPort("\\CI"), timestep
);
1126 std::vector
<int> bi
= importDefSigSpec(cell
->getPort("\\BI"), timestep
);
1127 std::vector
<int> co
= importDefSigSpec(cell
->getPort("\\CO"), timestep
);
1129 extendSignalWidth(a
, b
, y
, cell
);
1130 extendSignalWidth(a
, b
, x
, cell
);
1131 extendSignalWidth(a
, b
, co
, cell
);
1133 std::vector
<int> def_y
= model_undef
? ez
->vec_var(y
.size()) : y
;
1134 std::vector
<int> def_x
= model_undef
? ez
->vec_var(x
.size()) : x
;
1135 std::vector
<int> def_co
= model_undef
? ez
->vec_var(co
.size()) : co
;
1137 log_assert(GetSize(y
) == GetSize(x
));
1138 log_assert(GetSize(y
) == GetSize(co
));
1139 log_assert(GetSize(ci
) == 1);
1140 log_assert(GetSize(bi
) == 1);
1142 for (int i
= 0; i
< GetSize(y
); i
++)
1144 int s1
= a
.at(i
), s2
= ez
->XOR(b
.at(i
), bi
.at(0)), s3
= i
? co
.at(i
-1) : ci
.at(0);
1145 ez
->SET(def_x
.at(i
), ez
->XOR(s1
, s2
));
1146 ez
->SET(def_y
.at(i
), ez
->XOR(def_x
.at(i
), s3
));
1147 ez
->SET(def_co
.at(i
), ez
->OR(ez
->AND(s1
, s2
), ez
->AND(s1
, s3
), ez
->AND(s2
, s3
)));
1152 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
1153 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort("\\B"), timestep
);
1154 std::vector
<int> undef_ci
= importUndefSigSpec(cell
->getPort("\\CI"), timestep
);
1155 std::vector
<int> undef_bi
= importUndefSigSpec(cell
->getPort("\\BI"), timestep
);
1157 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
1158 std::vector
<int> undef_x
= importUndefSigSpec(cell
->getPort("\\X"), timestep
);
1159 std::vector
<int> undef_co
= importUndefSigSpec(cell
->getPort("\\CO"), timestep
);
1161 extendSignalWidth(undef_a
, undef_b
, undef_y
, cell
);
1162 extendSignalWidth(undef_a
, undef_b
, undef_x
, cell
);
1163 extendSignalWidth(undef_a
, undef_b
, undef_co
, cell
);
1165 std::vector
<int> all_inputs_undef
;
1166 all_inputs_undef
.insert(all_inputs_undef
.end(), undef_a
.begin(), undef_a
.end());
1167 all_inputs_undef
.insert(all_inputs_undef
.end(), undef_b
.begin(), undef_b
.end());
1168 all_inputs_undef
.insert(all_inputs_undef
.end(), undef_ci
.begin(), undef_ci
.end());
1169 all_inputs_undef
.insert(all_inputs_undef
.end(), undef_bi
.begin(), undef_bi
.end());
1170 int undef_any
= ez
->expression(ezSAT::OpOr
, all_inputs_undef
);
1172 for (int i
= 0; i
< GetSize(undef_y
); i
++) {
1173 ez
->SET(undef_y
.at(i
), undef_any
);
1174 ez
->SET(undef_x
.at(i
), ez
->OR(undef_a
.at(i
), undef_b
.at(i
), undef_bi
.at(0)));
1175 ez
->SET(undef_co
.at(i
), undef_any
);
1178 undefGating(y
, def_y
, undef_y
);
1179 undefGating(x
, def_x
, undef_x
);
1180 undefGating(co
, def_co
, undef_co
);
1185 if (cell
->type
== "$slice")
1187 RTLIL::SigSpec a
= cell
->getPort("\\A");
1188 RTLIL::SigSpec y
= cell
->getPort("\\Y");
1189 ez
->assume(signals_eq(a
.extract(cell
->parameters
.at("\\OFFSET").as_int(), y
.size()), y
, timestep
));
1193 if (cell
->type
== "$concat")
1195 RTLIL::SigSpec a
= cell
->getPort("\\A");
1196 RTLIL::SigSpec b
= cell
->getPort("\\B");
1197 RTLIL::SigSpec y
= cell
->getPort("\\Y");
1199 RTLIL::SigSpec ab
= a
;
1202 ez
->assume(signals_eq(ab
, y
, timestep
));
1206 if (timestep
> 0 && (cell
->type
== "$dff" || cell
->type
== "$_DFF_N_" || cell
->type
== "$_DFF_P_"))
1210 initial_state
.add((*sigmap
)(cell
->getPort("\\Q")));
1214 std::vector
<int> d
= importDefSigSpec(cell
->getPort("\\D"), timestep
-1);
1215 std::vector
<int> q
= importDefSigSpec(cell
->getPort("\\Q"), timestep
);
1217 std::vector
<int> qq
= model_undef
? ez
->vec_var(q
.size()) : q
;
1218 ez
->assume(ez
->vec_eq(d
, qq
));
1222 std::vector
<int> undef_d
= importUndefSigSpec(cell
->getPort("\\D"), timestep
-1);
1223 std::vector
<int> undef_q
= importUndefSigSpec(cell
->getPort("\\Q"), timestep
);
1225 ez
->assume(ez
->vec_eq(undef_d
, undef_q
));
1226 undefGating(q
, qq
, undef_q
);
1232 if (cell
->type
== "$_BUF_" || cell
->type
== "$equiv")
1234 std::vector
<int> a
= importDefSigSpec(cell
->getPort("\\A"), timestep
);
1235 std::vector
<int> y
= importDefSigSpec(cell
->getPort("\\Y"), timestep
);
1236 extendSignalWidthUnary(a
, y
, cell
);
1238 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
1239 ez
->assume(ez
->vec_eq(a
, yy
));
1242 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort("\\A"), timestep
);
1243 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort("\\Y"), timestep
);
1244 extendSignalWidthUnary(undef_a
, undef_y
, cell
, false);
1245 ez
->assume(ez
->vec_eq(undef_a
, undef_y
));
1246 undefGating(y
, yy
, undef_y
);
1251 if (cell
->type
== "$assert")
1253 std::string pf
= prefix
+ (timestep
== -1 ? "" : stringf("@%d:", timestep
));
1254 asserts_a
[pf
].append((*sigmap
)(cell
->getPort("\\A")));
1255 asserts_en
[pf
].append((*sigmap
)(cell
->getPort("\\EN")));
1259 if (cell
->type
== "$assume")
1261 std::string pf
= prefix
+ (timestep
== -1 ? "" : stringf("@%d:", timestep
));
1262 assumes_a
[pf
].append((*sigmap
)(cell
->getPort("\\A")));
1263 assumes_en
[pf
].append((*sigmap
)(cell
->getPort("\\EN")));
1267 // Unsupported internal cell types: $pow $lut
1268 // .. and all sequential cells except $dff and $_DFF_[NP]_