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/rtlil.h"
21 #include "kernel/register.h"
22 #include "kernel/sigtools.h"
23 #include "kernel/celltypes.h"
24 #include "kernel/log.h"
28 PRIVATE_NAMESPACE_BEGIN
34 RTLIL::Module
*module
;
39 int initstate_nid
= -1;
42 dict
<int, int> sorts_bv
;
44 // (<address-width>, <data-width>) => <sid>
45 dict
<pair
<int, int>, int> sorts_mem
;
47 // SigBit => (<nid>, <bitidx>)
48 dict
<SigBit
, pair
<int, int>> bit_nid
;
51 dict
<int, int> nid_width
;
54 dict
<SigSpec
, int> sig_nid
;
56 // bit to driving cell
57 dict
<SigBit
, Cell
*> bit_cell
;
60 dict
<Const
, int> consts
;
62 // ff inputs that need to be evaluated (<nid>, <ff_cell>)
63 vector
<pair
<int, Cell
*>> ff_todo
;
65 pool
<Cell
*> cell_recursion_guard
;
66 vector
<int> bad_properties
;
67 dict
<SigBit
, bool> initbits
;
68 pool
<Wire
*> statewires
;
71 void btorf(const char *fmt
, ...)
75 f
<< indent
<< vstringf(fmt
, ap
);
79 void btorf_push(const string
&id
)
82 f
<< indent
<< stringf(" ; begin %s\n", id
.c_str());
87 void btorf_pop(const string
&id
)
90 indent
= indent
.substr(4);
91 f
<< indent
<< stringf(" ; end %s\n", id
.c_str());
95 int get_bv_sid(int width
)
97 if (sorts_bv
.count(width
) == 0) {
99 btorf("%d sort bitvec %d\n", nid
, width
);
100 sorts_bv
[width
] = nid
;
102 return sorts_bv
.at(width
);
105 void add_nid_sig(int nid
, const SigSpec
&sig
)
108 f
<< indent
<< stringf("; %d %s\n", nid
, log_signal(sig
));
110 for (int i
= 0; i
< GetSize(sig
); i
++)
111 bit_nid
[sig
[i
]] = make_pair(nid
, i
);
114 nid_width
[nid
] = GetSize(sig
);
117 void export_cell(Cell
*cell
)
119 log_assert(cell_recursion_guard
.count(cell
) == 0);
120 cell_recursion_guard
.insert(cell
);
121 btorf_push(log_id(cell
));
123 if (cell
->type
.in("$add", "$sub", "$and", "$or", "$xor", "$xnor", "$shl", "$sshl", "$shr", "$sshr", "$shift", "$shiftx",
124 "$_AND_", "$_NAND_", "$_OR_", "$_NOR_", "$_XOR_", "$_XNOR_"))
127 if (cell
->type
== "$add") btor_op
= "add";
128 if (cell
->type
== "$sub") btor_op
= "sub";
129 if (cell
->type
.in("$shl", "$sshl")) btor_op
= "sll";
130 if (cell
->type
== "$shr") btor_op
= "srl";
131 if (cell
->type
== "$sshr") btor_op
= "sra";
132 if (cell
->type
.in("$shift", "$shiftx")) btor_op
= "shift";
133 if (cell
->type
.in("$and", "$_AND_")) btor_op
= "and";
134 if (cell
->type
.in("$or", "$_OR_")) btor_op
= "or";
135 if (cell
->type
.in("$xor", "$_XOR_")) btor_op
= "xor";
136 if (cell
->type
== "$_NAND_") btor_op
= "nand";
137 if (cell
->type
== "$_NOR_") btor_op
= "nor";
138 if (cell
->type
.in("$xnor", "$_XNOR_")) btor_op
= "xnor";
139 log_assert(!btor_op
.empty());
141 int width
= GetSize(cell
->getPort("\\Y"));
142 width
= std::max(width
, GetSize(cell
->getPort("\\A")));
143 width
= std::max(width
, GetSize(cell
->getPort("\\B")));
145 bool a_signed
= cell
->hasParam("\\A_SIGNED") ? cell
->getParam("\\A_SIGNED").as_bool() : false;
146 bool b_signed
= cell
->hasParam("\\B_SIGNED") ? cell
->getParam("\\B_SIGNED").as_bool() : false;
148 if (btor_op
== "shift" && !b_signed
)
151 if (cell
->type
.in("$shl", "$sshl", "$shr", "$sshr"))
154 if (cell
->type
== "$sshr" && !a_signed
)
157 int sid
= get_bv_sid(width
);
160 if (btor_op
== "shift")
162 int nid_a
= get_sig_nid(cell
->getPort("\\A"), width
, false);
163 int nid_b
= get_sig_nid(cell
->getPort("\\B"), width
, b_signed
);
165 int nid_r
= next_nid
++;
166 btorf("%d srl %d %d %d\n", nid_r
, sid
, nid_a
, nid_b
);
168 int nid_b_neg
= next_nid
++;
169 btorf("%d neg %d %d\n", nid_b_neg
, sid
, nid_b
);
171 int nid_l
= next_nid
++;
172 btorf("%d sll %d %d %d\n", nid_l
, sid
, nid_a
, nid_b_neg
);
174 int sid_bit
= get_bv_sid(1);
175 int nid_zero
= get_sig_nid(Const(0, width
));
176 int nid_b_ltz
= next_nid
++;
177 btorf("%d slt %d %d %d\n", nid_b_ltz
, sid_bit
, nid_b
, nid_zero
);
180 btorf("%d ite %d %d %d %d\n", nid
, sid
, nid_b_ltz
, nid_l
, nid_r
);
184 int nid_a
= get_sig_nid(cell
->getPort("\\A"), width
, a_signed
);
185 int nid_b
= get_sig_nid(cell
->getPort("\\B"), width
, b_signed
);
188 btorf("%d %s %d %d %d\n", nid
, btor_op
.c_str(), sid
, nid_a
, nid_b
);
191 SigSpec sig
= sigmap(cell
->getPort("\\Y"));
193 if (GetSize(sig
) < width
) {
194 int sid
= get_bv_sid(GetSize(sig
));
195 int nid2
= next_nid
++;
196 btorf("%d slice %d %d %d 0\n", nid2
, sid
, nid
, GetSize(sig
)-1);
200 add_nid_sig(nid
, sig
);
204 if (cell
->type
.in("$_ANDNOT_", "$_ORNOT_"))
206 int sid
= get_bv_sid(1);
207 int nid_a
= get_sig_nid(cell
->getPort("\\A"));
208 int nid_b
= get_sig_nid(cell
->getPort("\\B"));
210 int nid1
= next_nid
++;
211 int nid2
= next_nid
++;
213 if (cell
->type
== "$_ANDNOT_") {
214 btorf("%d not %d %d\n", nid1
, sid
, nid_b
);
215 btorf("%d and %d %d %d\n", nid2
, sid
, nid_a
, nid1
);
218 if (cell
->type
== "$_ORNOT_") {
219 btorf("%d not %d %d\n", nid1
, sid
, nid_b
);
220 btorf("%d or %d %d %d\n", nid2
, sid
, nid_a
, nid1
);
223 SigSpec sig
= sigmap(cell
->getPort("\\Y"));
224 add_nid_sig(nid2
, sig
);
228 if (cell
->type
.in("$_OAI3_", "$_AOI3_"))
230 int sid
= get_bv_sid(1);
231 int nid_a
= get_sig_nid(cell
->getPort("\\A"));
232 int nid_b
= get_sig_nid(cell
->getPort("\\B"));
233 int nid_c
= get_sig_nid(cell
->getPort("\\C"));
235 int nid1
= next_nid
++;
236 int nid2
= next_nid
++;
237 int nid3
= next_nid
++;
239 if (cell
->type
== "$_OAI3_") {
240 btorf("%d or %d %d %d\n", nid1
, sid
, nid_a
, nid_b
);
241 btorf("%d and %d %d %d\n", nid2
, sid
, nid1
, nid_c
);
242 btorf("%d not %d %d\n", nid3
, sid
, nid2
);
245 if (cell
->type
== "$_AOI3_") {
246 btorf("%d and %d %d %d\n", nid1
, sid
, nid_a
, nid_b
);
247 btorf("%d or %d %d %d\n", nid2
, sid
, nid1
, nid_c
);
248 btorf("%d not %d %d\n", nid3
, sid
, nid2
);
251 SigSpec sig
= sigmap(cell
->getPort("\\Y"));
252 add_nid_sig(nid3
, sig
);
256 if (cell
->type
.in("$_OAI4_", "$_AOI4_"))
258 int sid
= get_bv_sid(1);
259 int nid_a
= get_sig_nid(cell
->getPort("\\A"));
260 int nid_b
= get_sig_nid(cell
->getPort("\\B"));
261 int nid_c
= get_sig_nid(cell
->getPort("\\C"));
262 int nid_d
= get_sig_nid(cell
->getPort("\\D"));
264 int nid1
= next_nid
++;
265 int nid2
= next_nid
++;
266 int nid3
= next_nid
++;
267 int nid4
= next_nid
++;
269 if (cell
->type
== "$_OAI4_") {
270 btorf("%d or %d %d %d\n", nid1
, sid
, nid_a
, nid_b
);
271 btorf("%d or %d %d %d\n", nid2
, sid
, nid_c
, nid_d
);
272 btorf("%d and %d %d %d\n", nid3
, sid
, nid1
, nid2
);
273 btorf("%d not %d %d\n", nid4
, sid
, nid3
);
276 if (cell
->type
== "$_AOI4_") {
277 btorf("%d and %d %d %d\n", nid1
, sid
, nid_a
, nid_b
);
278 btorf("%d and %d %d %d\n", nid2
, sid
, nid_c
, nid_d
);
279 btorf("%d or %d %d %d\n", nid3
, sid
, nid1
, nid2
);
280 btorf("%d not %d %d\n", nid4
, sid
, nid3
);
283 SigSpec sig
= sigmap(cell
->getPort("\\Y"));
284 add_nid_sig(nid4
, sig
);
288 if (cell
->type
.in("$lt", "$le", "$eq", "$eqx", "$ne", "$nex", "$ge", "$gt"))
291 if (cell
->type
== "$lt") btor_op
= "lt";
292 if (cell
->type
== "$le") btor_op
= "lte";
293 if (cell
->type
.in("$eq", "$eqx")) btor_op
= "eq";
294 if (cell
->type
.in("$ne", "$nex")) btor_op
= "ne";
295 if (cell
->type
== "$ge") btor_op
= "gte";
296 if (cell
->type
== "$gt") btor_op
= "gt";
297 log_assert(!btor_op
.empty());
300 width
= std::max(width
, GetSize(cell
->getPort("\\A")));
301 width
= std::max(width
, GetSize(cell
->getPort("\\B")));
303 bool a_signed
= cell
->hasParam("\\A_SIGNED") ? cell
->getParam("\\A_SIGNED").as_bool() : false;
304 bool b_signed
= cell
->hasParam("\\B_SIGNED") ? cell
->getParam("\\B_SIGNED").as_bool() : false;
306 int sid
= get_bv_sid(1);
307 int nid_a
= get_sig_nid(cell
->getPort("\\A"), width
, a_signed
);
308 int nid_b
= get_sig_nid(cell
->getPort("\\B"), width
, b_signed
);
310 int nid
= next_nid
++;
311 if (cell
->type
.in("$lt", "$le", "$ge", "$gt")) {
312 btorf("%d %c%s %d %d %d\n", nid
, a_signed
|| b_signed
? 's' : 'u', btor_op
.c_str(), sid
, nid_a
, nid_b
);
314 btorf("%d %s %d %d %d\n", nid
, btor_op
.c_str(), sid
, nid_a
, nid_b
);
317 SigSpec sig
= sigmap(cell
->getPort("\\Y"));
319 if (GetSize(sig
) > 1) {
320 int sid
= get_bv_sid(GetSize(sig
));
321 int nid2
= next_nid
++;
322 btorf("%d uext %d %d %d\n", nid2
, sid
, nid
, GetSize(sig
) - 1);
326 add_nid_sig(nid
, sig
);
330 if (cell
->type
.in("$not", "$neg", "$_NOT_"))
333 if (cell
->type
.in("$not", "$_NOT_")) btor_op
= "not";
334 if (cell
->type
== "$neg") btor_op
= "neg";
335 log_assert(!btor_op
.empty());
337 int width
= GetSize(cell
->getPort("\\Y"));
338 width
= std::max(width
, GetSize(cell
->getPort("\\A")));
340 bool a_signed
= cell
->hasParam("\\A_SIGNED") ? cell
->getParam("\\A_SIGNED").as_bool() : false;
342 int sid
= get_bv_sid(width
);
343 int nid_a
= get_sig_nid(cell
->getPort("\\A"), width
, a_signed
);
345 int nid
= next_nid
++;
346 btorf("%d %s %d %d\n", nid
, btor_op
.c_str(), sid
, nid_a
);
348 SigSpec sig
= sigmap(cell
->getPort("\\Y"));
350 if (GetSize(sig
) < width
) {
351 int sid
= get_bv_sid(GetSize(sig
));
352 int nid2
= next_nid
++;
353 btorf("%d slice %d %d %d 0\n", nid2
, sid
, nid
, GetSize(sig
)-1);
357 add_nid_sig(nid
, sig
);
361 if (cell
->type
.in("$logic_and", "$logic_or", "$logic_not"))
364 if (cell
->type
== "$logic_and") btor_op
= "and";
365 if (cell
->type
== "$logic_or") btor_op
= "or";
366 if (cell
->type
== "$logic_not") btor_op
= "not";
367 log_assert(!btor_op
.empty());
369 int sid
= get_bv_sid(1);
370 int nid_a
= get_sig_nid(cell
->getPort("\\A"));
371 int nid_b
= btor_op
!= "not" ? get_sig_nid(cell
->getPort("\\B")) : 0;
373 if (GetSize(cell
->getPort("\\A")) > 1) {
374 int nid_red_a
= next_nid
++;
375 btorf("%d redor %d %d\n", nid_red_a
, sid
, nid_a
);
379 if (btor_op
!= "not" && GetSize(cell
->getPort("\\B")) > 1) {
380 int nid_red_b
= next_nid
++;
381 btorf("%d redor %d %d\n", nid_red_b
, sid
, nid_b
);
385 int nid
= next_nid
++;
386 if (btor_op
!= "not")
387 btorf("%d %s %d %d %d\n", nid
, btor_op
.c_str(), sid
, nid_a
, nid_b
);
389 btorf("%d %s %d %d\n", nid
, btor_op
.c_str(), sid
, nid_a
);
391 SigSpec sig
= sigmap(cell
->getPort("\\Y"));
393 if (GetSize(sig
) > 1) {
394 int sid
= get_bv_sid(GetSize(sig
));
395 int zeros_nid
= get_sig_nid(Const(0, GetSize(sig
)-1));
396 int nid2
= next_nid
++;
397 btorf("%d concat %d %d %d\n", nid2
, sid
, zeros_nid
, nid
);
401 add_nid_sig(nid
, sig
);
405 if (cell
->type
.in("$reduce_and", "$reduce_or", "$reduce_bool", "$reduce_xor", "$reduce_xnor"))
408 if (cell
->type
== "$reduce_and") btor_op
= "redand";
409 if (cell
->type
.in("$reduce_or", "$reduce_bool")) btor_op
= "redor";
410 if (cell
->type
.in("$reduce_xor", "$reduce_xnor")) btor_op
= "redxor";
411 log_assert(!btor_op
.empty());
413 int sid
= get_bv_sid(1);
414 int nid_a
= get_sig_nid(cell
->getPort("\\A"));
416 int nid
= next_nid
++;
417 btorf("%d %s %d %d\n", nid
, btor_op
.c_str(), sid
, nid_a
);
419 if (cell
->type
== "$reduce_xnor") {
420 int nid2
= next_nid
++;
421 btorf("%d not %d %d %d\n", nid2
, sid
, nid
);
425 SigSpec sig
= sigmap(cell
->getPort("\\Y"));
427 if (GetSize(sig
) > 1) {
428 int sid
= get_bv_sid(GetSize(sig
));
429 int zeros_nid
= get_sig_nid(Const(0, GetSize(sig
)-1));
430 int nid2
= next_nid
++;
431 btorf("%d concat %d %d %d\n", nid2
, sid
, zeros_nid
, nid
);
435 add_nid_sig(nid
, sig
);
439 if (cell
->type
.in("$mux", "$_MUX_"))
441 SigSpec sig_a
= sigmap(cell
->getPort("\\A"));
442 SigSpec sig_b
= sigmap(cell
->getPort("\\B"));
443 SigSpec sig_s
= sigmap(cell
->getPort("\\S"));
444 SigSpec sig_y
= sigmap(cell
->getPort("\\Y"));
446 int nid_a
= get_sig_nid(sig_a
);
447 int nid_b
= get_sig_nid(sig_b
);
448 int nid_s
= get_sig_nid(sig_s
);
450 int sid
= get_bv_sid(GetSize(sig_y
));
451 int nid
= next_nid
++;
452 btorf("%d ite %d %d %d %d\n", nid
, sid
, nid_s
, nid_b
, nid_a
);
454 add_nid_sig(nid
, sig_y
);
458 if (cell
->type
== "$pmux")
460 SigSpec sig_a
= sigmap(cell
->getPort("\\A"));
461 SigSpec sig_b
= sigmap(cell
->getPort("\\B"));
462 SigSpec sig_s
= sigmap(cell
->getPort("\\S"));
463 SigSpec sig_y
= sigmap(cell
->getPort("\\Y"));
465 int width
= GetSize(sig_a
);
466 int sid
= get_bv_sid(width
);
467 int nid
= get_sig_nid(sig_a
);
469 for (int i
= 0; i
< GetSize(sig_s
); i
++) {
470 int nid_b
= get_sig_nid(sig_b
.extract(i
*width
, width
));
471 int nid_s
= get_sig_nid(sig_s
.extract(i
));
472 int nid2
= next_nid
++;
473 btorf("%d ite %d %d %d %d\n", nid2
, sid
, nid_s
, nid_b
, nid
);
477 add_nid_sig(nid
, sig_y
);
481 if (cell
->type
.in("$dff", "$ff", "$_DFF_P_", "$_DFF_N", "$_FF_"))
483 SigSpec sig_d
= sigmap(cell
->getPort("\\D"));
484 SigSpec sig_q
= sigmap(cell
->getPort("\\Q"));
488 if (sig_q
.is_wire()) {
489 Wire
*w
= sig_q
.as_wire();
490 if (w
->port_id
== 0) {
491 statewires
.insert(w
);
496 int sid
= get_bv_sid(GetSize(sig_q
));
497 int nid
= next_nid
++;
500 btorf("%d state %d\n", nid
, sid
);
502 btorf("%d state %d %s\n", nid
, sid
, log_id(symbol
));
505 for (int i
= 0; i
< GetSize(sig_q
); i
++)
506 if (initbits
.count(sig_q
[i
]))
507 initval
.bits
.push_back(initbits
.at(sig_q
[i
]) ? State::S1
: State::S0
);
509 initval
.bits
.push_back(State::Sx
);
511 if (!initval
.is_fully_undef()) {
512 int nid_init_val
= get_sig_nid(initval
);
513 int nid_init
= next_nid
++;
515 btorf("; initval = %s\n", log_signal(initval
));
516 btorf("%d init %d %d %d\n", nid_init
, sid
, nid
, nid_init_val
);
519 ff_todo
.push_back(make_pair(nid
, cell
));
520 add_nid_sig(nid
, sig_q
);
524 if (cell
->type
.in("$anyconst", "$anyseq"))
526 SigSpec sig_y
= sigmap(cell
->getPort("\\Y"));
528 int sid
= get_bv_sid(GetSize(sig_y
));
529 int nid
= next_nid
++;
531 btorf("%d state %d\n", nid
, sid
);
533 if (cell
->type
== "$anyconst") {
534 int nid2
= next_nid
++;
535 btorf("%d next %d %d %d\n", nid2
, sid
, nid
, nid
);
538 add_nid_sig(nid
, sig_y
);
542 if (cell
->type
== "$initstate")
544 SigSpec sig_y
= sigmap(cell
->getPort("\\Y"));
546 if (initstate_nid
< 0)
548 int sid
= get_bv_sid(1);
549 int one_nid
= get_sig_nid(Const(1, 1));
550 int zero_nid
= get_sig_nid(Const(0, 1));
551 initstate_nid
= next_nid
++;
552 btorf("%d state %d\n", initstate_nid
, sid
);
553 btorf("%d init %d %d %d\n", next_nid
++, sid
, initstate_nid
, one_nid
);
554 btorf("%d next %d %d %d\n", next_nid
++, sid
, initstate_nid
, zero_nid
);
557 add_nid_sig(initstate_nid
, sig_y
);
561 log_error("Unsupported cell type: %s (%s)\n", log_id(cell
->type
), log_id(cell
));
564 btorf_pop(log_id(cell
));
565 cell_recursion_guard
.erase(cell
);
568 int get_sig_nid(SigSpec sig
, int to_width
= -1, bool is_signed
= false)
574 if (bit
== State::Sx
)
580 SigSpec sig_mask_undef
, sig_noundef
;
581 int first_undef
= -1;
583 for (int i
= 0; i
< GetSize(sig
); i
++)
584 if (sig
[i
] == State::Sx
) {
587 sig_mask_undef
.append(State::S1
);
588 sig_noundef
.append(State::S0
);
590 sig_mask_undef
.append(State::S0
);
591 sig_noundef
.append(sig
[i
]);
594 if (to_width
< 0 || first_undef
< to_width
)
596 int sid
= get_bv_sid(GetSize(sig
));
598 int nid_input
= next_nid
++;
599 btorf("%d input %d\n", nid_input
, sid
);
601 int nid_masked_input
;
602 if (sig_mask_undef
.is_fully_ones()) {
603 nid_masked_input
= nid_input
;
605 int nid_mask_undef
= get_sig_nid(sig_mask_undef
);
606 nid_masked_input
= next_nid
++;
607 btorf("%d and %d %d %d\n", nid_masked_input
, sid
, nid_input
, nid_mask_undef
);
610 if (sig_noundef
.is_fully_zero()) {
611 nid
= nid_masked_input
;
613 int nid_noundef
= get_sig_nid(sig_noundef
);
615 btorf("%d or %d %d %d\n", nid
, sid
, nid_masked_input
, nid_noundef
);
624 if (sig_nid
.count(sig
) == 0)
627 vector
<pair
<int, int>> nidbits
;
630 for (int i
= 0; i
< GetSize(sig
); i
++)
634 if (bit_nid
.count(bit
) == 0)
636 if (bit
.wire
== nullptr)
640 while (i
+GetSize(c
) < GetSize(sig
) && sig
[i
+GetSize(c
)].wire
== nullptr)
641 c
.bits
.push_back(sig
[i
+GetSize(c
)].data
);
643 if (consts
.count(c
) == 0) {
644 int sid
= get_bv_sid(GetSize(c
));
645 int nid
= next_nid
++;
646 btorf("%d const %d %s\n", nid
, sid
, c
.as_string().c_str());
648 nid_width
[nid
] = GetSize(c
);
651 int nid
= consts
.at(c
);
653 for (int j
= 0; j
< GetSize(c
); j
++)
654 nidbits
.push_back(make_pair(nid
, j
));
661 export_cell(bit_cell
.at(bit
));
662 log_assert(bit_nid
.count(bit
));
666 nidbits
.push_back(bit_nid
.at(bit
));
672 // group bits and emit slice-concat chain
673 for (int i
= 0; i
< GetSize(nidbits
); i
++)
675 int nid2
= nidbits
[i
].first
;
676 int lower
= nidbits
[i
].second
;
679 while (i
+1 < GetSize(nidbits
) && nidbits
[i
+1].first
== nidbits
[i
].first
&&
680 nidbits
[i
+1].second
== nidbits
[i
].second
+1)
685 if (lower
!= 0 || upper
+1 != nid_width
.at(nid2
)) {
686 int sid
= get_bv_sid(upper
-lower
+1);
688 btorf("%d slice %d %d %d %d\n", nid3
, sid
, nid2
, upper
, lower
);
694 int sid
= get_bv_sid(width
+upper
-lower
+1);
696 btorf("%d concat %d %d %d\n", nid4
, sid
, nid3
, nid
);
699 width
+= upper
-lower
+1;
704 nid_width
[nid
] = width
;
707 nid
= sig_nid
.at(sig
);
710 if (to_width
>= 0 && to_width
!= GetSize(sig
))
712 if (to_width
< GetSize(sig
))
714 int sid
= get_bv_sid(to_width
);
715 int nid2
= next_nid
++;
716 btorf("%d slice %d %d %d 0\n", nid2
, sid
, nid
, to_width
-1);
721 int sid
= get_bv_sid(to_width
);
722 int nid2
= next_nid
++;
723 btorf("%d %s %d %d %d\n", nid2
, is_signed
? "sext" : "uext",
724 sid
, nid
, to_width
- GetSize(sig
));
732 BtorWorker(std::ostream
&f
, RTLIL::Module
*module
, bool verbose
, bool single_bad
) :
733 f(f
), sigmap(module
), module(module
), verbose(verbose
), single_bad(single_bad
)
735 btorf_push("inputs");
737 for (auto wire
: module
->wires())
739 if (wire
->attributes
.count("\\init")) {
740 Const attrval
= wire
->attributes
.at("\\init");
741 for (int i
= 0; i
< GetSize(wire
) && i
< GetSize(attrval
); i
++)
742 if (attrval
[i
] == State::S0
|| attrval
[i
] == State::S1
)
743 initbits
[sigmap(SigBit(wire
, i
))] = (attrval
[i
] == State::S1
);
746 if (!wire
->port_id
|| !wire
->port_input
)
749 SigSpec sig
= sigmap(wire
);
750 int sid
= get_bv_sid(GetSize(sig
));
751 int nid
= next_nid
++;
753 btorf("%d input %d %s\n", nid
, sid
, log_id(wire
));
754 add_nid_sig(nid
, sig
);
759 for (auto cell
: module
->cells())
760 for (auto &conn
: cell
->connections())
762 if (!cell
->output(conn
.first
))
765 for (auto bit
: sigmap(conn
.second
))
766 bit_cell
[bit
] = cell
;
769 for (auto wire
: module
->wires())
771 if (!wire
->port_id
|| !wire
->port_output
)
774 btorf_push(stringf("output %s", log_id(wire
)));
776 int sid
= get_bv_sid(GetSize(wire
));
777 int nid
= get_sig_nid(wire
);
778 btorf("%d output %d %d %s\n", next_nid
++, sid
, nid
, log_id(wire
));
780 btorf_pop(stringf("output %s", log_id(wire
)));
783 for (auto cell
: module
->cells())
785 if (cell
->type
== "$assume")
787 btorf_push(log_id(cell
));
789 int sid
= get_bv_sid(1);
790 int nid_a
= get_sig_nid(cell
->getPort("\\A"));
791 int nid_en
= get_sig_nid(cell
->getPort("\\EN"));
792 int nid_not_en
= next_nid
++;
793 int nid_a_or_not_en
= next_nid
++;
794 int nid
= next_nid
++;
796 btorf("%d not %d %d\n", nid_not_en
, sid
, nid_en
);
797 btorf("%d or %d %d %d\n", nid_a_or_not_en
, sid
, nid_a
, nid_not_en
);
798 btorf("%d constraint %d\n", nid
, nid_a_or_not_en
);
800 btorf_pop(log_id(cell
));
803 if (cell
->type
== "$assert")
805 btorf_push(log_id(cell
));
807 int sid
= get_bv_sid(1);
808 int nid_a
= get_sig_nid(cell
->getPort("\\A"));
809 int nid_en
= get_sig_nid(cell
->getPort("\\EN"));
810 int nid_not_a
= next_nid
++;
811 int nid_en_and_not_a
= next_nid
++;
813 btorf("%d not %d %d\n", nid_not_a
, sid
, nid_a
);
814 btorf("%d and %d %d %d\n", nid_en_and_not_a
, sid
, nid_en
, nid_not_a
);
817 bad_properties
.push_back(nid_en_and_not_a
);
819 int nid
= next_nid
++;
820 btorf("%d bad %d\n", nid
, nid_en_and_not_a
);
823 btorf_pop(log_id(cell
));
827 for (auto wire
: module
->wires())
829 if (wire
->port_id
|| wire
->name
[0] == '$')
832 btorf_push(stringf("wire %s", log_id(wire
)));
834 int sid
= get_bv_sid(GetSize(wire
));
835 int nid
= get_sig_nid(sigmap(wire
));
837 if (statewires
.count(wire
))
840 int this_nid
= next_nid
++;
841 btorf("%d uext %d %d %d %s\n", this_nid
, sid
, nid
, 0, log_id(wire
));
843 btorf_pop(stringf("wire %s", log_id(wire
)));
847 while (!ff_todo
.empty())
849 vector
<pair
<int, Cell
*>> todo
;
852 for (auto &it
: todo
)
854 btorf_push(stringf("next %s", log_id(it
.second
)));
856 SigSpec sig
= sigmap(it
.second
->getPort("\\D"));
858 int nid
= get_sig_nid(sig
);
859 int sid
= get_bv_sid(GetSize(sig
));
860 btorf("%d next %d %d %d\n", next_nid
++, sid
, it
.first
, nid
);
862 btorf_pop(stringf("next %s", log_id(it
.second
)));
866 while (!bad_properties
.empty())
869 bad_properties
.swap(todo
);
871 int sid
= get_bv_sid(1);
874 while (cursor
+1 < GetSize(todo
))
876 int nid_a
= todo
[cursor
++];
877 int nid_b
= todo
[cursor
++];
878 int nid
= next_nid
++;
880 bad_properties
.push_back(nid
);
881 btorf("%d or %d %d %d\n", nid
, sid
, nid_a
, nid_b
);
884 if (!bad_properties
.empty()) {
885 if (cursor
< GetSize(todo
))
886 bad_properties
.push_back(todo
[cursor
++]);
887 log_assert(cursor
== GetSize(todo
));
889 int nid
= next_nid
++;
890 log_assert(cursor
== 0);
891 log_assert(GetSize(todo
) == 1);
892 btorf("%d bad %d\n", nid
, todo
[cursor
]);
898 struct BtorBackend
: public Backend
{
899 BtorBackend() : Backend("btor", "write design to BTOR file") { }
902 // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
904 log(" write_btor [options] [filename]\n");
906 log("Write a BTOR description of the current design.\n");
909 log(" Add comments and indentation to BTOR output file\n");
912 log(" Output only a single bad property for all asserts\n");
915 virtual void execute(std::ostream
*&f
, std::string filename
, std::vector
<std::string
> args
, RTLIL::Design
*design
)
917 bool verbose
= false, single_bad
= false;
919 log_header(design
, "Executing BTOR backend.\n");
922 for (argidx
= 1; argidx
< args
.size(); argidx
++)
924 if (args
[argidx
] == "-v") {
928 if (args
[argidx
] == "-s") {
934 extra_args(f
, filename
, args
, argidx
);
936 RTLIL::Module
*topmod
= design
->top_module();
938 if (topmod
== nullptr)
939 log_cmd_error("No top module found.\n");
941 *f
<< stringf("; BTOR description generated by %s for module %s.\n",
942 yosys_version_str
, log_id(topmod
));
944 BtorWorker(*f
, topmod
, verbose
, single_bad
);
946 *f
<< stringf("; end of yosys output\n");
950 PRIVATE_NAMESPACE_END