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 int get_mem_sid(int abits
, int dbits
)
107 pair
<int, int> key(abits
, dbits
);
108 if (sorts_mem
.count(key
) == 0) {
109 int addr_sid
= get_bv_sid(abits
);
110 int data_sid
= get_bv_sid(dbits
);
111 int nid
= next_nid
++;
112 btorf("%d sort array %d %d\n", nid
, addr_sid
, data_sid
);
113 sorts_mem
[key
] = nid
;
115 return sorts_mem
.at(key
);
118 void add_nid_sig(int nid
, const SigSpec
&sig
)
121 f
<< indent
<< stringf("; %d %s\n", nid
, log_signal(sig
));
123 for (int i
= 0; i
< GetSize(sig
); i
++)
124 bit_nid
[sig
[i
]] = make_pair(nid
, i
);
127 nid_width
[nid
] = GetSize(sig
);
130 void export_cell(Cell
*cell
)
132 if (cell_recursion_guard
.count(cell
)) {
134 for (auto c
: cell_recursion_guard
)
135 cell_list
+= stringf("\n %s", log_id(c
));
136 log_error("Found topological loop while processing cell %s. Active cells:%s\n", log_id(cell
), cell_list
.c_str());
139 cell_recursion_guard
.insert(cell
);
140 btorf_push(log_id(cell
));
142 if (cell
->type
.in("$add", "$sub", "$mul", "$and", "$or", "$xor", "$xnor", "$shl", "$sshl", "$shr", "$sshr", "$shift", "$shiftx",
143 "$concat", "$_AND_", "$_NAND_", "$_OR_", "$_NOR_", "$_XOR_", "$_XNOR_"))
146 if (cell
->type
== "$add") btor_op
= "add";
147 if (cell
->type
== "$sub") btor_op
= "sub";
148 if (cell
->type
== "$mul") btor_op
= "mul";
149 if (cell
->type
.in("$shl", "$sshl")) btor_op
= "sll";
150 if (cell
->type
== "$shr") btor_op
= "srl";
151 if (cell
->type
== "$sshr") btor_op
= "sra";
152 if (cell
->type
.in("$shift", "$shiftx")) btor_op
= "shift";
153 if (cell
->type
.in("$and", "$_AND_")) btor_op
= "and";
154 if (cell
->type
.in("$or", "$_OR_")) btor_op
= "or";
155 if (cell
->type
.in("$xor", "$_XOR_")) btor_op
= "xor";
156 if (cell
->type
== "$concat") btor_op
= "concat";
157 if (cell
->type
== "$_NAND_") btor_op
= "nand";
158 if (cell
->type
== "$_NOR_") btor_op
= "nor";
159 if (cell
->type
.in("$xnor", "$_XNOR_")) btor_op
= "xnor";
160 log_assert(!btor_op
.empty());
162 int width
= GetSize(cell
->getPort("\\Y"));
163 width
= std::max(width
, GetSize(cell
->getPort("\\A")));
164 width
= std::max(width
, GetSize(cell
->getPort("\\B")));
166 bool a_signed
= cell
->hasParam("\\A_SIGNED") ? cell
->getParam("\\A_SIGNED").as_bool() : false;
167 bool b_signed
= cell
->hasParam("\\B_SIGNED") ? cell
->getParam("\\B_SIGNED").as_bool() : false;
169 if (btor_op
== "shift" && !b_signed
)
172 if (cell
->type
.in("$shl", "$sshl", "$shr", "$sshr"))
175 if (cell
->type
== "$sshr" && !a_signed
)
178 int sid
= get_bv_sid(width
);
181 if (btor_op
== "shift")
183 int nid_a
= get_sig_nid(cell
->getPort("\\A"), width
, false);
184 int nid_b
= get_sig_nid(cell
->getPort("\\B"), width
, b_signed
);
186 int nid_r
= next_nid
++;
187 btorf("%d srl %d %d %d\n", nid_r
, sid
, nid_a
, nid_b
);
189 int nid_b_neg
= next_nid
++;
190 btorf("%d neg %d %d\n", nid_b_neg
, sid
, nid_b
);
192 int nid_l
= next_nid
++;
193 btorf("%d sll %d %d %d\n", nid_l
, sid
, nid_a
, nid_b_neg
);
195 int sid_bit
= get_bv_sid(1);
196 int nid_zero
= get_sig_nid(Const(0, width
));
197 int nid_b_ltz
= next_nid
++;
198 btorf("%d slt %d %d %d\n", nid_b_ltz
, sid_bit
, nid_b
, nid_zero
);
201 btorf("%d ite %d %d %d %d\n", nid
, sid
, nid_b_ltz
, nid_l
, nid_r
);
205 int nid_a
= get_sig_nid(cell
->getPort("\\A"), width
, a_signed
);
206 int nid_b
= get_sig_nid(cell
->getPort("\\B"), width
, b_signed
);
209 btorf("%d %s %d %d %d\n", nid
, btor_op
.c_str(), sid
, nid_a
, nid_b
);
212 SigSpec sig
= sigmap(cell
->getPort("\\Y"));
214 if (GetSize(sig
) < width
) {
215 int sid
= get_bv_sid(GetSize(sig
));
216 int nid2
= next_nid
++;
217 btorf("%d slice %d %d %d 0\n", nid2
, sid
, nid
, GetSize(sig
)-1);
221 add_nid_sig(nid
, sig
);
225 if (cell
->type
.in("$div", "$mod"))
228 if (cell
->type
== "$div") btor_op
= "div";
229 if (cell
->type
== "$mod") btor_op
= "rem";
230 log_assert(!btor_op
.empty());
232 int width
= GetSize(cell
->getPort("\\Y"));
233 width
= std::max(width
, GetSize(cell
->getPort("\\A")));
234 width
= std::max(width
, GetSize(cell
->getPort("\\B")));
236 bool a_signed
= cell
->hasParam("\\A_SIGNED") ? cell
->getParam("\\A_SIGNED").as_bool() : false;
237 bool b_signed
= cell
->hasParam("\\B_SIGNED") ? cell
->getParam("\\B_SIGNED").as_bool() : false;
239 int nid_a
= get_sig_nid(cell
->getPort("\\A"), width
, a_signed
);
240 int nid_b
= get_sig_nid(cell
->getPort("\\B"), width
, b_signed
);
242 int sid
= get_bv_sid(width
);
243 int nid
= next_nid
++;
244 btorf("%d %c%s %d %d %d\n", nid
, a_signed
|| b_signed
? 's' : 'u', btor_op
.c_str(), sid
, nid_a
, nid_b
);
246 SigSpec sig
= sigmap(cell
->getPort("\\Y"));
248 if (GetSize(sig
) < width
) {
249 int sid
= get_bv_sid(GetSize(sig
));
250 int nid2
= next_nid
++;
251 btorf("%d slice %d %d %d 0\n", nid2
, sid
, nid
, GetSize(sig
)-1);
255 add_nid_sig(nid
, sig
);
259 if (cell
->type
.in("$_ANDNOT_", "$_ORNOT_"))
261 int sid
= get_bv_sid(1);
262 int nid_a
= get_sig_nid(cell
->getPort("\\A"));
263 int nid_b
= get_sig_nid(cell
->getPort("\\B"));
265 int nid1
= next_nid
++;
266 int nid2
= next_nid
++;
268 if (cell
->type
== "$_ANDNOT_") {
269 btorf("%d not %d %d\n", nid1
, sid
, nid_b
);
270 btorf("%d and %d %d %d\n", nid2
, sid
, nid_a
, nid1
);
273 if (cell
->type
== "$_ORNOT_") {
274 btorf("%d not %d %d\n", nid1
, sid
, nid_b
);
275 btorf("%d or %d %d %d\n", nid2
, sid
, nid_a
, nid1
);
278 SigSpec sig
= sigmap(cell
->getPort("\\Y"));
279 add_nid_sig(nid2
, sig
);
283 if (cell
->type
.in("$_OAI3_", "$_AOI3_"))
285 int sid
= get_bv_sid(1);
286 int nid_a
= get_sig_nid(cell
->getPort("\\A"));
287 int nid_b
= get_sig_nid(cell
->getPort("\\B"));
288 int nid_c
= get_sig_nid(cell
->getPort("\\C"));
290 int nid1
= next_nid
++;
291 int nid2
= next_nid
++;
292 int nid3
= next_nid
++;
294 if (cell
->type
== "$_OAI3_") {
295 btorf("%d or %d %d %d\n", nid1
, sid
, nid_a
, nid_b
);
296 btorf("%d and %d %d %d\n", nid2
, sid
, nid1
, nid_c
);
297 btorf("%d not %d %d\n", nid3
, sid
, nid2
);
300 if (cell
->type
== "$_AOI3_") {
301 btorf("%d and %d %d %d\n", nid1
, sid
, nid_a
, nid_b
);
302 btorf("%d or %d %d %d\n", nid2
, sid
, nid1
, nid_c
);
303 btorf("%d not %d %d\n", nid3
, sid
, nid2
);
306 SigSpec sig
= sigmap(cell
->getPort("\\Y"));
307 add_nid_sig(nid3
, sig
);
311 if (cell
->type
.in("$_OAI4_", "$_AOI4_"))
313 int sid
= get_bv_sid(1);
314 int nid_a
= get_sig_nid(cell
->getPort("\\A"));
315 int nid_b
= get_sig_nid(cell
->getPort("\\B"));
316 int nid_c
= get_sig_nid(cell
->getPort("\\C"));
317 int nid_d
= get_sig_nid(cell
->getPort("\\D"));
319 int nid1
= next_nid
++;
320 int nid2
= next_nid
++;
321 int nid3
= next_nid
++;
322 int nid4
= next_nid
++;
324 if (cell
->type
== "$_OAI4_") {
325 btorf("%d or %d %d %d\n", nid1
, sid
, nid_a
, nid_b
);
326 btorf("%d or %d %d %d\n", nid2
, sid
, nid_c
, nid_d
);
327 btorf("%d and %d %d %d\n", nid3
, sid
, nid1
, nid2
);
328 btorf("%d not %d %d\n", nid4
, sid
, nid3
);
331 if (cell
->type
== "$_AOI4_") {
332 btorf("%d and %d %d %d\n", nid1
, sid
, nid_a
, nid_b
);
333 btorf("%d and %d %d %d\n", nid2
, sid
, nid_c
, nid_d
);
334 btorf("%d or %d %d %d\n", nid3
, sid
, nid1
, nid2
);
335 btorf("%d not %d %d\n", nid4
, sid
, nid3
);
338 SigSpec sig
= sigmap(cell
->getPort("\\Y"));
339 add_nid_sig(nid4
, sig
);
343 if (cell
->type
.in("$lt", "$le", "$eq", "$eqx", "$ne", "$nex", "$ge", "$gt"))
346 if (cell
->type
== "$lt") btor_op
= "lt";
347 if (cell
->type
== "$le") btor_op
= "lte";
348 if (cell
->type
.in("$eq", "$eqx")) btor_op
= "eq";
349 if (cell
->type
.in("$ne", "$nex")) btor_op
= "neq";
350 if (cell
->type
== "$ge") btor_op
= "gte";
351 if (cell
->type
== "$gt") btor_op
= "gt";
352 log_assert(!btor_op
.empty());
355 width
= std::max(width
, GetSize(cell
->getPort("\\A")));
356 width
= std::max(width
, GetSize(cell
->getPort("\\B")));
358 bool a_signed
= cell
->hasParam("\\A_SIGNED") ? cell
->getParam("\\A_SIGNED").as_bool() : false;
359 bool b_signed
= cell
->hasParam("\\B_SIGNED") ? cell
->getParam("\\B_SIGNED").as_bool() : false;
361 int sid
= get_bv_sid(1);
362 int nid_a
= get_sig_nid(cell
->getPort("\\A"), width
, a_signed
);
363 int nid_b
= get_sig_nid(cell
->getPort("\\B"), width
, b_signed
);
365 int nid
= next_nid
++;
366 if (cell
->type
.in("$lt", "$le", "$ge", "$gt")) {
367 btorf("%d %c%s %d %d %d\n", nid
, a_signed
|| b_signed
? 's' : 'u', btor_op
.c_str(), sid
, nid_a
, nid_b
);
369 btorf("%d %s %d %d %d\n", nid
, btor_op
.c_str(), sid
, nid_a
, nid_b
);
372 SigSpec sig
= sigmap(cell
->getPort("\\Y"));
374 if (GetSize(sig
) > 1) {
375 int sid
= get_bv_sid(GetSize(sig
));
376 int nid2
= next_nid
++;
377 btorf("%d uext %d %d %d\n", nid2
, sid
, nid
, GetSize(sig
) - 1);
381 add_nid_sig(nid
, sig
);
385 if (cell
->type
.in("$not", "$neg", "$_NOT_"))
388 if (cell
->type
.in("$not", "$_NOT_")) btor_op
= "not";
389 if (cell
->type
== "$neg") btor_op
= "neg";
390 log_assert(!btor_op
.empty());
392 int width
= GetSize(cell
->getPort("\\Y"));
393 width
= std::max(width
, GetSize(cell
->getPort("\\A")));
395 bool a_signed
= cell
->hasParam("\\A_SIGNED") ? cell
->getParam("\\A_SIGNED").as_bool() : false;
397 int sid
= get_bv_sid(width
);
398 int nid_a
= get_sig_nid(cell
->getPort("\\A"), width
, a_signed
);
400 int nid
= next_nid
++;
401 btorf("%d %s %d %d\n", nid
, btor_op
.c_str(), sid
, nid_a
);
403 SigSpec sig
= sigmap(cell
->getPort("\\Y"));
405 if (GetSize(sig
) < width
) {
406 int sid
= get_bv_sid(GetSize(sig
));
407 int nid2
= next_nid
++;
408 btorf("%d slice %d %d %d 0\n", nid2
, sid
, nid
, GetSize(sig
)-1);
412 add_nid_sig(nid
, sig
);
416 if (cell
->type
.in("$logic_and", "$logic_or", "$logic_not"))
419 if (cell
->type
== "$logic_and") btor_op
= "and";
420 if (cell
->type
== "$logic_or") btor_op
= "or";
421 if (cell
->type
== "$logic_not") btor_op
= "not";
422 log_assert(!btor_op
.empty());
424 int sid
= get_bv_sid(1);
425 int nid_a
= get_sig_nid(cell
->getPort("\\A"));
426 int nid_b
= btor_op
!= "not" ? get_sig_nid(cell
->getPort("\\B")) : 0;
428 if (GetSize(cell
->getPort("\\A")) > 1) {
429 int nid_red_a
= next_nid
++;
430 btorf("%d redor %d %d\n", nid_red_a
, sid
, nid_a
);
434 if (btor_op
!= "not" && GetSize(cell
->getPort("\\B")) > 1) {
435 int nid_red_b
= next_nid
++;
436 btorf("%d redor %d %d\n", nid_red_b
, sid
, nid_b
);
440 int nid
= next_nid
++;
441 if (btor_op
!= "not")
442 btorf("%d %s %d %d %d\n", nid
, btor_op
.c_str(), sid
, nid_a
, nid_b
);
444 btorf("%d %s %d %d\n", nid
, btor_op
.c_str(), sid
, nid_a
);
446 SigSpec sig
= sigmap(cell
->getPort("\\Y"));
448 if (GetSize(sig
) > 1) {
449 int sid
= get_bv_sid(GetSize(sig
));
450 int zeros_nid
= get_sig_nid(Const(0, GetSize(sig
)-1));
451 int nid2
= next_nid
++;
452 btorf("%d concat %d %d %d\n", nid2
, sid
, zeros_nid
, nid
);
456 add_nid_sig(nid
, sig
);
460 if (cell
->type
.in("$reduce_and", "$reduce_or", "$reduce_bool", "$reduce_xor", "$reduce_xnor"))
463 if (cell
->type
== "$reduce_and") btor_op
= "redand";
464 if (cell
->type
.in("$reduce_or", "$reduce_bool")) btor_op
= "redor";
465 if (cell
->type
.in("$reduce_xor", "$reduce_xnor")) btor_op
= "redxor";
466 log_assert(!btor_op
.empty());
468 int sid
= get_bv_sid(1);
469 int nid_a
= get_sig_nid(cell
->getPort("\\A"));
471 int nid
= next_nid
++;
472 btorf("%d %s %d %d\n", nid
, btor_op
.c_str(), sid
, nid_a
);
474 if (cell
->type
== "$reduce_xnor") {
475 int nid2
= next_nid
++;
476 btorf("%d not %d %d %d\n", nid2
, sid
, nid
);
480 SigSpec sig
= sigmap(cell
->getPort("\\Y"));
482 if (GetSize(sig
) > 1) {
483 int sid
= get_bv_sid(GetSize(sig
));
484 int zeros_nid
= get_sig_nid(Const(0, GetSize(sig
)-1));
485 int nid2
= next_nid
++;
486 btorf("%d concat %d %d %d\n", nid2
, sid
, zeros_nid
, nid
);
490 add_nid_sig(nid
, sig
);
494 if (cell
->type
.in("$mux", "$_MUX_"))
496 SigSpec sig_a
= sigmap(cell
->getPort("\\A"));
497 SigSpec sig_b
= sigmap(cell
->getPort("\\B"));
498 SigSpec sig_s
= sigmap(cell
->getPort("\\S"));
499 SigSpec sig_y
= sigmap(cell
->getPort("\\Y"));
501 int nid_a
= get_sig_nid(sig_a
);
502 int nid_b
= get_sig_nid(sig_b
);
503 int nid_s
= get_sig_nid(sig_s
);
505 int sid
= get_bv_sid(GetSize(sig_y
));
506 int nid
= next_nid
++;
507 btorf("%d ite %d %d %d %d\n", nid
, sid
, nid_s
, nid_b
, nid_a
);
509 add_nid_sig(nid
, sig_y
);
513 if (cell
->type
== "$pmux")
515 SigSpec sig_a
= sigmap(cell
->getPort("\\A"));
516 SigSpec sig_b
= sigmap(cell
->getPort("\\B"));
517 SigSpec sig_s
= sigmap(cell
->getPort("\\S"));
518 SigSpec sig_y
= sigmap(cell
->getPort("\\Y"));
520 int width
= GetSize(sig_a
);
521 int sid
= get_bv_sid(width
);
522 int nid
= get_sig_nid(sig_a
);
524 for (int i
= 0; i
< GetSize(sig_s
); i
++) {
525 int nid_b
= get_sig_nid(sig_b
.extract(i
*width
, width
));
526 int nid_s
= get_sig_nid(sig_s
.extract(i
));
527 int nid2
= next_nid
++;
528 btorf("%d ite %d %d %d %d\n", nid2
, sid
, nid_s
, nid_b
, nid
);
532 add_nid_sig(nid
, sig_y
);
536 if (cell
->type
.in("$dff", "$ff", "$_DFF_P_", "$_DFF_N", "$_FF_"))
538 SigSpec sig_d
= sigmap(cell
->getPort("\\D"));
539 SigSpec sig_q
= sigmap(cell
->getPort("\\Q"));
543 if (sig_q
.is_wire()) {
544 Wire
*w
= sig_q
.as_wire();
545 if (w
->port_id
== 0) {
546 statewires
.insert(w
);
552 for (int i
= 0; i
< GetSize(sig_q
); i
++)
553 if (initbits
.count(sig_q
[i
]))
554 initval
.bits
.push_back(initbits
.at(sig_q
[i
]) ? State::S1
: State::S0
);
556 initval
.bits
.push_back(State::Sx
);
558 int nid_init_val
= -1;
560 if (!initval
.is_fully_undef())
561 nid_init_val
= get_sig_nid(initval
);
563 int sid
= get_bv_sid(GetSize(sig_q
));
564 int nid
= next_nid
++;
567 btorf("%d state %d\n", nid
, sid
);
569 btorf("%d state %d %s\n", nid
, sid
, log_id(symbol
));
571 if (nid_init_val
>= 0) {
572 int nid_init
= next_nid
++;
574 btorf("; initval = %s\n", log_signal(initval
));
575 btorf("%d init %d %d %d\n", nid_init
, sid
, nid
, nid_init_val
);
578 ff_todo
.push_back(make_pair(nid
, cell
));
579 add_nid_sig(nid
, sig_q
);
583 if (cell
->type
.in("$anyconst", "$anyseq"))
585 SigSpec sig_y
= sigmap(cell
->getPort("\\Y"));
587 int sid
= get_bv_sid(GetSize(sig_y
));
588 int nid
= next_nid
++;
590 btorf("%d state %d\n", nid
, sid
);
592 if (cell
->type
== "$anyconst") {
593 int nid2
= next_nid
++;
594 btorf("%d next %d %d %d\n", nid2
, sid
, nid
, nid
);
597 add_nid_sig(nid
, sig_y
);
601 if (cell
->type
== "$initstate")
603 SigSpec sig_y
= sigmap(cell
->getPort("\\Y"));
605 if (initstate_nid
< 0)
607 int sid
= get_bv_sid(1);
608 int one_nid
= get_sig_nid(Const(1, 1));
609 int zero_nid
= get_sig_nid(Const(0, 1));
610 initstate_nid
= next_nid
++;
611 btorf("%d state %d\n", initstate_nid
, sid
);
612 btorf("%d init %d %d %d\n", next_nid
++, sid
, initstate_nid
, one_nid
);
613 btorf("%d next %d %d %d\n", next_nid
++, sid
, initstate_nid
, zero_nid
);
616 add_nid_sig(initstate_nid
, sig_y
);
620 if (cell
->type
== "$mem")
622 int abits
= cell
->getParam("\\ABITS").as_int();
623 int width
= cell
->getParam("\\WIDTH").as_int();
624 int nwords
= cell
->getParam("\\SIZE").as_int();
625 int rdports
= cell
->getParam("\\RD_PORTS").as_int();
626 int wrports
= cell
->getParam("\\WR_PORTS").as_int();
628 Const wr_clk_en
= cell
->getParam("\\WR_CLK_ENABLE");
629 Const rd_clk_en
= cell
->getParam("\\RD_CLK_ENABLE");
631 bool asyncwr
= wr_clk_en
.is_fully_zero();
633 if (!asyncwr
&& !wr_clk_en
.is_fully_ones())
634 log_error("Memory %s.%s has mixed async/sync write ports.\n",
635 log_id(module
), log_id(cell
));
637 if (!rd_clk_en
.is_fully_zero())
638 log_error("Memory %s.%s has sync read ports.\n",
639 log_id(module
), log_id(cell
));
641 SigSpec sig_rd_addr
= sigmap(cell
->getPort("\\RD_ADDR"));
642 SigSpec sig_rd_data
= sigmap(cell
->getPort("\\RD_DATA"));
644 SigSpec sig_wr_addr
= sigmap(cell
->getPort("\\WR_ADDR"));
645 SigSpec sig_wr_data
= sigmap(cell
->getPort("\\WR_DATA"));
646 SigSpec sig_wr_en
= sigmap(cell
->getPort("\\WR_EN"));
648 int data_sid
= get_bv_sid(width
);
649 int bool_sid
= get_bv_sid(1);
650 int sid
= get_mem_sid(abits
, width
);
652 Const initdata
= cell
->getParam("\\INIT");
653 initdata
.exts(nwords
*width
);
654 int nid_init_val
= -1;
656 if (!initdata
.is_fully_undef())
658 bool constword
= true;
659 Const firstword
= initdata
.extract(0, width
);
661 for (int i
= 1; i
< nwords
; i
++) {
662 Const thisword
= initdata
.extract(i
*width
, width
);
663 if (thisword
!= firstword
) {
672 btorf("; initval = %s\n", log_signal(firstword
));
673 nid_init_val
= get_sig_nid(firstword
);
677 int nid_init_val
= next_nid
++;
678 btorf("%d state %d\n", nid_init_val
, sid
);
680 for (int i
= 0; i
< nwords
; i
++) {
681 Const thisword
= initdata
.extract(i
*width
, width
);
682 if (thisword
.is_fully_undef())
684 Const
thisaddr(i
, abits
);
685 int nid_thisword
= get_sig_nid(thisword
);
686 int nid_thisaddr
= get_sig_nid(thisaddr
);
687 int last_nid_init_val
= nid_init_val
;
688 nid_init_val
= next_nid
++;
690 btorf("; initval[%d] = %s\n", i
, log_signal(thisword
));
691 btorf("%d write %d %d %d %d\n", nid_init_val
, sid
, last_nid_init_val
, nid_thisaddr
, nid_thisword
);
697 int nid
= next_nid
++;
700 if (cell
->name
[0] == '$')
701 btorf("%d state %d\n", nid
, sid
);
703 btorf("%d state %d %s\n", nid
, sid
, log_id(cell
));
705 if (nid_init_val
>= 0)
707 int nid_init
= next_nid
++;
708 btorf("%d init %d %d %d\n", nid_init
, sid
, nid
, nid_init_val
);
713 for (int port
= 0; port
< wrports
; port
++)
715 SigSpec wa
= sig_wr_addr
.extract(port
*abits
, abits
);
716 SigSpec wd
= sig_wr_data
.extract(port
*width
, width
);
717 SigSpec we
= sig_wr_en
.extract(port
*width
, width
);
719 int wa_nid
= get_sig_nid(wa
);
720 int wd_nid
= get_sig_nid(wd
);
721 int we_nid
= get_sig_nid(we
);
723 int nid2
= next_nid
++;
724 btorf("%d read %d %d %d\n", nid2
, data_sid
, nid_head
, wa_nid
);
726 int nid3
= next_nid
++;
727 btorf("%d not %d %d\n", nid3
, data_sid
, we_nid
);
729 int nid4
= next_nid
++;
730 btorf("%d and %d %d %d\n", nid4
, data_sid
, nid2
, nid3
);
732 int nid5
= next_nid
++;
733 btorf("%d and %d %d %d\n", nid5
, data_sid
, wd_nid
, we_nid
);
735 int nid6
= next_nid
++;
736 btorf("%d or %d %d %d\n", nid6
, data_sid
, nid5
, nid4
);
738 int nid7
= next_nid
++;
739 btorf("%d write %d %d %d %d\n", nid7
, sid
, nid_head
, wa_nid
, nid6
);
741 int nid8
= next_nid
++;
742 btorf("%d redor %d %d\n", nid8
, bool_sid
, we_nid
);
744 int nid9
= next_nid
++;
745 btorf("%d ite %d %d %d %d\n", nid9
, sid
, nid8
, nid7
, nid_head
);
751 for (int port
= 0; port
< rdports
; port
++)
753 SigSpec ra
= sig_rd_addr
.extract(port
*abits
, abits
);
754 SigSpec rd
= sig_rd_data
.extract(port
*width
, width
);
756 int ra_nid
= get_sig_nid(ra
);
757 int rd_nid
= next_nid
++;
759 btorf("%d read %d %d %d\n", rd_nid
, data_sid
, nid_head
, ra_nid
);
761 add_nid_sig(rd_nid
, rd
);
766 ff_todo
.push_back(make_pair(nid
, cell
));
770 int nid2
= next_nid
++;
771 btorf("%d next %d %d %d\n", nid2
, sid
, nid
, nid_head
);
777 log_error("Unsupported cell type: %s (%s)\n", log_id(cell
->type
), log_id(cell
));
780 btorf_pop(log_id(cell
));
781 cell_recursion_guard
.erase(cell
);
784 int get_sig_nid(SigSpec sig
, int to_width
= -1, bool is_signed
= false)
790 if (bit
== State::Sx
)
796 SigSpec sig_mask_undef
, sig_noundef
;
797 int first_undef
= -1;
799 for (int i
= 0; i
< GetSize(sig
); i
++)
800 if (sig
[i
] == State::Sx
) {
803 sig_mask_undef
.append(State::S1
);
804 sig_noundef
.append(State::S0
);
806 sig_mask_undef
.append(State::S0
);
807 sig_noundef
.append(sig
[i
]);
810 if (to_width
< 0 || first_undef
< to_width
)
812 int sid
= get_bv_sid(GetSize(sig
));
814 int nid_input
= next_nid
++;
815 btorf("%d input %d\n", nid_input
, sid
);
817 int nid_masked_input
;
818 if (sig_mask_undef
.is_fully_ones()) {
819 nid_masked_input
= nid_input
;
821 int nid_mask_undef
= get_sig_nid(sig_mask_undef
);
822 nid_masked_input
= next_nid
++;
823 btorf("%d and %d %d %d\n", nid_masked_input
, sid
, nid_input
, nid_mask_undef
);
826 if (sig_noundef
.is_fully_zero()) {
827 nid
= nid_masked_input
;
829 int nid_noundef
= get_sig_nid(sig_noundef
);
831 btorf("%d or %d %d %d\n", nid
, sid
, nid_masked_input
, nid_noundef
);
840 if (sig_nid
.count(sig
) == 0)
843 vector
<pair
<int, int>> nidbits
;
846 for (int i
= 0; i
< GetSize(sig
); i
++)
850 if (bit_nid
.count(bit
) == 0)
852 if (bit
.wire
== nullptr)
856 while (i
+GetSize(c
) < GetSize(sig
) && sig
[i
+GetSize(c
)].wire
== nullptr)
857 c
.bits
.push_back(sig
[i
+GetSize(c
)].data
);
859 if (consts
.count(c
) == 0) {
860 int sid
= get_bv_sid(GetSize(c
));
861 int nid
= next_nid
++;
862 btorf("%d const %d %s\n", nid
, sid
, c
.as_string().c_str());
864 nid_width
[nid
] = GetSize(c
);
867 int nid
= consts
.at(c
);
869 for (int j
= 0; j
< GetSize(c
); j
++)
870 nidbits
.push_back(make_pair(nid
, j
));
877 if (bit_cell
.count(bit
) == 0)
878 log_error("No driver for signal bit %s.\n", log_signal(bit
));
879 export_cell(bit_cell
.at(bit
));
880 log_assert(bit_nid
.count(bit
));
884 nidbits
.push_back(bit_nid
.at(bit
));
890 // group bits and emit slice-concat chain
891 for (int i
= 0; i
< GetSize(nidbits
); i
++)
893 int nid2
= nidbits
[i
].first
;
894 int lower
= nidbits
[i
].second
;
897 while (i
+1 < GetSize(nidbits
) && nidbits
[i
+1].first
== nidbits
[i
].first
&&
898 nidbits
[i
+1].second
== nidbits
[i
].second
+1)
903 if (lower
!= 0 || upper
+1 != nid_width
.at(nid2
)) {
904 int sid
= get_bv_sid(upper
-lower
+1);
906 btorf("%d slice %d %d %d %d\n", nid3
, sid
, nid2
, upper
, lower
);
912 int sid
= get_bv_sid(width
+upper
-lower
+1);
914 btorf("%d concat %d %d %d\n", nid4
, sid
, nid3
, nid
);
917 width
+= upper
-lower
+1;
922 nid_width
[nid
] = width
;
925 nid
= sig_nid
.at(sig
);
928 if (to_width
>= 0 && to_width
!= GetSize(sig
))
930 if (to_width
< GetSize(sig
))
932 int sid
= get_bv_sid(to_width
);
933 int nid2
= next_nid
++;
934 btorf("%d slice %d %d %d 0\n", nid2
, sid
, nid
, to_width
-1);
939 int sid
= get_bv_sid(to_width
);
940 int nid2
= next_nid
++;
941 btorf("%d %s %d %d %d\n", nid2
, is_signed
? "sext" : "uext",
942 sid
, nid
, to_width
- GetSize(sig
));
950 BtorWorker(std::ostream
&f
, RTLIL::Module
*module
, bool verbose
, bool single_bad
) :
951 f(f
), sigmap(module
), module(module
), verbose(verbose
), single_bad(single_bad
)
953 btorf_push("inputs");
955 for (auto wire
: module
->wires())
957 if (wire
->attributes
.count("\\init")) {
958 Const attrval
= wire
->attributes
.at("\\init");
959 for (int i
= 0; i
< GetSize(wire
) && i
< GetSize(attrval
); i
++)
960 if (attrval
[i
] == State::S0
|| attrval
[i
] == State::S1
)
961 initbits
[sigmap(SigBit(wire
, i
))] = (attrval
[i
] == State::S1
);
964 if (!wire
->port_id
|| !wire
->port_input
)
967 SigSpec sig
= sigmap(wire
);
968 int sid
= get_bv_sid(GetSize(sig
));
969 int nid
= next_nid
++;
971 btorf("%d input %d %s\n", nid
, sid
, log_id(wire
));
972 add_nid_sig(nid
, sig
);
977 for (auto cell
: module
->cells())
978 for (auto &conn
: cell
->connections())
980 if (!cell
->output(conn
.first
))
983 for (auto bit
: sigmap(conn
.second
))
984 bit_cell
[bit
] = cell
;
987 for (auto wire
: module
->wires())
989 if (!wire
->port_id
|| !wire
->port_output
)
992 btorf_push(stringf("output %s", log_id(wire
)));
994 int nid
= get_sig_nid(wire
);
995 btorf("%d output %d %s\n", next_nid
++, nid
, log_id(wire
));
997 btorf_pop(stringf("output %s", log_id(wire
)));
1000 for (auto cell
: module
->cells())
1002 if (cell
->type
== "$assume")
1004 btorf_push(log_id(cell
));
1006 int sid
= get_bv_sid(1);
1007 int nid_a
= get_sig_nid(cell
->getPort("\\A"));
1008 int nid_en
= get_sig_nid(cell
->getPort("\\EN"));
1009 int nid_not_en
= next_nid
++;
1010 int nid_a_or_not_en
= next_nid
++;
1011 int nid
= next_nid
++;
1013 btorf("%d not %d %d\n", nid_not_en
, sid
, nid_en
);
1014 btorf("%d or %d %d %d\n", nid_a_or_not_en
, sid
, nid_a
, nid_not_en
);
1015 btorf("%d constraint %d\n", nid
, nid_a_or_not_en
);
1017 btorf_pop(log_id(cell
));
1020 if (cell
->type
== "$assert")
1022 btorf_push(log_id(cell
));
1024 int sid
= get_bv_sid(1);
1025 int nid_a
= get_sig_nid(cell
->getPort("\\A"));
1026 int nid_en
= get_sig_nid(cell
->getPort("\\EN"));
1027 int nid_not_a
= next_nid
++;
1028 int nid_en_and_not_a
= next_nid
++;
1030 btorf("%d not %d %d\n", nid_not_a
, sid
, nid_a
);
1031 btorf("%d and %d %d %d\n", nid_en_and_not_a
, sid
, nid_en
, nid_not_a
);
1034 bad_properties
.push_back(nid_en_and_not_a
);
1036 int nid
= next_nid
++;
1037 btorf("%d bad %d\n", nid
, nid_en_and_not_a
);
1040 btorf_pop(log_id(cell
));
1044 for (auto wire
: module
->wires())
1046 if (wire
->port_id
|| wire
->name
[0] == '$')
1049 btorf_push(stringf("wire %s", log_id(wire
)));
1051 int sid
= get_bv_sid(GetSize(wire
));
1052 int nid
= get_sig_nid(sigmap(wire
));
1054 if (statewires
.count(wire
))
1057 int this_nid
= next_nid
++;
1058 btorf("%d uext %d %d %d %s\n", this_nid
, sid
, nid
, 0, log_id(wire
));
1060 btorf_pop(stringf("wire %s", log_id(wire
)));
1064 while (!ff_todo
.empty())
1066 vector
<pair
<int, Cell
*>> todo
;
1069 for (auto &it
: todo
)
1072 Cell
*cell
= it
.second
;
1074 btorf_push(stringf("next %s", log_id(cell
)));
1076 if (cell
->type
== "$mem")
1078 int abits
= cell
->getParam("\\ABITS").as_int();
1079 int width
= cell
->getParam("\\WIDTH").as_int();
1080 int wrports
= cell
->getParam("\\WR_PORTS").as_int();
1082 SigSpec sig_wr_addr
= sigmap(cell
->getPort("\\WR_ADDR"));
1083 SigSpec sig_wr_data
= sigmap(cell
->getPort("\\WR_DATA"));
1084 SigSpec sig_wr_en
= sigmap(cell
->getPort("\\WR_EN"));
1086 int data_sid
= get_bv_sid(width
);
1087 int bool_sid
= get_bv_sid(1);
1088 int sid
= get_mem_sid(abits
, width
);
1091 for (int port
= 0; port
< wrports
; port
++)
1093 SigSpec wa
= sig_wr_addr
.extract(port
*abits
, abits
);
1094 SigSpec wd
= sig_wr_data
.extract(port
*width
, width
);
1095 SigSpec we
= sig_wr_en
.extract(port
*width
, width
);
1097 int wa_nid
= get_sig_nid(wa
);
1098 int wd_nid
= get_sig_nid(wd
);
1099 int we_nid
= get_sig_nid(we
);
1101 int nid2
= next_nid
++;
1102 btorf("%d read %d %d %d\n", nid2
, data_sid
, nid_head
, wa_nid
);
1104 int nid3
= next_nid
++;
1105 btorf("%d not %d %d\n", nid3
, data_sid
, we_nid
);
1107 int nid4
= next_nid
++;
1108 btorf("%d and %d %d %d\n", nid4
, data_sid
, nid2
, nid3
);
1110 int nid5
= next_nid
++;
1111 btorf("%d and %d %d %d\n", nid5
, data_sid
, wd_nid
, we_nid
);
1113 int nid6
= next_nid
++;
1114 btorf("%d or %d %d %d\n", nid6
, data_sid
, nid5
, nid4
);
1116 int nid7
= next_nid
++;
1117 btorf("%d write %d %d %d %d\n", nid7
, sid
, nid_head
, wa_nid
, nid6
);
1119 int nid8
= next_nid
++;
1120 btorf("%d redor %d %d\n", nid8
, bool_sid
, we_nid
);
1122 int nid9
= next_nid
++;
1123 btorf("%d ite %d %d %d %d\n", nid9
, sid
, nid8
, nid7
, nid_head
);
1128 int nid2
= next_nid
++;
1129 btorf("%d next %d %d %d\n", nid2
, sid
, nid
, nid_head
);
1133 SigSpec sig
= sigmap(cell
->getPort("\\D"));
1134 int nid_q
= get_sig_nid(sig
);
1135 int sid
= get_bv_sid(GetSize(sig
));
1136 btorf("%d next %d %d %d\n", next_nid
++, sid
, nid
, nid_q
);
1139 btorf_pop(stringf("next %s", log_id(cell
)));
1143 while (!bad_properties
.empty())
1146 bad_properties
.swap(todo
);
1148 int sid
= get_bv_sid(1);
1151 while (cursor
+1 < GetSize(todo
))
1153 int nid_a
= todo
[cursor
++];
1154 int nid_b
= todo
[cursor
++];
1155 int nid
= next_nid
++;
1157 bad_properties
.push_back(nid
);
1158 btorf("%d or %d %d %d\n", nid
, sid
, nid_a
, nid_b
);
1161 if (!bad_properties
.empty()) {
1162 if (cursor
< GetSize(todo
))
1163 bad_properties
.push_back(todo
[cursor
++]);
1164 log_assert(cursor
== GetSize(todo
));
1166 int nid
= next_nid
++;
1167 log_assert(cursor
== 0);
1168 log_assert(GetSize(todo
) == 1);
1169 btorf("%d bad %d\n", nid
, todo
[cursor
]);
1175 struct BtorBackend
: public Backend
{
1176 BtorBackend() : Backend("btor", "write design to BTOR file") { }
1177 void help() YS_OVERRIDE
1179 // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
1181 log(" write_btor [options] [filename]\n");
1183 log("Write a BTOR description of the current design.\n");
1186 log(" Add comments and indentation to BTOR output file\n");
1189 log(" Output only a single bad property for all asserts\n");
1192 void execute(std::ostream
*&f
, std::string filename
, std::vector
<std::string
> args
, RTLIL::Design
*design
) YS_OVERRIDE
1194 bool verbose
= false, single_bad
= false;
1196 log_header(design
, "Executing BTOR backend.\n");
1199 for (argidx
= 1; argidx
< args
.size(); argidx
++)
1201 if (args
[argidx
] == "-v") {
1205 if (args
[argidx
] == "-s") {
1211 extra_args(f
, filename
, args
, argidx
);
1213 RTLIL::Module
*topmod
= design
->top_module();
1215 if (topmod
== nullptr)
1216 log_cmd_error("No top module found.\n");
1218 *f
<< stringf("; BTOR description generated by %s for module %s.\n",
1219 yosys_version_str
, log_id(topmod
));
1221 BtorWorker(*f
, topmod
, verbose
, single_bad
);
1223 *f
<< stringf("; end of yosys output\n");
1227 PRIVATE_NAMESPACE_END