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 // [[CITE]] Btor2 , BtorMC and Boolector 3.0
21 // Aina Niemetz, Mathias Preiner, Clifford Wolf, Armin Biere
22 // Computer Aided Verification - 30th International Conference, CAV 2018
23 // https://cs.stanford.edu/people/niemetz/publication/2018/niemetzpreinerwolfbiere-cav18/
25 #include "kernel/rtlil.h"
26 #include "kernel/register.h"
27 #include "kernel/sigtools.h"
28 #include "kernel/celltypes.h"
29 #include "kernel/log.h"
33 PRIVATE_NAMESPACE_BEGIN
39 RTLIL::Module
*module
;
44 int initstate_nid
= -1;
47 dict
<int, int> sorts_bv
;
49 // (<address-width>, <data-width>) => <sid>
50 dict
<pair
<int, int>, int> sorts_mem
;
52 // SigBit => (<nid>, <bitidx>)
53 dict
<SigBit
, pair
<int, int>> bit_nid
;
56 dict
<int, int> nid_width
;
59 dict
<SigSpec
, int> sig_nid
;
61 // bit to driving cell
62 dict
<SigBit
, Cell
*> bit_cell
;
65 dict
<Const
, int> consts
;
67 // ff inputs that need to be evaluated (<nid>, <ff_cell>)
68 vector
<pair
<int, Cell
*>> ff_todo
;
70 pool
<Cell
*> cell_recursion_guard
;
71 vector
<int> bad_properties
;
72 dict
<SigBit
, bool> initbits
;
73 pool
<Wire
*> statewires
;
76 void btorf(const char *fmt
, ...)
80 f
<< indent
<< vstringf(fmt
, ap
);
84 void btorf_push(const string
&id
)
87 f
<< indent
<< stringf(" ; begin %s\n", id
.c_str());
92 void btorf_pop(const string
&id
)
95 indent
= indent
.substr(4);
96 f
<< indent
<< stringf(" ; end %s\n", id
.c_str());
100 int get_bv_sid(int width
)
102 if (sorts_bv
.count(width
) == 0) {
103 int nid
= next_nid
++;
104 btorf("%d sort bitvec %d\n", nid
, width
);
105 sorts_bv
[width
] = nid
;
107 return sorts_bv
.at(width
);
110 int get_mem_sid(int abits
, int dbits
)
112 pair
<int, int> key(abits
, dbits
);
113 if (sorts_mem
.count(key
) == 0) {
114 int addr_sid
= get_bv_sid(abits
);
115 int data_sid
= get_bv_sid(dbits
);
116 int nid
= next_nid
++;
117 btorf("%d sort array %d %d\n", nid
, addr_sid
, data_sid
);
118 sorts_mem
[key
] = nid
;
120 return sorts_mem
.at(key
);
123 void add_nid_sig(int nid
, const SigSpec
&sig
)
126 f
<< indent
<< stringf("; %d %s\n", nid
, log_signal(sig
));
128 for (int i
= 0; i
< GetSize(sig
); i
++)
129 bit_nid
[sig
[i
]] = make_pair(nid
, i
);
132 nid_width
[nid
] = GetSize(sig
);
135 void export_cell(Cell
*cell
)
137 if (cell_recursion_guard
.count(cell
)) {
139 for (auto c
: cell_recursion_guard
)
140 cell_list
+= stringf("\n %s", log_id(c
));
141 log_error("Found topological loop while processing cell %s. Active cells:%s\n", log_id(cell
), cell_list
.c_str());
144 cell_recursion_guard
.insert(cell
);
145 btorf_push(log_id(cell
));
147 if (cell
->type
.in("$add", "$sub", "$mul", "$and", "$or", "$xor", "$xnor", "$shl", "$sshl", "$shr", "$sshr", "$shift", "$shiftx",
148 "$concat", "$_AND_", "$_NAND_", "$_OR_", "$_NOR_", "$_XOR_", "$_XNOR_"))
151 if (cell
->type
== "$add") btor_op
= "add";
152 if (cell
->type
== "$sub") btor_op
= "sub";
153 if (cell
->type
== "$mul") btor_op
= "mul";
154 if (cell
->type
.in("$shl", "$sshl")) btor_op
= "sll";
155 if (cell
->type
== "$shr") btor_op
= "srl";
156 if (cell
->type
== "$sshr") btor_op
= "sra";
157 if (cell
->type
.in("$shift", "$shiftx")) btor_op
= "shift";
158 if (cell
->type
.in("$and", "$_AND_")) btor_op
= "and";
159 if (cell
->type
.in("$or", "$_OR_")) btor_op
= "or";
160 if (cell
->type
.in("$xor", "$_XOR_")) btor_op
= "xor";
161 if (cell
->type
== "$concat") btor_op
= "concat";
162 if (cell
->type
== "$_NAND_") btor_op
= "nand";
163 if (cell
->type
== "$_NOR_") btor_op
= "nor";
164 if (cell
->type
.in("$xnor", "$_XNOR_")) btor_op
= "xnor";
165 log_assert(!btor_op
.empty());
167 int width
= GetSize(cell
->getPort("\\Y"));
168 width
= std::max(width
, GetSize(cell
->getPort("\\A")));
169 width
= std::max(width
, GetSize(cell
->getPort("\\B")));
171 bool a_signed
= cell
->hasParam("\\A_SIGNED") ? cell
->getParam("\\A_SIGNED").as_bool() : false;
172 bool b_signed
= cell
->hasParam("\\B_SIGNED") ? cell
->getParam("\\B_SIGNED").as_bool() : false;
174 if (btor_op
== "shift" && !b_signed
)
177 if (cell
->type
.in("$shl", "$sshl", "$shr", "$sshr"))
180 if (cell
->type
== "$sshr" && !a_signed
)
183 int sid
= get_bv_sid(width
);
186 if (btor_op
== "shift")
188 int nid_a
= get_sig_nid(cell
->getPort("\\A"), width
, false);
189 int nid_b
= get_sig_nid(cell
->getPort("\\B"), width
, b_signed
);
191 int nid_r
= next_nid
++;
192 btorf("%d srl %d %d %d\n", nid_r
, sid
, nid_a
, nid_b
);
194 int nid_b_neg
= next_nid
++;
195 btorf("%d neg %d %d\n", nid_b_neg
, sid
, nid_b
);
197 int nid_l
= next_nid
++;
198 btorf("%d sll %d %d %d\n", nid_l
, sid
, nid_a
, nid_b_neg
);
200 int sid_bit
= get_bv_sid(1);
201 int nid_zero
= get_sig_nid(Const(0, width
));
202 int nid_b_ltz
= next_nid
++;
203 btorf("%d slt %d %d %d\n", nid_b_ltz
, sid_bit
, nid_b
, nid_zero
);
206 btorf("%d ite %d %d %d %d\n", nid
, sid
, nid_b_ltz
, nid_l
, nid_r
);
210 int nid_a
= get_sig_nid(cell
->getPort("\\A"), width
, a_signed
);
211 int nid_b
= get_sig_nid(cell
->getPort("\\B"), width
, b_signed
);
214 btorf("%d %s %d %d %d\n", nid
, btor_op
.c_str(), sid
, nid_a
, nid_b
);
217 SigSpec sig
= sigmap(cell
->getPort("\\Y"));
219 if (GetSize(sig
) < width
) {
220 int sid
= get_bv_sid(GetSize(sig
));
221 int nid2
= next_nid
++;
222 btorf("%d slice %d %d %d 0\n", nid2
, sid
, nid
, GetSize(sig
)-1);
226 add_nid_sig(nid
, sig
);
230 if (cell
->type
.in("$div", "$mod"))
233 if (cell
->type
== "$div") btor_op
= "div";
234 if (cell
->type
== "$mod") btor_op
= "rem";
235 log_assert(!btor_op
.empty());
237 int width
= GetSize(cell
->getPort("\\Y"));
238 width
= std::max(width
, GetSize(cell
->getPort("\\A")));
239 width
= std::max(width
, GetSize(cell
->getPort("\\B")));
241 bool a_signed
= cell
->hasParam("\\A_SIGNED") ? cell
->getParam("\\A_SIGNED").as_bool() : false;
242 bool b_signed
= cell
->hasParam("\\B_SIGNED") ? cell
->getParam("\\B_SIGNED").as_bool() : false;
244 int nid_a
= get_sig_nid(cell
->getPort("\\A"), width
, a_signed
);
245 int nid_b
= get_sig_nid(cell
->getPort("\\B"), width
, b_signed
);
247 int sid
= get_bv_sid(width
);
248 int nid
= next_nid
++;
249 btorf("%d %c%s %d %d %d\n", nid
, a_signed
|| b_signed
? 's' : 'u', btor_op
.c_str(), sid
, nid_a
, nid_b
);
251 SigSpec sig
= sigmap(cell
->getPort("\\Y"));
253 if (GetSize(sig
) < width
) {
254 int sid
= get_bv_sid(GetSize(sig
));
255 int nid2
= next_nid
++;
256 btorf("%d slice %d %d %d 0\n", nid2
, sid
, nid
, GetSize(sig
)-1);
260 add_nid_sig(nid
, sig
);
264 if (cell
->type
.in("$_ANDNOT_", "$_ORNOT_"))
266 int sid
= get_bv_sid(1);
267 int nid_a
= get_sig_nid(cell
->getPort("\\A"));
268 int nid_b
= get_sig_nid(cell
->getPort("\\B"));
270 int nid1
= next_nid
++;
271 int nid2
= next_nid
++;
273 if (cell
->type
== "$_ANDNOT_") {
274 btorf("%d not %d %d\n", nid1
, sid
, nid_b
);
275 btorf("%d and %d %d %d\n", nid2
, sid
, nid_a
, nid1
);
278 if (cell
->type
== "$_ORNOT_") {
279 btorf("%d not %d %d\n", nid1
, sid
, nid_b
);
280 btorf("%d or %d %d %d\n", nid2
, sid
, nid_a
, nid1
);
283 SigSpec sig
= sigmap(cell
->getPort("\\Y"));
284 add_nid_sig(nid2
, sig
);
288 if (cell
->type
.in("$_OAI3_", "$_AOI3_"))
290 int sid
= get_bv_sid(1);
291 int nid_a
= get_sig_nid(cell
->getPort("\\A"));
292 int nid_b
= get_sig_nid(cell
->getPort("\\B"));
293 int nid_c
= get_sig_nid(cell
->getPort("\\C"));
295 int nid1
= next_nid
++;
296 int nid2
= next_nid
++;
297 int nid3
= next_nid
++;
299 if (cell
->type
== "$_OAI3_") {
300 btorf("%d or %d %d %d\n", nid1
, sid
, nid_a
, nid_b
);
301 btorf("%d and %d %d %d\n", nid2
, sid
, nid1
, nid_c
);
302 btorf("%d not %d %d\n", nid3
, sid
, nid2
);
305 if (cell
->type
== "$_AOI3_") {
306 btorf("%d and %d %d %d\n", nid1
, sid
, nid_a
, nid_b
);
307 btorf("%d or %d %d %d\n", nid2
, sid
, nid1
, nid_c
);
308 btorf("%d not %d %d\n", nid3
, sid
, nid2
);
311 SigSpec sig
= sigmap(cell
->getPort("\\Y"));
312 add_nid_sig(nid3
, sig
);
316 if (cell
->type
.in("$_OAI4_", "$_AOI4_"))
318 int sid
= get_bv_sid(1);
319 int nid_a
= get_sig_nid(cell
->getPort("\\A"));
320 int nid_b
= get_sig_nid(cell
->getPort("\\B"));
321 int nid_c
= get_sig_nid(cell
->getPort("\\C"));
322 int nid_d
= get_sig_nid(cell
->getPort("\\D"));
324 int nid1
= next_nid
++;
325 int nid2
= next_nid
++;
326 int nid3
= next_nid
++;
327 int nid4
= next_nid
++;
329 if (cell
->type
== "$_OAI4_") {
330 btorf("%d or %d %d %d\n", nid1
, sid
, nid_a
, nid_b
);
331 btorf("%d or %d %d %d\n", nid2
, sid
, nid_c
, nid_d
);
332 btorf("%d and %d %d %d\n", nid3
, sid
, nid1
, nid2
);
333 btorf("%d not %d %d\n", nid4
, sid
, nid3
);
336 if (cell
->type
== "$_AOI4_") {
337 btorf("%d and %d %d %d\n", nid1
, sid
, nid_a
, nid_b
);
338 btorf("%d and %d %d %d\n", nid2
, sid
, nid_c
, nid_d
);
339 btorf("%d or %d %d %d\n", nid3
, sid
, nid1
, nid2
);
340 btorf("%d not %d %d\n", nid4
, sid
, nid3
);
343 SigSpec sig
= sigmap(cell
->getPort("\\Y"));
344 add_nid_sig(nid4
, sig
);
348 if (cell
->type
.in("$lt", "$le", "$eq", "$eqx", "$ne", "$nex", "$ge", "$gt"))
351 if (cell
->type
== "$lt") btor_op
= "lt";
352 if (cell
->type
== "$le") btor_op
= "lte";
353 if (cell
->type
.in("$eq", "$eqx")) btor_op
= "eq";
354 if (cell
->type
.in("$ne", "$nex")) btor_op
= "neq";
355 if (cell
->type
== "$ge") btor_op
= "gte";
356 if (cell
->type
== "$gt") btor_op
= "gt";
357 log_assert(!btor_op
.empty());
360 width
= std::max(width
, GetSize(cell
->getPort("\\A")));
361 width
= std::max(width
, GetSize(cell
->getPort("\\B")));
363 bool a_signed
= cell
->hasParam("\\A_SIGNED") ? cell
->getParam("\\A_SIGNED").as_bool() : false;
364 bool b_signed
= cell
->hasParam("\\B_SIGNED") ? cell
->getParam("\\B_SIGNED").as_bool() : false;
366 int sid
= get_bv_sid(1);
367 int nid_a
= get_sig_nid(cell
->getPort("\\A"), width
, a_signed
);
368 int nid_b
= get_sig_nid(cell
->getPort("\\B"), width
, b_signed
);
370 int nid
= next_nid
++;
371 if (cell
->type
.in("$lt", "$le", "$ge", "$gt")) {
372 btorf("%d %c%s %d %d %d\n", nid
, a_signed
|| b_signed
? 's' : 'u', btor_op
.c_str(), sid
, nid_a
, nid_b
);
374 btorf("%d %s %d %d %d\n", nid
, btor_op
.c_str(), sid
, nid_a
, nid_b
);
377 SigSpec sig
= sigmap(cell
->getPort("\\Y"));
379 if (GetSize(sig
) > 1) {
380 int sid
= get_bv_sid(GetSize(sig
));
381 int nid2
= next_nid
++;
382 btorf("%d uext %d %d %d\n", nid2
, sid
, nid
, GetSize(sig
) - 1);
386 add_nid_sig(nid
, sig
);
390 if (cell
->type
.in("$not", "$neg", "$_NOT_"))
393 if (cell
->type
.in("$not", "$_NOT_")) btor_op
= "not";
394 if (cell
->type
== "$neg") btor_op
= "neg";
395 log_assert(!btor_op
.empty());
397 int width
= GetSize(cell
->getPort("\\Y"));
398 width
= std::max(width
, GetSize(cell
->getPort("\\A")));
400 bool a_signed
= cell
->hasParam("\\A_SIGNED") ? cell
->getParam("\\A_SIGNED").as_bool() : false;
402 int sid
= get_bv_sid(width
);
403 int nid_a
= get_sig_nid(cell
->getPort("\\A"), width
, a_signed
);
405 int nid
= next_nid
++;
406 btorf("%d %s %d %d\n", nid
, btor_op
.c_str(), sid
, nid_a
);
408 SigSpec sig
= sigmap(cell
->getPort("\\Y"));
410 if (GetSize(sig
) < width
) {
411 int sid
= get_bv_sid(GetSize(sig
));
412 int nid2
= next_nid
++;
413 btorf("%d slice %d %d %d 0\n", nid2
, sid
, nid
, GetSize(sig
)-1);
417 add_nid_sig(nid
, sig
);
421 if (cell
->type
.in("$logic_and", "$logic_or", "$logic_not"))
424 if (cell
->type
== "$logic_and") btor_op
= "and";
425 if (cell
->type
== "$logic_or") btor_op
= "or";
426 if (cell
->type
== "$logic_not") btor_op
= "not";
427 log_assert(!btor_op
.empty());
429 int sid
= get_bv_sid(1);
430 int nid_a
= get_sig_nid(cell
->getPort("\\A"));
431 int nid_b
= btor_op
!= "not" ? get_sig_nid(cell
->getPort("\\B")) : 0;
433 if (GetSize(cell
->getPort("\\A")) > 1) {
434 int nid_red_a
= next_nid
++;
435 btorf("%d redor %d %d\n", nid_red_a
, sid
, nid_a
);
439 if (btor_op
!= "not" && GetSize(cell
->getPort("\\B")) > 1) {
440 int nid_red_b
= next_nid
++;
441 btorf("%d redor %d %d\n", nid_red_b
, sid
, nid_b
);
445 int nid
= next_nid
++;
446 if (btor_op
!= "not")
447 btorf("%d %s %d %d %d\n", nid
, btor_op
.c_str(), sid
, nid_a
, nid_b
);
449 btorf("%d %s %d %d\n", nid
, btor_op
.c_str(), sid
, nid_a
);
451 SigSpec sig
= sigmap(cell
->getPort("\\Y"));
453 if (GetSize(sig
) > 1) {
454 int sid
= get_bv_sid(GetSize(sig
));
455 int zeros_nid
= get_sig_nid(Const(0, GetSize(sig
)-1));
456 int nid2
= next_nid
++;
457 btorf("%d concat %d %d %d\n", nid2
, sid
, zeros_nid
, nid
);
461 add_nid_sig(nid
, sig
);
465 if (cell
->type
.in("$reduce_and", "$reduce_or", "$reduce_bool", "$reduce_xor", "$reduce_xnor"))
468 if (cell
->type
== "$reduce_and") btor_op
= "redand";
469 if (cell
->type
.in("$reduce_or", "$reduce_bool")) btor_op
= "redor";
470 if (cell
->type
.in("$reduce_xor", "$reduce_xnor")) btor_op
= "redxor";
471 log_assert(!btor_op
.empty());
473 int sid
= get_bv_sid(1);
474 int nid_a
= get_sig_nid(cell
->getPort("\\A"));
476 int nid
= next_nid
++;
477 btorf("%d %s %d %d\n", nid
, btor_op
.c_str(), sid
, nid_a
);
479 if (cell
->type
== "$reduce_xnor") {
480 int nid2
= next_nid
++;
481 btorf("%d not %d %d %d\n", nid2
, sid
, nid
);
485 SigSpec sig
= sigmap(cell
->getPort("\\Y"));
487 if (GetSize(sig
) > 1) {
488 int sid
= get_bv_sid(GetSize(sig
));
489 int zeros_nid
= get_sig_nid(Const(0, GetSize(sig
)-1));
490 int nid2
= next_nid
++;
491 btorf("%d concat %d %d %d\n", nid2
, sid
, zeros_nid
, nid
);
495 add_nid_sig(nid
, sig
);
499 if (cell
->type
.in("$mux", "$_MUX_", "$_NMUX_"))
501 SigSpec sig_a
= sigmap(cell
->getPort("\\A"));
502 SigSpec sig_b
= sigmap(cell
->getPort("\\B"));
503 SigSpec sig_s
= sigmap(cell
->getPort("\\S"));
504 SigSpec sig_y
= sigmap(cell
->getPort("\\Y"));
506 int nid_a
= get_sig_nid(sig_a
);
507 int nid_b
= get_sig_nid(sig_b
);
508 int nid_s
= get_sig_nid(sig_s
);
510 int sid
= get_bv_sid(GetSize(sig_y
));
511 int nid
= next_nid
++;
512 btorf("%d ite %d %d %d %d\n", nid
, sid
, nid_s
, nid_b
, nid_a
);
514 if (cell
->type
== "$_NMUX_") {
517 btorf("%d not %d %d\n", nid
, sid
, tmp
);
520 add_nid_sig(nid
, sig_y
);
524 if (cell
->type
== "$pmux")
526 SigSpec sig_a
= sigmap(cell
->getPort("\\A"));
527 SigSpec sig_b
= sigmap(cell
->getPort("\\B"));
528 SigSpec sig_s
= sigmap(cell
->getPort("\\S"));
529 SigSpec sig_y
= sigmap(cell
->getPort("\\Y"));
531 int width
= GetSize(sig_a
);
532 int sid
= get_bv_sid(width
);
533 int nid
= get_sig_nid(sig_a
);
535 for (int i
= 0; i
< GetSize(sig_s
); i
++) {
536 int nid_b
= get_sig_nid(sig_b
.extract(i
*width
, width
));
537 int nid_s
= get_sig_nid(sig_s
.extract(i
));
538 int nid2
= next_nid
++;
539 btorf("%d ite %d %d %d %d\n", nid2
, sid
, nid_s
, nid_b
, nid
);
543 add_nid_sig(nid
, sig_y
);
547 if (cell
->type
.in("$dff", "$ff", "$_DFF_P_", "$_DFF_N", "$_FF_"))
549 SigSpec sig_d
= sigmap(cell
->getPort("\\D"));
550 SigSpec sig_q
= sigmap(cell
->getPort("\\Q"));
554 if (sig_q
.is_wire()) {
555 Wire
*w
= sig_q
.as_wire();
556 if (w
->port_id
== 0) {
557 statewires
.insert(w
);
563 for (int i
= 0; i
< GetSize(sig_q
); i
++)
564 if (initbits
.count(sig_q
[i
]))
565 initval
.bits
.push_back(initbits
.at(sig_q
[i
]) ? State::S1
: State::S0
);
567 initval
.bits
.push_back(State::Sx
);
569 int nid_init_val
= -1;
571 if (!initval
.is_fully_undef())
572 nid_init_val
= get_sig_nid(initval
, -1, false, true);
574 int sid
= get_bv_sid(GetSize(sig_q
));
575 int nid
= next_nid
++;
578 btorf("%d state %d\n", nid
, sid
);
580 btorf("%d state %d %s\n", nid
, sid
, log_id(symbol
));
582 if (nid_init_val
>= 0) {
583 int nid_init
= next_nid
++;
585 btorf("; initval = %s\n", log_signal(initval
));
586 btorf("%d init %d %d %d\n", nid_init
, sid
, nid
, nid_init_val
);
589 ff_todo
.push_back(make_pair(nid
, cell
));
590 add_nid_sig(nid
, sig_q
);
594 if (cell
->type
.in("$anyconst", "$anyseq"))
596 SigSpec sig_y
= sigmap(cell
->getPort("\\Y"));
598 int sid
= get_bv_sid(GetSize(sig_y
));
599 int nid
= next_nid
++;
601 btorf("%d state %d\n", nid
, sid
);
603 if (cell
->type
== "$anyconst") {
604 int nid2
= next_nid
++;
605 btorf("%d next %d %d %d\n", nid2
, sid
, nid
, nid
);
608 add_nid_sig(nid
, sig_y
);
612 if (cell
->type
== "$initstate")
614 SigSpec sig_y
= sigmap(cell
->getPort("\\Y"));
616 if (initstate_nid
< 0)
618 int sid
= get_bv_sid(1);
619 int one_nid
= get_sig_nid(State::S1
);
620 int zero_nid
= get_sig_nid(State::S0
);
621 initstate_nid
= next_nid
++;
622 btorf("%d state %d\n", initstate_nid
, sid
);
623 btorf("%d init %d %d %d\n", next_nid
++, sid
, initstate_nid
, one_nid
);
624 btorf("%d next %d %d %d\n", next_nid
++, sid
, initstate_nid
, zero_nid
);
627 add_nid_sig(initstate_nid
, sig_y
);
631 if (cell
->type
== "$mem")
633 int abits
= cell
->getParam("\\ABITS").as_int();
634 int width
= cell
->getParam("\\WIDTH").as_int();
635 int nwords
= cell
->getParam("\\SIZE").as_int();
636 int rdports
= cell
->getParam("\\RD_PORTS").as_int();
637 int wrports
= cell
->getParam("\\WR_PORTS").as_int();
639 Const wr_clk_en
= cell
->getParam("\\WR_CLK_ENABLE");
640 Const rd_clk_en
= cell
->getParam("\\RD_CLK_ENABLE");
642 bool asyncwr
= wr_clk_en
.is_fully_zero();
644 if (!asyncwr
&& !wr_clk_en
.is_fully_ones())
645 log_error("Memory %s.%s has mixed async/sync write ports.\n",
646 log_id(module
), log_id(cell
));
648 if (!rd_clk_en
.is_fully_zero())
649 log_error("Memory %s.%s has sync read ports.\n",
650 log_id(module
), log_id(cell
));
652 SigSpec sig_rd_addr
= sigmap(cell
->getPort("\\RD_ADDR"));
653 SigSpec sig_rd_data
= sigmap(cell
->getPort("\\RD_DATA"));
655 SigSpec sig_wr_addr
= sigmap(cell
->getPort("\\WR_ADDR"));
656 SigSpec sig_wr_data
= sigmap(cell
->getPort("\\WR_DATA"));
657 SigSpec sig_wr_en
= sigmap(cell
->getPort("\\WR_EN"));
659 int data_sid
= get_bv_sid(width
);
660 int bool_sid
= get_bv_sid(1);
661 int sid
= get_mem_sid(abits
, width
);
663 Const initdata
= cell
->getParam("\\INIT");
664 initdata
.exts(nwords
*width
);
665 int nid_init_val
= -1;
667 if (!initdata
.is_fully_undef())
669 bool constword
= true;
670 Const firstword
= initdata
.extract(0, width
);
672 for (int i
= 1; i
< nwords
; i
++) {
673 Const thisword
= initdata
.extract(i
*width
, width
);
674 if (thisword
!= firstword
) {
683 btorf("; initval = %s\n", log_signal(firstword
));
684 nid_init_val
= get_sig_nid(firstword
, -1, false, true);
688 nid_init_val
= next_nid
++;
689 btorf("%d state %d\n", nid_init_val
, sid
);
691 for (int i
= 0; i
< nwords
; i
++) {
692 Const thisword
= initdata
.extract(i
*width
, width
);
693 if (thisword
.is_fully_undef())
695 Const
thisaddr(i
, abits
);
696 int nid_thisword
= get_sig_nid(thisword
, -1, false, true);
697 int nid_thisaddr
= get_sig_nid(thisaddr
, -1, false, true);
698 int last_nid_init_val
= nid_init_val
;
699 nid_init_val
= next_nid
++;
701 btorf("; initval[%d] = %s\n", i
, log_signal(thisword
));
702 btorf("%d write %d %d %d %d\n", nid_init_val
, sid
, last_nid_init_val
, nid_thisaddr
, nid_thisword
);
708 int nid
= next_nid
++;
711 if (cell
->name
[0] == '$')
712 btorf("%d state %d\n", nid
, sid
);
714 btorf("%d state %d %s\n", nid
, sid
, log_id(cell
));
716 if (nid_init_val
>= 0)
718 int nid_init
= next_nid
++;
719 btorf("%d init %d %d %d\n", nid_init
, sid
, nid
, nid_init_val
);
724 for (int port
= 0; port
< wrports
; port
++)
726 SigSpec wa
= sig_wr_addr
.extract(port
*abits
, abits
);
727 SigSpec wd
= sig_wr_data
.extract(port
*width
, width
);
728 SigSpec we
= sig_wr_en
.extract(port
*width
, width
);
730 int wa_nid
= get_sig_nid(wa
);
731 int wd_nid
= get_sig_nid(wd
);
732 int we_nid
= get_sig_nid(we
);
734 int nid2
= next_nid
++;
735 btorf("%d read %d %d %d\n", nid2
, data_sid
, nid_head
, wa_nid
);
737 int nid3
= next_nid
++;
738 btorf("%d not %d %d\n", nid3
, data_sid
, we_nid
);
740 int nid4
= next_nid
++;
741 btorf("%d and %d %d %d\n", nid4
, data_sid
, nid2
, nid3
);
743 int nid5
= next_nid
++;
744 btorf("%d and %d %d %d\n", nid5
, data_sid
, wd_nid
, we_nid
);
746 int nid6
= next_nid
++;
747 btorf("%d or %d %d %d\n", nid6
, data_sid
, nid5
, nid4
);
749 int nid7
= next_nid
++;
750 btorf("%d write %d %d %d %d\n", nid7
, sid
, nid_head
, wa_nid
, nid6
);
752 int nid8
= next_nid
++;
753 btorf("%d redor %d %d\n", nid8
, bool_sid
, we_nid
);
755 int nid9
= next_nid
++;
756 btorf("%d ite %d %d %d %d\n", nid9
, sid
, nid8
, nid7
, nid_head
);
762 for (int port
= 0; port
< rdports
; port
++)
764 SigSpec ra
= sig_rd_addr
.extract(port
*abits
, abits
);
765 SigSpec rd
= sig_rd_data
.extract(port
*width
, width
);
767 int ra_nid
= get_sig_nid(ra
);
768 int rd_nid
= next_nid
++;
770 btorf("%d read %d %d %d\n", rd_nid
, data_sid
, nid_head
, ra_nid
);
772 add_nid_sig(rd_nid
, rd
);
777 ff_todo
.push_back(make_pair(nid
, cell
));
781 int nid2
= next_nid
++;
782 btorf("%d next %d %d %d\n", nid2
, sid
, nid
, nid_head
);
788 log_error("Unsupported cell type: %s (%s)\n", log_id(cell
->type
), log_id(cell
));
791 btorf_pop(log_id(cell
));
792 cell_recursion_guard
.erase(cell
);
795 int get_sig_nid(SigSpec sig
, int to_width
= -1, bool is_signed
= false, bool is_init
= false)
801 if (bit
== State::Sx
)
807 SigSpec sig_mask_undef
, sig_noundef
;
808 int first_undef
= -1;
810 for (int i
= 0; i
< GetSize(sig
); i
++)
811 if (sig
[i
] == State::Sx
) {
814 sig_mask_undef
.append(State::S1
);
815 sig_noundef
.append(State::S0
);
817 sig_mask_undef
.append(State::S0
);
818 sig_noundef
.append(sig
[i
]);
821 if (to_width
< 0 || first_undef
< to_width
)
823 int sid
= get_bv_sid(GetSize(sig
));
825 int nid_input
= next_nid
++;
827 btorf("%d state %d\n", nid_input
, sid
);
829 btorf("%d input %d\n", nid_input
, sid
);
831 int nid_masked_input
;
832 if (sig_mask_undef
.is_fully_ones()) {
833 nid_masked_input
= nid_input
;
835 int nid_mask_undef
= get_sig_nid(sig_mask_undef
);
836 nid_masked_input
= next_nid
++;
837 btorf("%d and %d %d %d\n", nid_masked_input
, sid
, nid_input
, nid_mask_undef
);
840 if (sig_noundef
.is_fully_zero()) {
841 nid
= nid_masked_input
;
843 int nid_noundef
= get_sig_nid(sig_noundef
);
845 btorf("%d or %d %d %d\n", nid
, sid
, nid_masked_input
, nid_noundef
);
854 if (sig_nid
.count(sig
) == 0)
857 vector
<pair
<int, int>> nidbits
;
860 for (int i
= 0; i
< GetSize(sig
); i
++)
864 if (bit_nid
.count(bit
) == 0)
866 if (bit
.wire
== nullptr)
870 while (i
+GetSize(c
) < GetSize(sig
) && sig
[i
+GetSize(c
)].wire
== nullptr)
871 c
.bits
.push_back(sig
[i
+GetSize(c
)].data
);
873 if (consts
.count(c
) == 0) {
874 int sid
= get_bv_sid(GetSize(c
));
875 int nid
= next_nid
++;
876 btorf("%d const %d %s\n", nid
, sid
, c
.as_string().c_str());
878 nid_width
[nid
] = GetSize(c
);
881 int nid
= consts
.at(c
);
883 for (int j
= 0; j
< GetSize(c
); j
++)
884 nidbits
.push_back(make_pair(nid
, j
));
891 if (bit_cell
.count(bit
) == 0)
895 while (i
+GetSize(s
) < GetSize(sig
) && sig
[i
+GetSize(s
)].wire
!= nullptr &&
896 bit_cell
.count(sig
[i
+GetSize(s
)]) == 0)
897 s
.append(sig
[i
+GetSize(s
)]);
899 log_warning("No driver for signal %s.\n", log_signal(s
));
901 int sid
= get_bv_sid(GetSize(s
));
902 int nid
= next_nid
++;
903 btorf("%d input %d\n", nid
, sid
);
904 nid_width
[nid
] = GetSize(s
);
906 for (int j
= 0; j
< GetSize(s
); j
++)
907 nidbits
.push_back(make_pair(nid
, j
));
914 export_cell(bit_cell
.at(bit
));
915 log_assert(bit_nid
.count(bit
));
920 nidbits
.push_back(bit_nid
.at(bit
));
926 // group bits and emit slice-concat chain
927 for (int i
= 0; i
< GetSize(nidbits
); i
++)
929 int nid2
= nidbits
[i
].first
;
930 int lower
= nidbits
[i
].second
;
933 while (i
+1 < GetSize(nidbits
) && nidbits
[i
+1].first
== nidbits
[i
].first
&&
934 nidbits
[i
+1].second
== nidbits
[i
].second
+1)
939 if (lower
!= 0 || upper
+1 != nid_width
.at(nid2
)) {
940 int sid
= get_bv_sid(upper
-lower
+1);
942 btorf("%d slice %d %d %d %d\n", nid3
, sid
, nid2
, upper
, lower
);
948 int sid
= get_bv_sid(width
+upper
-lower
+1);
950 btorf("%d concat %d %d %d\n", nid4
, sid
, nid3
, nid
);
953 width
+= upper
-lower
+1;
958 nid_width
[nid
] = width
;
961 nid
= sig_nid
.at(sig
);
964 if (to_width
>= 0 && to_width
!= GetSize(sig
))
966 if (to_width
< GetSize(sig
))
968 int sid
= get_bv_sid(to_width
);
969 int nid2
= next_nid
++;
970 btorf("%d slice %d %d %d 0\n", nid2
, sid
, nid
, to_width
-1);
975 int sid
= get_bv_sid(to_width
);
976 int nid2
= next_nid
++;
977 btorf("%d %s %d %d %d\n", nid2
, is_signed
? "sext" : "uext",
978 sid
, nid
, to_width
- GetSize(sig
));
986 BtorWorker(std::ostream
&f
, RTLIL::Module
*module
, bool verbose
, bool single_bad
) :
987 f(f
), sigmap(module
), module(module
), verbose(verbose
), single_bad(single_bad
)
989 btorf_push("inputs");
991 for (auto wire
: module
->wires())
993 if (wire
->attributes
.count("\\init")) {
994 Const attrval
= wire
->attributes
.at("\\init");
995 for (int i
= 0; i
< GetSize(wire
) && i
< GetSize(attrval
); i
++)
996 if (attrval
[i
] == State::S0
|| attrval
[i
] == State::S1
)
997 initbits
[sigmap(SigBit(wire
, i
))] = (attrval
[i
] == State::S1
);
1000 if (!wire
->port_id
|| !wire
->port_input
)
1003 SigSpec sig
= sigmap(wire
);
1004 int sid
= get_bv_sid(GetSize(sig
));
1005 int nid
= next_nid
++;
1007 btorf("%d input %d %s\n", nid
, sid
, log_id(wire
));
1008 add_nid_sig(nid
, sig
);
1011 btorf_pop("inputs");
1013 for (auto cell
: module
->cells())
1014 for (auto &conn
: cell
->connections())
1016 if (!cell
->output(conn
.first
))
1019 for (auto bit
: sigmap(conn
.second
))
1020 bit_cell
[bit
] = cell
;
1023 for (auto wire
: module
->wires())
1025 if (!wire
->port_id
|| !wire
->port_output
)
1028 btorf_push(stringf("output %s", log_id(wire
)));
1030 int nid
= get_sig_nid(wire
);
1031 btorf("%d output %d %s\n", next_nid
++, nid
, log_id(wire
));
1033 btorf_pop(stringf("output %s", log_id(wire
)));
1036 for (auto cell
: module
->cells())
1038 if (cell
->type
== "$assume")
1040 btorf_push(log_id(cell
));
1042 int sid
= get_bv_sid(1);
1043 int nid_a
= get_sig_nid(cell
->getPort("\\A"));
1044 int nid_en
= get_sig_nid(cell
->getPort("\\EN"));
1045 int nid_not_en
= next_nid
++;
1046 int nid_a_or_not_en
= next_nid
++;
1047 int nid
= next_nid
++;
1049 btorf("%d not %d %d\n", nid_not_en
, sid
, nid_en
);
1050 btorf("%d or %d %d %d\n", nid_a_or_not_en
, sid
, nid_a
, nid_not_en
);
1051 btorf("%d constraint %d\n", nid
, nid_a_or_not_en
);
1053 btorf_pop(log_id(cell
));
1056 if (cell
->type
== "$assert")
1058 btorf_push(log_id(cell
));
1060 int sid
= get_bv_sid(1);
1061 int nid_a
= get_sig_nid(cell
->getPort("\\A"));
1062 int nid_en
= get_sig_nid(cell
->getPort("\\EN"));
1063 int nid_not_a
= next_nid
++;
1064 int nid_en_and_not_a
= next_nid
++;
1066 btorf("%d not %d %d\n", nid_not_a
, sid
, nid_a
);
1067 btorf("%d and %d %d %d\n", nid_en_and_not_a
, sid
, nid_en
, nid_not_a
);
1070 bad_properties
.push_back(nid_en_and_not_a
);
1072 int nid
= next_nid
++;
1073 string infostr
= log_id(cell
);
1074 if (infostr
[0] == '$' && cell
->attributes
.count("\\src")) {
1075 infostr
= cell
->attributes
.at("\\src").decode_string().c_str();
1076 std::replace(infostr
.begin(), infostr
.end(), ' ', '_');
1078 btorf("%d bad %d %s\n", nid
, nid_en_and_not_a
, infostr
.c_str());
1081 btorf_pop(log_id(cell
));
1085 for (auto wire
: module
->wires())
1087 if (wire
->port_id
|| wire
->name
[0] == '$')
1090 btorf_push(stringf("wire %s", log_id(wire
)));
1092 int sid
= get_bv_sid(GetSize(wire
));
1093 int nid
= get_sig_nid(sigmap(wire
));
1095 if (statewires
.count(wire
))
1098 int this_nid
= next_nid
++;
1099 btorf("%d uext %d %d %d %s\n", this_nid
, sid
, nid
, 0, log_id(wire
));
1101 btorf_pop(stringf("wire %s", log_id(wire
)));
1105 while (!ff_todo
.empty())
1107 vector
<pair
<int, Cell
*>> todo
;
1110 for (auto &it
: todo
)
1113 Cell
*cell
= it
.second
;
1115 btorf_push(stringf("next %s", log_id(cell
)));
1117 if (cell
->type
== "$mem")
1119 int abits
= cell
->getParam("\\ABITS").as_int();
1120 int width
= cell
->getParam("\\WIDTH").as_int();
1121 int wrports
= cell
->getParam("\\WR_PORTS").as_int();
1123 SigSpec sig_wr_addr
= sigmap(cell
->getPort("\\WR_ADDR"));
1124 SigSpec sig_wr_data
= sigmap(cell
->getPort("\\WR_DATA"));
1125 SigSpec sig_wr_en
= sigmap(cell
->getPort("\\WR_EN"));
1127 int data_sid
= get_bv_sid(width
);
1128 int bool_sid
= get_bv_sid(1);
1129 int sid
= get_mem_sid(abits
, width
);
1132 for (int port
= 0; port
< wrports
; port
++)
1134 SigSpec wa
= sig_wr_addr
.extract(port
*abits
, abits
);
1135 SigSpec wd
= sig_wr_data
.extract(port
*width
, width
);
1136 SigSpec we
= sig_wr_en
.extract(port
*width
, width
);
1138 int wa_nid
= get_sig_nid(wa
);
1139 int wd_nid
= get_sig_nid(wd
);
1140 int we_nid
= get_sig_nid(we
);
1142 int nid2
= next_nid
++;
1143 btorf("%d read %d %d %d\n", nid2
, data_sid
, nid_head
, wa_nid
);
1145 int nid3
= next_nid
++;
1146 btorf("%d not %d %d\n", nid3
, data_sid
, we_nid
);
1148 int nid4
= next_nid
++;
1149 btorf("%d and %d %d %d\n", nid4
, data_sid
, nid2
, nid3
);
1151 int nid5
= next_nid
++;
1152 btorf("%d and %d %d %d\n", nid5
, data_sid
, wd_nid
, we_nid
);
1154 int nid6
= next_nid
++;
1155 btorf("%d or %d %d %d\n", nid6
, data_sid
, nid5
, nid4
);
1157 int nid7
= next_nid
++;
1158 btorf("%d write %d %d %d %d\n", nid7
, sid
, nid_head
, wa_nid
, nid6
);
1160 int nid8
= next_nid
++;
1161 btorf("%d redor %d %d\n", nid8
, bool_sid
, we_nid
);
1163 int nid9
= next_nid
++;
1164 btorf("%d ite %d %d %d %d\n", nid9
, sid
, nid8
, nid7
, nid_head
);
1169 int nid2
= next_nid
++;
1170 btorf("%d next %d %d %d\n", nid2
, sid
, nid
, nid_head
);
1174 SigSpec sig
= sigmap(cell
->getPort("\\D"));
1175 int nid_q
= get_sig_nid(sig
);
1176 int sid
= get_bv_sid(GetSize(sig
));
1177 btorf("%d next %d %d %d\n", next_nid
++, sid
, nid
, nid_q
);
1180 btorf_pop(stringf("next %s", log_id(cell
)));
1184 while (!bad_properties
.empty())
1187 bad_properties
.swap(todo
);
1189 int sid
= get_bv_sid(1);
1192 while (cursor
+1 < GetSize(todo
))
1194 int nid_a
= todo
[cursor
++];
1195 int nid_b
= todo
[cursor
++];
1196 int nid
= next_nid
++;
1198 bad_properties
.push_back(nid
);
1199 btorf("%d or %d %d %d\n", nid
, sid
, nid_a
, nid_b
);
1202 if (!bad_properties
.empty()) {
1203 if (cursor
< GetSize(todo
))
1204 bad_properties
.push_back(todo
[cursor
++]);
1205 log_assert(cursor
== GetSize(todo
));
1207 int nid
= next_nid
++;
1208 log_assert(cursor
== 0);
1209 log_assert(GetSize(todo
) == 1);
1210 btorf("%d bad %d\n", nid
, todo
[cursor
]);
1216 struct BtorBackend
: public Backend
{
1217 BtorBackend() : Backend("btor", "write design to BTOR file") { }
1218 void help() YS_OVERRIDE
1220 // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
1222 log(" write_btor [options] [filename]\n");
1224 log("Write a BTOR description of the current design.\n");
1227 log(" Add comments and indentation to BTOR output file\n");
1230 log(" Output only a single bad property for all asserts\n");
1233 void execute(std::ostream
*&f
, std::string filename
, std::vector
<std::string
> args
, RTLIL::Design
*design
) YS_OVERRIDE
1235 bool verbose
= false, single_bad
= false;
1237 log_header(design
, "Executing BTOR backend.\n");
1240 for (argidx
= 1; argidx
< args
.size(); argidx
++)
1242 if (args
[argidx
] == "-v") {
1246 if (args
[argidx
] == "-s") {
1252 extra_args(f
, filename
, args
, argidx
);
1254 RTLIL::Module
*topmod
= design
->top_module();
1256 if (topmod
== nullptr)
1257 log_cmd_error("No top module found.\n");
1259 *f
<< stringf("; BTOR description generated by %s for module %s.\n",
1260 yosys_version_str
, log_id(topmod
));
1262 BtorWorker(*f
, topmod
, verbose
, single_bad
);
1264 *f
<< stringf("; end of yosys output\n");
1268 PRIVATE_NAMESPACE_END