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.
20 #include "kernel/satgen.h"
21 #include "kernel/ff.h"
25 bool SatGen::importCell(RTLIL::Cell
*cell
, int timestep
)
27 bool arith_undef_handled
= false;
28 bool is_arith_compare
= cell
->type
.in(ID($lt
), ID($le
), ID($ge
), ID($gt
));
30 if (model_undef
&& (cell
->type
.in(ID($add
), ID($sub
), ID($mul
), ID($div
), ID($mod
), ID($divfloor
), ID($modfloor
)) || is_arith_compare
))
32 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort(ID::A
), timestep
);
33 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort(ID::B
), timestep
);
34 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort(ID::Y
), timestep
);
36 extendSignalWidth(undef_a
, undef_b
, cell
, true);
38 extendSignalWidth(undef_a
, undef_b
, undef_y
, cell
, true);
40 int undef_any_a
= ez
->expression(ezSAT::OpOr
, undef_a
);
41 int undef_any_b
= ez
->expression(ezSAT::OpOr
, undef_b
);
42 int undef_y_bit
= ez
->OR(undef_any_a
, undef_any_b
);
44 if (cell
->type
.in(ID($div
), ID($mod
), ID($divfloor
), ID($modfloor
))) {
45 std::vector
<int> b
= importSigSpec(cell
->getPort(ID::B
), timestep
);
46 undef_y_bit
= ez
->OR(undef_y_bit
, ez
->NOT(ez
->expression(ezSAT::OpOr
, b
)));
49 if (is_arith_compare
) {
50 for (size_t i
= 1; i
< undef_y
.size(); i
++)
51 ez
->SET(ez
->CONST_FALSE
, undef_y
.at(i
));
52 ez
->SET(undef_y_bit
, undef_y
.at(0));
54 std::vector
<int> undef_y_bits(undef_y
.size(), undef_y_bit
);
55 ez
->assume(ez
->vec_eq(undef_y_bits
, undef_y
));
58 arith_undef_handled
= true;
61 if (cell
->type
.in(ID($_AND_
), ID($_NAND_
), ID($_OR_
), ID($_NOR_
), ID($_XOR_
), ID($_XNOR_
), ID($_ANDNOT_
), ID($_ORNOT_
),
62 ID($
and), ID($
or), ID($
xor), ID($xnor
), ID($add
), ID($sub
)))
64 std::vector
<int> a
= importDefSigSpec(cell
->getPort(ID::A
), timestep
);
65 std::vector
<int> b
= importDefSigSpec(cell
->getPort(ID::B
), timestep
);
66 std::vector
<int> y
= importDefSigSpec(cell
->getPort(ID::Y
), timestep
);
67 extendSignalWidth(a
, b
, y
, cell
);
69 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
71 if (cell
->type
.in(ID($
and), ID($_AND_
)))
72 ez
->assume(ez
->vec_eq(ez
->vec_and(a
, b
), yy
));
73 if (cell
->type
== ID($_NAND_
))
74 ez
->assume(ez
->vec_eq(ez
->vec_not(ez
->vec_and(a
, b
)), yy
));
75 if (cell
->type
.in(ID($
or), ID($_OR_
)))
76 ez
->assume(ez
->vec_eq(ez
->vec_or(a
, b
), yy
));
77 if (cell
->type
== ID($_NOR_
))
78 ez
->assume(ez
->vec_eq(ez
->vec_not(ez
->vec_or(a
, b
)), yy
));
79 if (cell
->type
.in(ID($
xor), ID($_XOR_
)))
80 ez
->assume(ez
->vec_eq(ez
->vec_xor(a
, b
), yy
));
81 if (cell
->type
.in(ID($xnor
), ID($_XNOR_
)))
82 ez
->assume(ez
->vec_eq(ez
->vec_not(ez
->vec_xor(a
, b
)), yy
));
83 if (cell
->type
== ID($_ANDNOT_
))
84 ez
->assume(ez
->vec_eq(ez
->vec_and(a
, ez
->vec_not(b
)), yy
));
85 if (cell
->type
== ID($_ORNOT_
))
86 ez
->assume(ez
->vec_eq(ez
->vec_or(a
, ez
->vec_not(b
)), yy
));
87 if (cell
->type
== ID($add
))
88 ez
->assume(ez
->vec_eq(ez
->vec_add(a
, b
), yy
));
89 if (cell
->type
== ID($sub
))
90 ez
->assume(ez
->vec_eq(ez
->vec_sub(a
, b
), yy
));
92 if (model_undef
&& !arith_undef_handled
)
94 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort(ID::A
), timestep
);
95 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort(ID::B
), timestep
);
96 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort(ID::Y
), timestep
);
97 extendSignalWidth(undef_a
, undef_b
, undef_y
, cell
, false);
99 if (cell
->type
.in(ID($
and), ID($_AND_
), ID($_NAND_
))) {
100 std::vector
<int> a0
= ez
->vec_and(ez
->vec_not(a
), ez
->vec_not(undef_a
));
101 std::vector
<int> b0
= ez
->vec_and(ez
->vec_not(b
), ez
->vec_not(undef_b
));
102 std::vector
<int> yX
= ez
->vec_and(ez
->vec_or(undef_a
, undef_b
), ez
->vec_not(ez
->vec_or(a0
, b0
)));
103 ez
->assume(ez
->vec_eq(yX
, undef_y
));
105 else if (cell
->type
.in(ID($
or), ID($_OR_
), ID($_NOR_
))) {
106 std::vector
<int> a1
= ez
->vec_and(a
, ez
->vec_not(undef_a
));
107 std::vector
<int> b1
= ez
->vec_and(b
, ez
->vec_not(undef_b
));
108 std::vector
<int> yX
= ez
->vec_and(ez
->vec_or(undef_a
, undef_b
), ez
->vec_not(ez
->vec_or(a1
, b1
)));
109 ez
->assume(ez
->vec_eq(yX
, undef_y
));
111 else if (cell
->type
.in(ID($
xor), ID($xnor
), ID($_XOR_
), ID($_XNOR_
))) {
112 std::vector
<int> yX
= ez
->vec_or(undef_a
, undef_b
);
113 ez
->assume(ez
->vec_eq(yX
, undef_y
));
115 else if (cell
->type
== ID($_ANDNOT_
)) {
116 std::vector
<int> a0
= ez
->vec_and(ez
->vec_not(a
), ez
->vec_not(undef_a
));
117 std::vector
<int> b1
= ez
->vec_and(b
, ez
->vec_not(undef_b
));
118 std::vector
<int> yX
= ez
->vec_and(ez
->vec_or(undef_a
, undef_b
), ez
->vec_not(ez
->vec_or(a0
, b1
)));
119 ez
->assume(ez
->vec_eq(yX
, undef_y
));
122 else if (cell
->type
== ID($_ORNOT_
)) {
123 std::vector
<int> a1
= ez
->vec_and(a
, ez
->vec_not(undef_a
));
124 std::vector
<int> b0
= ez
->vec_and(ez
->vec_not(b
), ez
->vec_not(undef_b
));
125 std::vector
<int> yX
= ez
->vec_and(ez
->vec_or(undef_a
, undef_b
), ez
->vec_not(ez
->vec_or(a1
, b0
)));
126 ez
->assume(ez
->vec_eq(yX
, undef_y
));
131 undefGating(y
, yy
, undef_y
);
133 else if (model_undef
)
135 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort(ID::Y
), timestep
);
136 undefGating(y
, yy
, undef_y
);
141 if (cell
->type
.in(ID($_AOI3_
), ID($_OAI3_
), ID($_AOI4_
), ID($_OAI4_
)))
143 bool aoi_mode
= cell
->type
.in(ID($_AOI3_
), ID($_AOI4_
));
144 bool three_mode
= cell
->type
.in(ID($_AOI3_
), ID($_OAI3_
));
146 int a
= importDefSigSpec(cell
->getPort(ID::A
), timestep
).at(0);
147 int b
= importDefSigSpec(cell
->getPort(ID::B
), timestep
).at(0);
148 int c
= importDefSigSpec(cell
->getPort(ID::C
), timestep
).at(0);
149 int d
= three_mode
? (aoi_mode
? ez
->CONST_TRUE
: ez
->CONST_FALSE
) : importDefSigSpec(cell
->getPort(ID::D
), timestep
).at(0);
150 int y
= importDefSigSpec(cell
->getPort(ID::Y
), timestep
).at(0);
151 int yy
= model_undef
? ez
->literal() : y
;
153 if (cell
->type
.in(ID($_AOI3_
), ID($_AOI4_
)))
154 ez
->assume(ez
->IFF(ez
->NOT(ez
->OR(ez
->AND(a
, b
), ez
->AND(c
, d
))), yy
));
156 ez
->assume(ez
->IFF(ez
->NOT(ez
->AND(ez
->OR(a
, b
), ez
->OR(c
, d
))), yy
));
160 int undef_a
= importUndefSigSpec(cell
->getPort(ID::A
), timestep
).at(0);
161 int undef_b
= importUndefSigSpec(cell
->getPort(ID::B
), timestep
).at(0);
162 int undef_c
= importUndefSigSpec(cell
->getPort(ID::C
), timestep
).at(0);
163 int undef_d
= three_mode
? ez
->CONST_FALSE
: importUndefSigSpec(cell
->getPort(ID::D
), timestep
).at(0);
164 int undef_y
= importUndefSigSpec(cell
->getPort(ID::Y
), timestep
).at(0);
168 int a0
= ez
->AND(ez
->NOT(a
), ez
->NOT(undef_a
));
169 int b0
= ez
->AND(ez
->NOT(b
), ez
->NOT(undef_b
));
170 int c0
= ez
->AND(ez
->NOT(c
), ez
->NOT(undef_c
));
171 int d0
= ez
->AND(ez
->NOT(d
), ez
->NOT(undef_d
));
173 int ab
= ez
->AND(a
, b
), cd
= ez
->AND(c
, d
);
174 int undef_ab
= ez
->AND(ez
->OR(undef_a
, undef_b
), ez
->NOT(ez
->OR(a0
, b0
)));
175 int undef_cd
= ez
->AND(ez
->OR(undef_c
, undef_d
), ez
->NOT(ez
->OR(c0
, d0
)));
177 int ab1
= ez
->AND(ab
, ez
->NOT(undef_ab
));
178 int cd1
= ez
->AND(cd
, ez
->NOT(undef_cd
));
179 int yX
= ez
->AND(ez
->OR(undef_ab
, undef_cd
), ez
->NOT(ez
->OR(ab1
, cd1
)));
181 ez
->assume(ez
->IFF(yX
, undef_y
));
185 int a1
= ez
->AND(a
, ez
->NOT(undef_a
));
186 int b1
= ez
->AND(b
, ez
->NOT(undef_b
));
187 int c1
= ez
->AND(c
, ez
->NOT(undef_c
));
188 int d1
= ez
->AND(d
, ez
->NOT(undef_d
));
190 int ab
= ez
->OR(a
, b
), cd
= ez
->OR(c
, d
);
191 int undef_ab
= ez
->AND(ez
->OR(undef_a
, undef_b
), ez
->NOT(ez
->OR(a1
, b1
)));
192 int undef_cd
= ez
->AND(ez
->OR(undef_c
, undef_d
), ez
->NOT(ez
->OR(c1
, d1
)));
194 int ab0
= ez
->AND(ez
->NOT(ab
), ez
->NOT(undef_ab
));
195 int cd0
= ez
->AND(ez
->NOT(cd
), ez
->NOT(undef_cd
));
196 int yX
= ez
->AND(ez
->OR(undef_ab
, undef_cd
), ez
->NOT(ez
->OR(ab0
, cd0
)));
198 ez
->assume(ez
->IFF(yX
, undef_y
));
201 undefGating(y
, yy
, undef_y
);
207 if (cell
->type
.in(ID($_NOT_
), ID($
not)))
209 std::vector
<int> a
= importDefSigSpec(cell
->getPort(ID::A
), timestep
);
210 std::vector
<int> y
= importDefSigSpec(cell
->getPort(ID::Y
), timestep
);
211 extendSignalWidthUnary(a
, y
, cell
);
213 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
214 ez
->assume(ez
->vec_eq(ez
->vec_not(a
), yy
));
217 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort(ID::A
), timestep
);
218 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort(ID::Y
), timestep
);
219 extendSignalWidthUnary(undef_a
, undef_y
, cell
, false);
220 ez
->assume(ez
->vec_eq(undef_a
, undef_y
));
221 undefGating(y
, yy
, undef_y
);
226 if (cell
->type
.in(ID($_MUX_
), ID($mux
), ID($_NMUX_
)))
228 std::vector
<int> a
= importDefSigSpec(cell
->getPort(ID::A
), timestep
);
229 std::vector
<int> b
= importDefSigSpec(cell
->getPort(ID::B
), timestep
);
230 std::vector
<int> s
= importDefSigSpec(cell
->getPort(ID::S
), timestep
);
231 std::vector
<int> y
= importDefSigSpec(cell
->getPort(ID::Y
), timestep
);
233 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
234 if (cell
->type
== ID($_NMUX_
))
235 ez
->assume(ez
->vec_eq(ez
->vec_not(ez
->vec_ite(s
.at(0), b
, a
)), yy
));
237 ez
->assume(ez
->vec_eq(ez
->vec_ite(s
.at(0), b
, a
), yy
));
241 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort(ID::A
), timestep
);
242 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort(ID::B
), timestep
);
243 std::vector
<int> undef_s
= importUndefSigSpec(cell
->getPort(ID::S
), timestep
);
244 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort(ID::Y
), timestep
);
246 std::vector
<int> unequal_ab
= ez
->vec_not(ez
->vec_iff(a
, b
));
247 std::vector
<int> undef_ab
= ez
->vec_or(unequal_ab
, ez
->vec_or(undef_a
, undef_b
));
248 std::vector
<int> yX
= ez
->vec_ite(undef_s
.at(0), undef_ab
, ez
->vec_ite(s
.at(0), undef_b
, undef_a
));
249 ez
->assume(ez
->vec_eq(yX
, undef_y
));
250 undefGating(y
, yy
, undef_y
);
255 if (cell
->type
== ID($pmux
))
257 std::vector
<int> a
= importDefSigSpec(cell
->getPort(ID::A
), timestep
);
258 std::vector
<int> b
= importDefSigSpec(cell
->getPort(ID::B
), timestep
);
259 std::vector
<int> s
= importDefSigSpec(cell
->getPort(ID::S
), timestep
);
260 std::vector
<int> y
= importDefSigSpec(cell
->getPort(ID::Y
), timestep
);
262 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
264 std::vector
<int> tmp
= a
;
265 for (size_t i
= 0; i
< s
.size(); i
++) {
266 std::vector
<int> part_of_b(b
.begin()+i
*a
.size(), b
.begin()+(i
+1)*a
.size());
267 tmp
= ez
->vec_ite(s
.at(i
), part_of_b
, tmp
);
269 ez
->assume(ez
->vec_eq(tmp
, yy
));
273 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort(ID::A
), timestep
);
274 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort(ID::B
), timestep
);
275 std::vector
<int> undef_s
= importUndefSigSpec(cell
->getPort(ID::S
), timestep
);
276 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort(ID::Y
), timestep
);
278 int maybe_a
= ez
->CONST_TRUE
;
280 std::vector
<int> bits_set
= std::vector
<int>(undef_y
.size(), ez
->CONST_FALSE
);
281 std::vector
<int> bits_clr
= std::vector
<int>(undef_y
.size(), ez
->CONST_FALSE
);
283 for (size_t i
= 0; i
< s
.size(); i
++)
285 std::vector
<int> part_of_b(b
.begin()+i
*a
.size(), b
.begin()+(i
+1)*a
.size());
286 std::vector
<int> part_of_undef_b(undef_b
.begin()+i
*a
.size(), undef_b
.begin()+(i
+1)*a
.size());
288 int maybe_s
= ez
->OR(s
.at(i
), undef_s
.at(i
));
289 int sure_s
= ez
->AND(s
.at(i
), ez
->NOT(undef_s
.at(i
)));
291 maybe_a
= ez
->AND(maybe_a
, ez
->NOT(sure_s
));
293 bits_set
= ez
->vec_ite(maybe_s
, ez
->vec_or(bits_set
, ez
->vec_or(part_of_b
, part_of_undef_b
)), bits_set
);
294 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
);
297 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
);
298 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
);
300 ez
->assume(ez
->vec_eq(ez
->vec_not(ez
->vec_xor(bits_set
, bits_clr
)), undef_y
));
301 undefGating(y
, yy
, undef_y
);
306 if (cell
->type
.in(ID($pos
), ID($neg
)))
308 std::vector
<int> a
= importDefSigSpec(cell
->getPort(ID::A
), timestep
);
309 std::vector
<int> y
= importDefSigSpec(cell
->getPort(ID::Y
), timestep
);
310 extendSignalWidthUnary(a
, y
, cell
);
312 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
314 if (cell
->type
== ID($pos
)) {
315 ez
->assume(ez
->vec_eq(a
, yy
));
317 std::vector
<int> zero(a
.size(), ez
->CONST_FALSE
);
318 ez
->assume(ez
->vec_eq(ez
->vec_sub(zero
, a
), yy
));
323 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort(ID::A
), timestep
);
324 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort(ID::Y
), timestep
);
325 extendSignalWidthUnary(undef_a
, undef_y
, cell
);
327 if (cell
->type
== ID($pos
)) {
328 ez
->assume(ez
->vec_eq(undef_a
, undef_y
));
330 int undef_any_a
= ez
->expression(ezSAT::OpOr
, undef_a
);
331 std::vector
<int> undef_y_bits(undef_y
.size(), undef_any_a
);
332 ez
->assume(ez
->vec_eq(undef_y_bits
, undef_y
));
335 undefGating(y
, yy
, undef_y
);
340 if (cell
->type
.in(ID($reduce_and
), ID($reduce_or
), ID($reduce_xor
), ID($reduce_xnor
), ID($reduce_bool
), ID($logic_not
)))
342 std::vector
<int> a
= importDefSigSpec(cell
->getPort(ID::A
), timestep
);
343 std::vector
<int> y
= importDefSigSpec(cell
->getPort(ID::Y
), timestep
);
345 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
347 if (cell
->type
== ID($reduce_and
))
348 ez
->SET(ez
->expression(ez
->OpAnd
, a
), yy
.at(0));
349 if (cell
->type
.in(ID($reduce_or
), ID($reduce_bool
)))
350 ez
->SET(ez
->expression(ez
->OpOr
, a
), yy
.at(0));
351 if (cell
->type
== ID($reduce_xor
))
352 ez
->SET(ez
->expression(ez
->OpXor
, a
), yy
.at(0));
353 if (cell
->type
== ID($reduce_xnor
))
354 ez
->SET(ez
->NOT(ez
->expression(ez
->OpXor
, a
)), yy
.at(0));
355 if (cell
->type
== ID($logic_not
))
356 ez
->SET(ez
->NOT(ez
->expression(ez
->OpOr
, a
)), yy
.at(0));
357 for (size_t i
= 1; i
< y
.size(); i
++)
358 ez
->SET(ez
->CONST_FALSE
, yy
.at(i
));
362 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort(ID::A
), timestep
);
363 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort(ID::Y
), timestep
);
364 int aX
= ez
->expression(ezSAT::OpOr
, undef_a
);
366 if (cell
->type
== ID($reduce_and
)) {
367 int a0
= ez
->expression(ezSAT::OpOr
, ez
->vec_and(ez
->vec_not(a
), ez
->vec_not(undef_a
)));
368 ez
->assume(ez
->IFF(ez
->AND(ez
->NOT(a0
), aX
), undef_y
.at(0)));
370 else if (cell
->type
.in(ID($reduce_or
), ID($reduce_bool
), ID($logic_not
))) {
371 int a1
= ez
->expression(ezSAT::OpOr
, ez
->vec_and(a
, ez
->vec_not(undef_a
)));
372 ez
->assume(ez
->IFF(ez
->AND(ez
->NOT(a1
), aX
), undef_y
.at(0)));
374 else if (cell
->type
.in(ID($reduce_xor
), ID($reduce_xnor
))) {
375 ez
->assume(ez
->IFF(aX
, undef_y
.at(0)));
379 for (size_t i
= 1; i
< undef_y
.size(); i
++)
380 ez
->SET(ez
->CONST_FALSE
, undef_y
.at(i
));
382 undefGating(y
, yy
, undef_y
);
387 if (cell
->type
.in(ID($logic_and
), ID($logic_or
)))
389 std::vector
<int> vec_a
= importDefSigSpec(cell
->getPort(ID::A
), timestep
);
390 std::vector
<int> vec_b
= importDefSigSpec(cell
->getPort(ID::B
), timestep
);
392 int a
= ez
->expression(ez
->OpOr
, vec_a
);
393 int b
= ez
->expression(ez
->OpOr
, vec_b
);
394 std::vector
<int> y
= importDefSigSpec(cell
->getPort(ID::Y
), timestep
);
396 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
398 if (cell
->type
== ID($logic_and
))
399 ez
->SET(ez
->expression(ez
->OpAnd
, a
, b
), yy
.at(0));
401 ez
->SET(ez
->expression(ez
->OpOr
, a
, b
), yy
.at(0));
402 for (size_t i
= 1; i
< y
.size(); i
++)
403 ez
->SET(ez
->CONST_FALSE
, yy
.at(i
));
407 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort(ID::A
), timestep
);
408 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort(ID::B
), timestep
);
409 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort(ID::Y
), timestep
);
411 int a0
= ez
->NOT(ez
->OR(ez
->expression(ezSAT::OpOr
, vec_a
), ez
->expression(ezSAT::OpOr
, undef_a
)));
412 int b0
= ez
->NOT(ez
->OR(ez
->expression(ezSAT::OpOr
, vec_b
), ez
->expression(ezSAT::OpOr
, undef_b
)));
413 int a1
= ez
->expression(ezSAT::OpOr
, ez
->vec_and(vec_a
, ez
->vec_not(undef_a
)));
414 int b1
= ez
->expression(ezSAT::OpOr
, ez
->vec_and(vec_b
, ez
->vec_not(undef_b
)));
415 int aX
= ez
->expression(ezSAT::OpOr
, undef_a
);
416 int bX
= ez
->expression(ezSAT::OpOr
, undef_b
);
418 if (cell
->type
== ID($logic_and
))
419 ez
->SET(ez
->AND(ez
->OR(aX
, bX
), ez
->NOT(ez
->AND(a1
, b1
)), ez
->NOT(a0
), ez
->NOT(b0
)), undef_y
.at(0));
420 else if (cell
->type
== ID($logic_or
))
421 ez
->SET(ez
->AND(ez
->OR(aX
, bX
), ez
->NOT(ez
->AND(a0
, b0
)), ez
->NOT(a1
), ez
->NOT(b1
)), undef_y
.at(0));
425 for (size_t i
= 1; i
< undef_y
.size(); i
++)
426 ez
->SET(ez
->CONST_FALSE
, undef_y
.at(i
));
428 undefGating(y
, yy
, undef_y
);
433 if (cell
->type
.in(ID($lt
), ID($le
), ID($eq
), ID($ne
), ID($eqx
), ID($nex
), ID($ge
), ID($gt
)))
435 bool is_signed
= cell
->parameters
[ID::A_SIGNED
].as_bool() && cell
->parameters
[ID::B_SIGNED
].as_bool();
436 std::vector
<int> a
= importDefSigSpec(cell
->getPort(ID::A
), timestep
);
437 std::vector
<int> b
= importDefSigSpec(cell
->getPort(ID::B
), timestep
);
438 std::vector
<int> y
= importDefSigSpec(cell
->getPort(ID::Y
), timestep
);
439 extendSignalWidth(a
, b
, cell
);
441 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
443 if (model_undef
&& cell
->type
.in(ID($eqx
), ID($nex
))) {
444 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort(ID::A
), timestep
);
445 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort(ID::B
), timestep
);
446 extendSignalWidth(undef_a
, undef_b
, cell
, true);
447 a
= ez
->vec_or(a
, undef_a
);
448 b
= ez
->vec_or(b
, undef_b
);
451 if (cell
->type
== ID($lt
))
452 ez
->SET(is_signed
? ez
->vec_lt_signed(a
, b
) : ez
->vec_lt_unsigned(a
, b
), yy
.at(0));
453 if (cell
->type
== ID($le
))
454 ez
->SET(is_signed
? ez
->vec_le_signed(a
, b
) : ez
->vec_le_unsigned(a
, b
), yy
.at(0));
455 if (cell
->type
.in(ID($eq
), ID($eqx
)))
456 ez
->SET(ez
->vec_eq(a
, b
), yy
.at(0));
457 if (cell
->type
.in(ID($ne
), ID($nex
)))
458 ez
->SET(ez
->vec_ne(a
, b
), yy
.at(0));
459 if (cell
->type
== ID($ge
))
460 ez
->SET(is_signed
? ez
->vec_ge_signed(a
, b
) : ez
->vec_ge_unsigned(a
, b
), yy
.at(0));
461 if (cell
->type
== ID($gt
))
462 ez
->SET(is_signed
? ez
->vec_gt_signed(a
, b
) : ez
->vec_gt_unsigned(a
, b
), yy
.at(0));
463 for (size_t i
= 1; i
< y
.size(); i
++)
464 ez
->SET(ez
->CONST_FALSE
, yy
.at(i
));
466 if (model_undef
&& cell
->type
.in(ID($eqx
), ID($nex
)))
468 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort(ID::A
), timestep
);
469 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort(ID::B
), timestep
);
470 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort(ID::Y
), timestep
);
471 extendSignalWidth(undef_a
, undef_b
, cell
, true);
473 if (cell
->type
== ID($eqx
))
474 yy
.at(0) = ez
->AND(yy
.at(0), ez
->vec_eq(undef_a
, undef_b
));
476 yy
.at(0) = ez
->OR(yy
.at(0), ez
->vec_ne(undef_a
, undef_b
));
478 for (size_t i
= 0; i
< y
.size(); i
++)
479 ez
->SET(ez
->CONST_FALSE
, undef_y
.at(i
));
481 ez
->assume(ez
->vec_eq(y
, yy
));
483 else if (model_undef
&& cell
->type
.in(ID($eq
), ID($ne
)))
485 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort(ID::A
), timestep
);
486 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort(ID::B
), timestep
);
487 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort(ID::Y
), timestep
);
488 extendSignalWidth(undef_a
, undef_b
, cell
, true);
490 int undef_any_a
= ez
->expression(ezSAT::OpOr
, undef_a
);
491 int undef_any_b
= ez
->expression(ezSAT::OpOr
, undef_b
);
492 int undef_any
= ez
->OR(undef_any_a
, undef_any_b
);
494 std::vector
<int> masked_a_bits
= ez
->vec_or(a
, ez
->vec_or(undef_a
, undef_b
));
495 std::vector
<int> masked_b_bits
= ez
->vec_or(b
, ez
->vec_or(undef_a
, undef_b
));
497 int masked_ne
= ez
->vec_ne(masked_a_bits
, masked_b_bits
);
498 int undef_y_bit
= ez
->AND(undef_any
, ez
->NOT(masked_ne
));
500 for (size_t i
= 1; i
< undef_y
.size(); i
++)
501 ez
->SET(ez
->CONST_FALSE
, undef_y
.at(i
));
502 ez
->SET(undef_y_bit
, undef_y
.at(0));
504 undefGating(y
, yy
, undef_y
);
509 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort(ID::Y
), timestep
);
510 undefGating(y
, yy
, undef_y
);
512 log_assert(!model_undef
|| arith_undef_handled
);
517 if (cell
->type
.in(ID($shl
), ID($shr
), ID($sshl
), ID($sshr
), ID($shift
), ID($shiftx
)))
519 std::vector
<int> a
= importDefSigSpec(cell
->getPort(ID::A
), timestep
);
520 std::vector
<int> b
= importDefSigSpec(cell
->getPort(ID::B
), timestep
);
521 std::vector
<int> y
= importDefSigSpec(cell
->getPort(ID::Y
), timestep
);
523 int extend_bit
= ez
->CONST_FALSE
;
525 if (cell
->parameters
[ID::A_SIGNED
].as_bool())
526 extend_bit
= a
.back();
528 while (y
.size() < a
.size())
529 y
.push_back(ez
->literal());
530 while (y
.size() > a
.size())
531 a
.push_back(extend_bit
);
533 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
534 std::vector
<int> shifted_a
;
536 if (cell
->type
.in( ID($shl
), ID($sshl
)))
537 shifted_a
= ez
->vec_shift_left(a
, b
, false, ez
->CONST_FALSE
, ez
->CONST_FALSE
);
539 if (cell
->type
== ID($shr
))
540 shifted_a
= ez
->vec_shift_right(a
, b
, false, ez
->CONST_FALSE
, ez
->CONST_FALSE
);
542 if (cell
->type
== ID($sshr
))
543 shifted_a
= ez
->vec_shift_right(a
, b
, false, cell
->parameters
[ID::A_SIGNED
].as_bool() ? a
.back() : ez
->CONST_FALSE
, ez
->CONST_FALSE
);
545 if (cell
->type
.in(ID($shift
), ID($shiftx
)))
546 shifted_a
= ez
->vec_shift_right(a
, b
, cell
->parameters
[ID::B_SIGNED
].as_bool(), ez
->CONST_FALSE
, ez
->CONST_FALSE
);
548 ez
->assume(ez
->vec_eq(shifted_a
, yy
));
552 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort(ID::A
), timestep
);
553 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort(ID::B
), timestep
);
554 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort(ID::Y
), timestep
);
555 std::vector
<int> undef_a_shifted
;
557 extend_bit
= cell
->type
== ID($shiftx
) ? ez
->CONST_TRUE
: ez
->CONST_FALSE
;
558 if (cell
->parameters
[ID::A_SIGNED
].as_bool())
559 extend_bit
= undef_a
.back();
561 while (undef_y
.size() < undef_a
.size())
562 undef_y
.push_back(ez
->literal());
563 while (undef_y
.size() > undef_a
.size())
564 undef_a
.push_back(extend_bit
);
566 if (cell
->type
.in(ID($shl
), ID($sshl
)))
567 undef_a_shifted
= ez
->vec_shift_left(undef_a
, b
, false, ez
->CONST_FALSE
, ez
->CONST_FALSE
);
569 if (cell
->type
== ID($shr
))
570 undef_a_shifted
= ez
->vec_shift_right(undef_a
, b
, false, ez
->CONST_FALSE
, ez
->CONST_FALSE
);
572 if (cell
->type
== ID($sshr
))
573 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
);
575 if (cell
->type
== ID($shift
))
576 undef_a_shifted
= ez
->vec_shift_right(undef_a
, b
, cell
->parameters
[ID::B_SIGNED
].as_bool(), ez
->CONST_FALSE
, ez
->CONST_FALSE
);
578 if (cell
->type
== ID($shiftx
))
579 undef_a_shifted
= ez
->vec_shift_right(undef_a
, b
, cell
->parameters
[ID::B_SIGNED
].as_bool(), ez
->CONST_TRUE
, ez
->CONST_TRUE
);
581 int undef_any_b
= ez
->expression(ezSAT::OpOr
, undef_b
);
582 std::vector
<int> undef_all_y_bits(undef_y
.size(), undef_any_b
);
583 ez
->assume(ez
->vec_eq(ez
->vec_or(undef_a_shifted
, undef_all_y_bits
), undef_y
));
584 undefGating(y
, yy
, undef_y
);
589 if (cell
->type
== ID($mul
))
591 std::vector
<int> a
= importDefSigSpec(cell
->getPort(ID::A
), timestep
);
592 std::vector
<int> b
= importDefSigSpec(cell
->getPort(ID::B
), timestep
);
593 std::vector
<int> y
= importDefSigSpec(cell
->getPort(ID::Y
), timestep
);
594 extendSignalWidth(a
, b
, y
, cell
);
596 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
598 std::vector
<int> tmp(a
.size(), ez
->CONST_FALSE
);
599 for (int i
= 0; i
< int(a
.size()); i
++)
601 std::vector
<int> shifted_a(a
.size(), ez
->CONST_FALSE
);
602 for (int j
= i
; j
< int(a
.size()); j
++)
603 shifted_a
.at(j
) = a
.at(j
-i
);
604 tmp
= ez
->vec_ite(b
.at(i
), ez
->vec_add(tmp
, shifted_a
), tmp
);
606 ez
->assume(ez
->vec_eq(tmp
, yy
));
609 log_assert(arith_undef_handled
);
610 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort(ID::Y
), timestep
);
611 undefGating(y
, yy
, undef_y
);
616 if (cell
->type
== ID($macc
))
618 std::vector
<int> a
= importDefSigSpec(cell
->getPort(ID::A
), timestep
);
619 std::vector
<int> b
= importDefSigSpec(cell
->getPort(ID::B
), timestep
);
620 std::vector
<int> y
= importDefSigSpec(cell
->getPort(ID::Y
), timestep
);
623 macc
.from_cell(cell
);
625 std::vector
<int> tmp(GetSize(y
), ez
->CONST_FALSE
);
627 for (auto &port
: macc
.ports
)
629 std::vector
<int> in_a
= importDefSigSpec(port
.in_a
, timestep
);
630 std::vector
<int> in_b
= importDefSigSpec(port
.in_b
, timestep
);
632 while (GetSize(in_a
) < GetSize(y
))
633 in_a
.push_back(port
.is_signed
&& !in_a
.empty() ? in_a
.back() : ez
->CONST_FALSE
);
634 in_a
.resize(GetSize(y
));
638 while (GetSize(in_b
) < GetSize(y
))
639 in_b
.push_back(port
.is_signed
&& !in_b
.empty() ? in_b
.back() : ez
->CONST_FALSE
);
640 in_b
.resize(GetSize(y
));
642 for (int i
= 0; i
< GetSize(in_b
); i
++) {
643 std::vector
<int> shifted_a(in_a
.size(), ez
->CONST_FALSE
);
644 for (int j
= i
; j
< int(in_a
.size()); j
++)
645 shifted_a
.at(j
) = in_a
.at(j
-i
);
646 if (port
.do_subtract
)
647 tmp
= ez
->vec_ite(in_b
.at(i
), ez
->vec_sub(tmp
, shifted_a
), tmp
);
649 tmp
= ez
->vec_ite(in_b
.at(i
), ez
->vec_add(tmp
, shifted_a
), tmp
);
654 if (port
.do_subtract
)
655 tmp
= ez
->vec_sub(tmp
, in_a
);
657 tmp
= ez
->vec_add(tmp
, in_a
);
661 for (int i
= 0; i
< GetSize(b
); i
++) {
662 std::vector
<int> val(GetSize(y
), ez
->CONST_FALSE
);
664 tmp
= ez
->vec_add(tmp
, val
);
669 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort(ID::A
), timestep
);
670 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort(ID::B
), timestep
);
672 int undef_any_a
= ez
->expression(ezSAT::OpOr
, undef_a
);
673 int undef_any_b
= ez
->expression(ezSAT::OpOr
, undef_b
);
675 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort(ID::Y
), timestep
);
676 ez
->assume(ez
->vec_eq(undef_y
, std::vector
<int>(GetSize(y
), ez
->OR(undef_any_a
, undef_any_b
))));
678 undefGating(y
, tmp
, undef_y
);
681 ez
->assume(ez
->vec_eq(y
, tmp
));
686 if (cell
->type
.in(ID($div
), ID($mod
), ID($divfloor
), ID($modfloor
)))
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
, y
, cell
);
693 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
695 std::vector
<int> a_u
, b_u
;
696 if (cell
->parameters
[ID::A_SIGNED
].as_bool() && cell
->parameters
[ID::B_SIGNED
].as_bool()) {
697 a_u
= ez
->vec_ite(a
.back(), ez
->vec_neg(a
), a
);
698 b_u
= ez
->vec_ite(b
.back(), ez
->vec_neg(b
), b
);
704 std::vector
<int> chain_buf
= a_u
;
705 std::vector
<int> y_u(a_u
.size(), ez
->CONST_FALSE
);
706 for (int i
= int(a
.size())-1; i
>= 0; i
--)
708 chain_buf
.insert(chain_buf
.end(), chain_buf
.size(), ez
->CONST_FALSE
);
710 std::vector
<int> b_shl(i
, ez
->CONST_FALSE
);
711 b_shl
.insert(b_shl
.end(), b_u
.begin(), b_u
.end());
712 b_shl
.insert(b_shl
.end(), chain_buf
.size()-b_shl
.size(), ez
->CONST_FALSE
);
714 y_u
.at(i
) = ez
->vec_ge_unsigned(chain_buf
, b_shl
);
715 chain_buf
= ez
->vec_ite(y_u
.at(i
), ez
->vec_sub(chain_buf
, b_shl
), chain_buf
);
717 chain_buf
.erase(chain_buf
.begin() + a_u
.size(), chain_buf
.end());
720 std::vector
<int> y_tmp
= ignore_div_by_zero
? yy
: ez
->vec_var(y
.size());
722 // modulo calculation
723 std::vector
<int> modulo_trunc
;
724 int floored_eq_trunc
;
725 if (cell
->parameters
[ID::A_SIGNED
].as_bool() && cell
->parameters
[ID::B_SIGNED
].as_bool()) {
726 modulo_trunc
= ez
->vec_ite(a
.back(), ez
->vec_neg(chain_buf
), chain_buf
);
727 // floor == trunc when sgn(a) == sgn(b) or trunc == 0
728 floored_eq_trunc
= ez
->OR(ez
->IFF(a
.back(), b
.back()), ez
->NOT(ez
->expression(ezSAT::OpOr
, modulo_trunc
)));
730 modulo_trunc
= chain_buf
;
731 floored_eq_trunc
= ez
->CONST_TRUE
;
734 if (cell
->type
== ID($div
)) {
735 if (cell
->parameters
[ID::A_SIGNED
].as_bool() && cell
->parameters
[ID::B_SIGNED
].as_bool())
736 ez
->assume(ez
->vec_eq(y_tmp
, ez
->vec_ite(ez
->XOR(a
.back(), b
.back()), ez
->vec_neg(y_u
), y_u
)));
738 ez
->assume(ez
->vec_eq(y_tmp
, y_u
));
739 } else if (cell
->type
== ID($mod
)) {
740 ez
->assume(ez
->vec_eq(y_tmp
, modulo_trunc
));
741 } else if (cell
->type
== ID($divfloor
)) {
742 if (cell
->parameters
[ID::A_SIGNED
].as_bool() && cell
->parameters
[ID::B_SIGNED
].as_bool())
743 ez
->assume(ez
->vec_eq(y_tmp
, ez
->vec_ite(
744 ez
->XOR(a
.back(), b
.back()),
745 ez
->vec_neg(ez
->vec_ite(
746 ez
->vec_reduce_or(modulo_trunc
),
747 ez
->vec_add(y_u
, ez
->vec_const_unsigned(1, y_u
.size())),
753 ez
->assume(ez
->vec_eq(y_tmp
, y_u
));
754 } else if (cell
->type
== ID($modfloor
)) {
755 ez
->assume(ez
->vec_eq(y_tmp
, ez
->vec_ite(floored_eq_trunc
, modulo_trunc
, ez
->vec_add(modulo_trunc
, b
))));
758 if (ignore_div_by_zero
) {
759 ez
->assume(ez
->expression(ezSAT::OpOr
, b
));
761 std::vector
<int> div_zero_result
;
762 if (cell
->type
.in(ID($div
), ID($divfloor
))) {
763 if (cell
->parameters
[ID::A_SIGNED
].as_bool() && cell
->parameters
[ID::B_SIGNED
].as_bool()) {
764 std::vector
<int> all_ones(y
.size(), ez
->CONST_TRUE
);
765 std::vector
<int> only_first_one(y
.size(), ez
->CONST_FALSE
);
766 only_first_one
.at(0) = ez
->CONST_TRUE
;
767 div_zero_result
= ez
->vec_ite(a
.back(), only_first_one
, all_ones
);
769 div_zero_result
.insert(div_zero_result
.end(), cell
->getPort(ID::A
).size(), ez
->CONST_TRUE
);
770 div_zero_result
.insert(div_zero_result
.end(), y
.size() - div_zero_result
.size(), ez
->CONST_FALSE
);
772 } else if (cell
->type
.in(ID($mod
), ID($modfloor
))) {
774 int copy_a_bits
= min(cell
->getPort(ID::A
).size(), cell
->getPort(ID::B
).size());
775 div_zero_result
.insert(div_zero_result
.end(), a
.begin(), a
.begin() + copy_a_bits
);
776 if (cell
->parameters
[ID::A_SIGNED
].as_bool() && cell
->parameters
[ID::B_SIGNED
].as_bool())
777 div_zero_result
.insert(div_zero_result
.end(), y
.size() - div_zero_result
.size(), div_zero_result
.back());
779 div_zero_result
.insert(div_zero_result
.end(), y
.size() - div_zero_result
.size(), ez
->CONST_FALSE
);
781 ez
->assume(ez
->vec_eq(yy
, ez
->vec_ite(ez
->expression(ezSAT::OpOr
, b
), y_tmp
, div_zero_result
)));
785 log_assert(arith_undef_handled
);
786 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort(ID::Y
), timestep
);
787 undefGating(y
, yy
, undef_y
);
792 if (cell
->type
== ID($lut
))
794 std::vector
<int> a
= importDefSigSpec(cell
->getPort(ID::A
), timestep
);
795 std::vector
<int> y
= importDefSigSpec(cell
->getPort(ID::Y
), timestep
);
797 std::vector
<int> lut
;
798 for (auto bit
: cell
->getParam(ID::LUT
).bits
)
799 lut
.push_back(bit
== State::S1
? ez
->CONST_TRUE
: ez
->CONST_FALSE
);
800 while (GetSize(lut
) < (1 << GetSize(a
)))
801 lut
.push_back(ez
->CONST_FALSE
);
802 lut
.resize(1 << GetSize(a
));
806 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort(ID::A
), timestep
);
807 std::vector
<int> t(lut
), u(GetSize(t
), ez
->CONST_FALSE
);
809 for (int i
= GetSize(a
)-1; i
>= 0; i
--)
811 std::vector
<int> t0(t
.begin(), t
.begin() + GetSize(t
)/2);
812 std::vector
<int> t1(t
.begin() + GetSize(t
)/2, t
.end());
814 std::vector
<int> u0(u
.begin(), u
.begin() + GetSize(u
)/2);
815 std::vector
<int> u1(u
.begin() + GetSize(u
)/2, u
.end());
817 t
= ez
->vec_ite(a
[i
], t1
, t0
);
818 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
));
821 log_assert(GetSize(t
) == 1);
822 log_assert(GetSize(u
) == 1);
823 undefGating(y
, t
, u
);
824 ez
->assume(ez
->vec_eq(importUndefSigSpec(cell
->getPort(ID::Y
), timestep
), u
));
828 std::vector
<int> t
= lut
;
829 for (int i
= GetSize(a
)-1; i
>= 0; i
--)
831 std::vector
<int> t0(t
.begin(), t
.begin() + GetSize(t
)/2);
832 std::vector
<int> t1(t
.begin() + GetSize(t
)/2, t
.end());
833 t
= ez
->vec_ite(a
[i
], t1
, t0
);
836 log_assert(GetSize(t
) == 1);
837 ez
->assume(ez
->vec_eq(y
, t
));
842 if (cell
->type
== ID($sop
))
844 std::vector
<int> a
= importDefSigSpec(cell
->getPort(ID::A
), timestep
);
845 int y
= importDefSigSpec(cell
->getPort(ID::Y
), timestep
).at(0);
847 int width
= cell
->getParam(ID::WIDTH
).as_int();
848 int depth
= cell
->getParam(ID::DEPTH
).as_int();
850 vector
<State
> table_raw
= cell
->getParam(ID::TABLE
).bits
;
851 while (GetSize(table_raw
) < 2*width
*depth
)
852 table_raw
.push_back(State::S0
);
854 vector
<vector
<int>> table(depth
);
856 for (int i
= 0; i
< depth
; i
++)
857 for (int j
= 0; j
< width
; j
++)
859 bool pat0
= (table_raw
[2*width
*i
+ 2*j
+ 0] == State::S1
);
860 bool pat1
= (table_raw
[2*width
*i
+ 2*j
+ 1] == State::S1
);
863 table
.at(i
).push_back(0);
864 else if (!pat0
&& pat1
)
865 table
.at(i
).push_back(1);
867 table
.at(i
).push_back(-1);
872 std::vector
<int> products
, undef_products
;
873 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort(ID::A
), timestep
);
874 int undef_y
= importUndefSigSpec(cell
->getPort(ID::Y
), timestep
).at(0);
876 for (int i
= 0; i
< depth
; i
++)
878 std::vector
<int> cmp_a
, cmp_ua
, cmp_b
;
880 for (int j
= 0; j
< width
; j
++)
881 if (table
.at(i
).at(j
) >= 0) {
882 cmp_a
.push_back(a
.at(j
));
883 cmp_ua
.push_back(undef_a
.at(j
));
884 cmp_b
.push_back(table
.at(i
).at(j
) ? ez
->CONST_TRUE
: ez
->CONST_FALSE
);
887 std::vector
<int> masked_a
= ez
->vec_or(cmp_a
, cmp_ua
);
888 std::vector
<int> masked_b
= ez
->vec_or(cmp_b
, cmp_ua
);
890 int masked_eq
= ez
->vec_eq(masked_a
, masked_b
);
891 int any_undef
= ez
->expression(ezSAT::OpOr
, cmp_ua
);
893 undef_products
.push_back(ez
->AND(any_undef
, masked_eq
));
894 products
.push_back(ez
->AND(ez
->NOT(any_undef
), masked_eq
));
897 int yy
= ez
->expression(ezSAT::OpOr
, products
);
898 ez
->SET(undef_y
, ez
->AND(ez
->NOT(yy
), ez
->expression(ezSAT::OpOr
, undef_products
)));
899 undefGating(y
, yy
, undef_y
);
903 std::vector
<int> products
;
905 for (int i
= 0; i
< depth
; i
++)
907 std::vector
<int> cmp_a
, cmp_b
;
909 for (int j
= 0; j
< width
; j
++)
910 if (table
.at(i
).at(j
) >= 0) {
911 cmp_a
.push_back(a
.at(j
));
912 cmp_b
.push_back(table
.at(i
).at(j
) ? ez
->CONST_TRUE
: ez
->CONST_FALSE
);
915 products
.push_back(ez
->vec_eq(cmp_a
, cmp_b
));
918 ez
->SET(y
, ez
->expression(ezSAT::OpOr
, products
));
924 if (cell
->type
== ID($fa
))
926 std::vector
<int> a
= importDefSigSpec(cell
->getPort(ID::A
), timestep
);
927 std::vector
<int> b
= importDefSigSpec(cell
->getPort(ID::B
), timestep
);
928 std::vector
<int> c
= importDefSigSpec(cell
->getPort(ID::C
), timestep
);
929 std::vector
<int> y
= importDefSigSpec(cell
->getPort(ID::Y
), timestep
);
930 std::vector
<int> x
= importDefSigSpec(cell
->getPort(ID::X
), timestep
);
932 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
933 std::vector
<int> xx
= model_undef
? ez
->vec_var(x
.size()) : x
;
935 std::vector
<int> t1
= ez
->vec_xor(a
, b
);
936 ez
->assume(ez
->vec_eq(yy
, ez
->vec_xor(t1
, c
)));
938 std::vector
<int> t2
= ez
->vec_and(a
, b
);
939 std::vector
<int> t3
= ez
->vec_and(c
, t1
);
940 ez
->assume(ez
->vec_eq(xx
, ez
->vec_or(t2
, t3
)));
944 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort(ID::A
), timestep
);
945 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort(ID::B
), timestep
);
946 std::vector
<int> undef_c
= importUndefSigSpec(cell
->getPort(ID::C
), timestep
);
948 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort(ID::Y
), timestep
);
949 std::vector
<int> undef_x
= importUndefSigSpec(cell
->getPort(ID::X
), timestep
);
951 ez
->assume(ez
->vec_eq(undef_y
, ez
->vec_or(ez
->vec_or(undef_a
, undef_b
), undef_c
)));
952 ez
->assume(ez
->vec_eq(undef_x
, undef_y
));
954 undefGating(y
, yy
, undef_y
);
955 undefGating(x
, xx
, undef_x
);
960 if (cell
->type
== ID($lcu
))
962 std::vector
<int> p
= importDefSigSpec(cell
->getPort(ID::P
), timestep
);
963 std::vector
<int> g
= importDefSigSpec(cell
->getPort(ID::G
), timestep
);
964 std::vector
<int> ci
= importDefSigSpec(cell
->getPort(ID::CI
), timestep
);
965 std::vector
<int> co
= importDefSigSpec(cell
->getPort(ID::CO
), timestep
);
967 std::vector
<int> yy
= model_undef
? ez
->vec_var(co
.size()) : co
;
969 for (int i
= 0; i
< GetSize(co
); i
++)
970 ez
->SET(yy
[i
], ez
->OR(g
[i
], ez
->AND(p
[i
], i
? yy
[i
-1] : ci
[0])));
974 std::vector
<int> undef_p
= importUndefSigSpec(cell
->getPort(ID::P
), timestep
);
975 std::vector
<int> undef_g
= importUndefSigSpec(cell
->getPort(ID::G
), timestep
);
976 std::vector
<int> undef_ci
= importUndefSigSpec(cell
->getPort(ID::CI
), timestep
);
977 std::vector
<int> undef_co
= importUndefSigSpec(cell
->getPort(ID::CO
), timestep
);
979 int undef_any_p
= ez
->expression(ezSAT::OpOr
, undef_p
);
980 int undef_any_g
= ez
->expression(ezSAT::OpOr
, undef_g
);
981 int undef_any_ci
= ez
->expression(ezSAT::OpOr
, undef_ci
);
982 int undef_co_bit
= ez
->OR(undef_any_p
, undef_any_g
, undef_any_ci
);
984 std::vector
<int> undef_co_bits(undef_co
.size(), undef_co_bit
);
985 ez
->assume(ez
->vec_eq(undef_co_bits
, undef_co
));
987 undefGating(co
, yy
, undef_co
);
992 if (cell
->type
== ID($alu
))
994 std::vector
<int> a
= importDefSigSpec(cell
->getPort(ID::A
), timestep
);
995 std::vector
<int> b
= importDefSigSpec(cell
->getPort(ID::B
), timestep
);
996 std::vector
<int> y
= importDefSigSpec(cell
->getPort(ID::Y
), timestep
);
997 std::vector
<int> x
= importDefSigSpec(cell
->getPort(ID::X
), timestep
);
998 std::vector
<int> ci
= importDefSigSpec(cell
->getPort(ID::CI
), timestep
);
999 std::vector
<int> bi
= importDefSigSpec(cell
->getPort(ID::BI
), timestep
);
1000 std::vector
<int> co
= importDefSigSpec(cell
->getPort(ID::CO
), timestep
);
1002 extendSignalWidth(a
, b
, y
, cell
);
1003 extendSignalWidth(a
, b
, x
, cell
);
1004 extendSignalWidth(a
, b
, co
, cell
);
1006 std::vector
<int> def_y
= model_undef
? ez
->vec_var(y
.size()) : y
;
1007 std::vector
<int> def_x
= model_undef
? ez
->vec_var(x
.size()) : x
;
1008 std::vector
<int> def_co
= model_undef
? ez
->vec_var(co
.size()) : co
;
1010 log_assert(GetSize(y
) == GetSize(x
));
1011 log_assert(GetSize(y
) == GetSize(co
));
1012 log_assert(GetSize(ci
) == 1);
1013 log_assert(GetSize(bi
) == 1);
1015 for (int i
= 0; i
< GetSize(y
); i
++)
1017 int s1
= a
.at(i
), s2
= ez
->XOR(b
.at(i
), bi
.at(0)), s3
= i
? co
.at(i
-1) : ci
.at(0);
1018 ez
->SET(def_x
.at(i
), ez
->XOR(s1
, s2
));
1019 ez
->SET(def_y
.at(i
), ez
->XOR(def_x
.at(i
), s3
));
1020 ez
->SET(def_co
.at(i
), ez
->OR(ez
->AND(s1
, s2
), ez
->AND(s1
, s3
), ez
->AND(s2
, s3
)));
1025 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort(ID::A
), timestep
);
1026 std::vector
<int> undef_b
= importUndefSigSpec(cell
->getPort(ID::B
), timestep
);
1027 std::vector
<int> undef_ci
= importUndefSigSpec(cell
->getPort(ID::CI
), timestep
);
1028 std::vector
<int> undef_bi
= importUndefSigSpec(cell
->getPort(ID::BI
), timestep
);
1030 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort(ID::Y
), timestep
);
1031 std::vector
<int> undef_x
= importUndefSigSpec(cell
->getPort(ID::X
), timestep
);
1032 std::vector
<int> undef_co
= importUndefSigSpec(cell
->getPort(ID::CO
), timestep
);
1034 extendSignalWidth(undef_a
, undef_b
, undef_y
, cell
);
1035 extendSignalWidth(undef_a
, undef_b
, undef_x
, cell
);
1036 extendSignalWidth(undef_a
, undef_b
, undef_co
, cell
);
1038 std::vector
<int> all_inputs_undef
;
1039 all_inputs_undef
.insert(all_inputs_undef
.end(), undef_a
.begin(), undef_a
.end());
1040 all_inputs_undef
.insert(all_inputs_undef
.end(), undef_b
.begin(), undef_b
.end());
1041 all_inputs_undef
.insert(all_inputs_undef
.end(), undef_ci
.begin(), undef_ci
.end());
1042 all_inputs_undef
.insert(all_inputs_undef
.end(), undef_bi
.begin(), undef_bi
.end());
1043 int undef_any
= ez
->expression(ezSAT::OpOr
, all_inputs_undef
);
1045 for (int i
= 0; i
< GetSize(undef_y
); i
++) {
1046 ez
->SET(undef_y
.at(i
), undef_any
);
1047 ez
->SET(undef_x
.at(i
), ez
->OR(undef_a
.at(i
), undef_b
.at(i
), undef_bi
.at(0)));
1048 ez
->SET(undef_co
.at(i
), undef_any
);
1051 undefGating(y
, def_y
, undef_y
);
1052 undefGating(x
, def_x
, undef_x
);
1053 undefGating(co
, def_co
, undef_co
);
1058 if (cell
->type
== ID($slice
))
1060 RTLIL::SigSpec a
= cell
->getPort(ID::A
);
1061 RTLIL::SigSpec y
= cell
->getPort(ID::Y
);
1062 ez
->assume(signals_eq(a
.extract(cell
->parameters
.at(ID::OFFSET
).as_int(), y
.size()), y
, timestep
));
1066 if (cell
->type
== ID($concat
))
1068 RTLIL::SigSpec a
= cell
->getPort(ID::A
);
1069 RTLIL::SigSpec b
= cell
->getPort(ID::B
);
1070 RTLIL::SigSpec y
= cell
->getPort(ID::Y
);
1072 RTLIL::SigSpec ab
= a
;
1075 ez
->assume(signals_eq(ab
, y
, timestep
));
1079 if (timestep
> 0 && RTLIL::builtin_ff_cell_types().count(cell
->type
))
1081 FfData
ff(nullptr, cell
);
1083 // Latches and FFs with async inputs are not supported — use clk2fflogic or async2sync first.
1084 if (!ff
.has_d
|| ff
.has_arst
|| ff
.has_sr
|| (ff
.has_en
&& !ff
.has_clk
))
1089 initial_state
.add((*sigmap
)(cell
->getPort(ID::Q
)));
1093 std::vector
<int> d
= importDefSigSpec(cell
->getPort(ID::D
), timestep
-1);
1094 std::vector
<int> undef_d
;
1096 undef_d
= importUndefSigSpec(cell
->getPort(ID::D
), timestep
-1);
1097 if (ff
.has_srst
&& ff
.has_en
&& ff
.ce_over_srst
) {
1098 int srst
= importDefSigSpec(ff
.sig_srst
, timestep
-1).at(0);
1099 std::vector
<int> rval
= importDefSigSpec(ff
.val_srst
, timestep
-1);
1101 std::vector
<int> undef_rval
;
1103 undef_srst
= importUndefSigSpec(ff
.sig_srst
, timestep
-1).at(0);
1104 undef_rval
= importUndefSigSpec(ff
.val_srst
, timestep
-1);
1107 std::tie(d
, undef_d
) = mux(srst
, undef_srst
, d
, undef_d
, rval
, undef_rval
);
1109 std::tie(d
, undef_d
) = mux(srst
, undef_srst
, rval
, undef_rval
, d
, undef_d
);
1112 int en
= importDefSigSpec(ff
.sig_en
, timestep
-1).at(0);
1113 std::vector
<int> old_q
= importDefSigSpec(ff
.sig_q
, timestep
-1);
1115 std::vector
<int> undef_old_q
;
1117 undef_en
= importUndefSigSpec(ff
.sig_en
, timestep
-1).at(0);
1118 undef_old_q
= importUndefSigSpec(ff
.sig_q
, timestep
-1);
1121 std::tie(d
, undef_d
) = mux(en
, undef_en
, old_q
, undef_old_q
, d
, undef_d
);
1123 std::tie(d
, undef_d
) = mux(en
, undef_en
, d
, undef_d
, old_q
, undef_old_q
);
1125 if (ff
.has_srst
&& !(ff
.has_en
&& ff
.ce_over_srst
)) {
1126 int srst
= importDefSigSpec(ff
.sig_srst
, timestep
-1).at(0);
1127 std::vector
<int> rval
= importDefSigSpec(ff
.val_srst
, timestep
-1);
1129 std::vector
<int> undef_rval
;
1131 undef_srst
= importUndefSigSpec(ff
.sig_srst
, timestep
-1).at(0);
1132 undef_rval
= importUndefSigSpec(ff
.val_srst
, timestep
-1);
1135 std::tie(d
, undef_d
) = mux(srst
, undef_srst
, d
, undef_d
, rval
, undef_rval
);
1137 std::tie(d
, undef_d
) = mux(srst
, undef_srst
, rval
, undef_rval
, d
, undef_d
);
1139 std::vector
<int> q
= importDefSigSpec(cell
->getPort(ID::Q
), timestep
);
1141 std::vector
<int> qq
= model_undef
? ez
->vec_var(q
.size()) : q
;
1142 ez
->assume(ez
->vec_eq(d
, qq
));
1146 std::vector
<int> undef_q
= importUndefSigSpec(cell
->getPort(ID::Q
), timestep
);
1148 ez
->assume(ez
->vec_eq(undef_d
, undef_q
));
1149 undefGating(q
, qq
, undef_q
);
1155 if (cell
->type
== ID($anyconst
))
1160 std::vector
<int> d
= importDefSigSpec(cell
->getPort(ID::Y
), timestep
-1);
1161 std::vector
<int> q
= importDefSigSpec(cell
->getPort(ID::Y
), timestep
);
1163 std::vector
<int> qq
= model_undef
? ez
->vec_var(q
.size()) : q
;
1164 ez
->assume(ez
->vec_eq(d
, qq
));
1168 std::vector
<int> undef_d
= importUndefSigSpec(cell
->getPort(ID::Y
), timestep
-1);
1169 std::vector
<int> undef_q
= importUndefSigSpec(cell
->getPort(ID::Y
), timestep
);
1171 ez
->assume(ez
->vec_eq(undef_d
, undef_q
));
1172 undefGating(q
, qq
, undef_q
);
1177 if (cell
->type
== ID($anyseq
))
1182 if (cell
->type
.in(ID($_BUF_
), ID($equiv
)))
1184 std::vector
<int> a
= importDefSigSpec(cell
->getPort(ID::A
), timestep
);
1185 std::vector
<int> y
= importDefSigSpec(cell
->getPort(ID::Y
), timestep
);
1186 extendSignalWidthUnary(a
, y
, cell
);
1188 std::vector
<int> yy
= model_undef
? ez
->vec_var(y
.size()) : y
;
1189 ez
->assume(ez
->vec_eq(a
, yy
));
1192 std::vector
<int> undef_a
= importUndefSigSpec(cell
->getPort(ID::A
), timestep
);
1193 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort(ID::Y
), timestep
);
1194 extendSignalWidthUnary(undef_a
, undef_y
, cell
, false);
1195 ez
->assume(ez
->vec_eq(undef_a
, undef_y
));
1196 undefGating(y
, yy
, undef_y
);
1201 if (cell
->type
== ID($initstate
))
1203 auto key
= make_pair(prefix
, timestep
);
1204 if (initstates
.count(key
) == 0)
1205 initstates
[key
] = false;
1207 std::vector
<int> y
= importDefSigSpec(cell
->getPort(ID::Y
), timestep
);
1208 log_assert(GetSize(y
) == 1);
1209 ez
->SET(y
[0], initstates
[key
] ? ez
->CONST_TRUE
: ez
->CONST_FALSE
);
1212 std::vector
<int> undef_y
= importUndefSigSpec(cell
->getPort(ID::Y
), timestep
);
1213 log_assert(GetSize(undef_y
) == 1);
1214 ez
->SET(undef_y
[0], ez
->CONST_FALSE
);
1220 if (cell
->type
== ID($
assert))
1222 std::string pf
= prefix
+ (timestep
== -1 ? "" : stringf("@%d:", timestep
));
1223 asserts_a
[pf
].append((*sigmap
)(cell
->getPort(ID::A
)));
1224 asserts_en
[pf
].append((*sigmap
)(cell
->getPort(ID::EN
)));
1228 if (cell
->type
== ID($assume
))
1230 std::string pf
= prefix
+ (timestep
== -1 ? "" : stringf("@%d:", timestep
));
1231 assumes_a
[pf
].append((*sigmap
)(cell
->getPort(ID::A
)));
1232 assumes_en
[pf
].append((*sigmap
)(cell
->getPort(ID::EN
)));
1236 // Unsupported internal cell types: $pow $fsm $mem*
1237 // .. and all sequential cells with asynchronous inputs