2 * yosys -- Yosys Open SYnthesis Suite
4 * Copyright (C) 2012 Claire Xenia Wolf <claire@yosyshq.com>
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, C. 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"
30 #include "kernel/mem.h"
34 PRIVATE_NAMESPACE_BEGIN
40 RTLIL::Module
*module
;
44 bool print_internal_names
;
47 int initstate_nid
= -1;
50 dict
<int, int> sorts_bv
;
52 // (<address-width>, <data-width>) => <sid>
53 dict
<pair
<int, int>, int> sorts_mem
;
55 // SigBit => (<nid>, <bitidx>)
56 dict
<SigBit
, pair
<int, int>> bit_nid
;
59 dict
<int, int> nid_width
;
62 dict
<SigSpec
, int> sig_nid
;
64 // bit to driving cell
65 dict
<SigBit
, Cell
*> bit_cell
;
68 dict
<Const
, int> consts
;
70 // ff inputs that need to be evaluated (<nid>, <ff_cell>)
71 vector
<pair
<int, Cell
*>> ff_todo
;
72 vector
<pair
<int, Mem
*>> mem_todo
;
74 pool
<Cell
*> cell_recursion_guard
;
75 vector
<int> bad_properties
;
76 dict
<SigBit
, bool> initbits
;
77 pool
<Wire
*> statewires
;
78 pool
<string
> srcsymbols
;
80 dict
<Cell
*, Mem
*> mem_cells
;
82 string indent
, info_filename
;
83 vector
<string
> info_lines
;
84 dict
<int, int> info_clocks
;
86 void btorf(const char *fmt
, ...) YS_ATTRIBUTE(format(printf
, 2, 3))
90 f
<< indent
<< vstringf(fmt
, ap
);
94 void infof(const char *fmt
, ...) YS_ATTRIBUTE(format(printf
, 2, 3))
98 info_lines
.push_back(vstringf(fmt
, ap
));
103 string
getinfo(T
*obj
, bool srcsym
= false)
105 string infostr
= log_id(obj
);
106 if (!srcsym
&& !print_internal_names
&& infostr
[0] == '$') return "";
107 if (obj
->attributes
.count(ID::src
)) {
108 string src
= obj
->attributes
.at(ID::src
).decode_string().c_str();
109 if (srcsym
&& infostr
[0] == '$') {
110 std::replace(src
.begin(), src
.end(), ' ', '_');
111 if (srcsymbols
.count(src
) || module
->count_id("\\" + src
)) {
112 for (int i
= 1;; i
++) {
113 string s
= stringf("%s-%d", src
.c_str(), i
);
114 if (!srcsymbols
.count(s
) && !module
->count_id("\\" + s
)) {
120 srcsymbols
.insert(src
);
123 infostr
+= " ; " + src
;
126 return " " + infostr
;
129 void btorf_push(const string
&id
)
132 f
<< indent
<< stringf(" ; begin %s\n", id
.c_str());
137 void btorf_pop(const string
&id
)
140 indent
= indent
.substr(4);
141 f
<< indent
<< stringf(" ; end %s\n", id
.c_str());
145 int get_bv_sid(int width
)
147 if (sorts_bv
.count(width
) == 0) {
148 int nid
= next_nid
++;
149 btorf("%d sort bitvec %d\n", nid
, width
);
150 sorts_bv
[width
] = nid
;
152 return sorts_bv
.at(width
);
155 int get_mem_sid(int abits
, int dbits
)
157 pair
<int, int> key(abits
, dbits
);
158 if (sorts_mem
.count(key
) == 0) {
159 int addr_sid
= get_bv_sid(abits
);
160 int data_sid
= get_bv_sid(dbits
);
161 int nid
= next_nid
++;
162 btorf("%d sort array %d %d\n", nid
, addr_sid
, data_sid
);
163 sorts_mem
[key
] = nid
;
165 return sorts_mem
.at(key
);
168 void add_nid_sig(int nid
, const SigSpec
&sig
)
171 f
<< indent
<< stringf("; %d %s\n", nid
, log_signal(sig
));
173 for (int i
= 0; i
< GetSize(sig
); i
++)
174 bit_nid
[sig
[i
]] = make_pair(nid
, i
);
177 nid_width
[nid
] = GetSize(sig
);
180 void export_cell(Cell
*cell
)
182 if (cell_recursion_guard
.count(cell
)) {
184 for (auto c
: cell_recursion_guard
)
185 cell_list
+= stringf("\n %s", log_id(c
));
186 log_error("Found topological loop while processing cell %s. Active cells:%s\n", log_id(cell
), cell_list
.c_str());
189 cell_recursion_guard
.insert(cell
);
190 btorf_push(log_id(cell
));
192 if (cell
->type
.in(ID($add
), ID($sub
), ID($mul
), ID($
and), ID($
or), ID($
xor), ID($xnor
), ID($shl
), ID($sshl
), ID($shr
), ID($sshr
), ID($shift
), ID($shiftx
),
193 ID($concat
), ID($_AND_
), ID($_NAND_
), ID($_OR_
), ID($_NOR_
), ID($_XOR_
), ID($_XNOR_
)))
196 if (cell
->type
== ID($add
)) btor_op
= "add";
197 if (cell
->type
== ID($sub
)) btor_op
= "sub";
198 if (cell
->type
== ID($mul
)) btor_op
= "mul";
199 if (cell
->type
.in(ID($shl
), ID($sshl
))) btor_op
= "sll";
200 if (cell
->type
== ID($shr
)) btor_op
= "srl";
201 if (cell
->type
== ID($sshr
)) btor_op
= "sra";
202 if (cell
->type
.in(ID($shift
), ID($shiftx
))) btor_op
= "shift";
203 if (cell
->type
.in(ID($
and), ID($_AND_
))) btor_op
= "and";
204 if (cell
->type
.in(ID($
or), ID($_OR_
))) btor_op
= "or";
205 if (cell
->type
.in(ID($
xor), ID($_XOR_
))) btor_op
= "xor";
206 if (cell
->type
== ID($concat
)) btor_op
= "concat";
207 if (cell
->type
== ID($_NAND_
)) btor_op
= "nand";
208 if (cell
->type
== ID($_NOR_
)) btor_op
= "nor";
209 if (cell
->type
.in(ID($xnor
), ID($_XNOR_
))) btor_op
= "xnor";
210 log_assert(!btor_op
.empty());
212 int width_ay
= std::max(GetSize(cell
->getPort(ID::A
)), GetSize(cell
->getPort(ID::Y
)));
213 int width
= std::max(width_ay
, GetSize(cell
->getPort(ID::B
)));
215 bool a_signed
= cell
->hasParam(ID::A_SIGNED
) ? cell
->getParam(ID::A_SIGNED
).as_bool() : false;
216 bool b_signed
= cell
->hasParam(ID::B_SIGNED
) ? cell
->getParam(ID::B_SIGNED
).as_bool() : false;
218 if (btor_op
== "shift" && !b_signed
)
221 if (cell
->type
.in(ID($shl
), ID($sshl
), ID($shr
), ID($sshr
)))
224 if (cell
->type
== ID($sshr
) && !a_signed
)
227 int sid
= get_bv_sid(width
);
231 if (cell
->type
.in(ID($shl
), ID($shr
), ID($shift
), ID($shiftx
)) && a_signed
&& width_ay
< width
) {
232 // sign-extend A up to the width of Y
233 int nid_a_padded
= get_sig_nid(cell
->getPort(ID::A
), width_ay
, a_signed
);
235 // zero-extend the rest
236 int zeroes
= get_sig_nid(Const(0, width
-width_ay
));
238 btorf("%d concat %d %d %d\n", nid_a
, sid
, zeroes
, nid_a_padded
);
240 nid_a
= get_sig_nid(cell
->getPort(ID::A
), width
, a_signed
);
243 int nid_b
= get_sig_nid(cell
->getPort(ID::B
), width
, b_signed
);
245 if (btor_op
== "shift")
247 int nid_r
= next_nid
++;
248 btorf("%d srl %d %d %d\n", nid_r
, sid
, nid_a
, nid_b
);
250 int nid_b_neg
= next_nid
++;
251 btorf("%d neg %d %d\n", nid_b_neg
, sid
, nid_b
);
253 int nid_l
= next_nid
++;
254 btorf("%d sll %d %d %d\n", nid_l
, sid
, nid_a
, nid_b_neg
);
256 int sid_bit
= get_bv_sid(1);
257 int nid_zero
= get_sig_nid(Const(0, width
));
258 int nid_b_ltz
= next_nid
++;
259 btorf("%d slt %d %d %d\n", nid_b_ltz
, sid_bit
, nid_b
, nid_zero
);
262 btorf("%d ite %d %d %d %d%s\n", nid
, sid
, nid_b_ltz
, nid_l
, nid_r
, getinfo(cell
).c_str());
267 btorf("%d %s %d %d %d%s\n", nid
, btor_op
.c_str(), sid
, nid_a
, nid_b
, getinfo(cell
).c_str());
270 SigSpec sig
= sigmap(cell
->getPort(ID::Y
));
272 if (GetSize(sig
) < width
) {
273 int sid
= get_bv_sid(GetSize(sig
));
274 int nid2
= next_nid
++;
275 btorf("%d slice %d %d %d 0\n", nid2
, sid
, nid
, GetSize(sig
)-1);
279 add_nid_sig(nid
, sig
);
283 if (cell
->type
.in(ID($div
), ID($mod
), ID($modfloor
)))
285 bool a_signed
= cell
->hasParam(ID::A_SIGNED
) ? cell
->getParam(ID::A_SIGNED
).as_bool() : false;
286 bool b_signed
= cell
->hasParam(ID::B_SIGNED
) ? cell
->getParam(ID::B_SIGNED
).as_bool() : false;
289 if (cell
->type
== ID($div
)) btor_op
= "div";
290 // "rem" = truncating modulo
291 if (cell
->type
== ID($mod
)) btor_op
= "rem";
292 // "mod" = flooring modulo
293 if (cell
->type
== ID($modfloor
)) {
294 // "umod" doesn't exist because it's the same as "urem"
295 btor_op
= a_signed
|| b_signed
? "mod" : "rem";
297 log_assert(!btor_op
.empty());
299 int width
= GetSize(cell
->getPort(ID::Y
));
300 width
= std::max(width
, GetSize(cell
->getPort(ID::A
)));
301 width
= std::max(width
, GetSize(cell
->getPort(ID::B
)));
303 int nid_a
= get_sig_nid(cell
->getPort(ID::A
), width
, a_signed
);
304 int nid_b
= get_sig_nid(cell
->getPort(ID::B
), width
, b_signed
);
306 int sid
= get_bv_sid(width
);
307 int nid
= next_nid
++;
308 btorf("%d %c%s %d %d %d%s\n", nid
, a_signed
|| b_signed
? 's' : 'u', btor_op
.c_str(), sid
, nid_a
, nid_b
, getinfo(cell
).c_str());
310 SigSpec sig
= sigmap(cell
->getPort(ID::Y
));
312 if (GetSize(sig
) < width
) {
313 int sid
= get_bv_sid(GetSize(sig
));
314 int nid2
= next_nid
++;
315 btorf("%d slice %d %d %d 0\n", nid2
, sid
, nid
, GetSize(sig
)-1);
319 add_nid_sig(nid
, sig
);
323 if (cell
->type
.in(ID($_ANDNOT_
), ID($_ORNOT_
)))
325 int sid
= get_bv_sid(1);
326 int nid_a
= get_sig_nid(cell
->getPort(ID::A
));
327 int nid_b
= get_sig_nid(cell
->getPort(ID::B
));
329 int nid1
= next_nid
++;
330 int nid2
= next_nid
++;
332 if (cell
->type
== ID($_ANDNOT_
)) {
333 btorf("%d not %d %d\n", nid1
, sid
, nid_b
);
334 btorf("%d and %d %d %d%s\n", nid2
, sid
, nid_a
, nid1
, getinfo(cell
).c_str());
337 if (cell
->type
== ID($_ORNOT_
)) {
338 btorf("%d not %d %d\n", nid1
, sid
, nid_b
);
339 btorf("%d or %d %d %d%s\n", nid2
, sid
, nid_a
, nid1
, getinfo(cell
).c_str());
342 SigSpec sig
= sigmap(cell
->getPort(ID::Y
));
343 add_nid_sig(nid2
, sig
);
347 if (cell
->type
.in(ID($_OAI3_
), ID($_AOI3_
)))
349 int sid
= get_bv_sid(1);
350 int nid_a
= get_sig_nid(cell
->getPort(ID::A
));
351 int nid_b
= get_sig_nid(cell
->getPort(ID::B
));
352 int nid_c
= get_sig_nid(cell
->getPort(ID::C
));
354 int nid1
= next_nid
++;
355 int nid2
= next_nid
++;
356 int nid3
= next_nid
++;
358 if (cell
->type
== ID($_OAI3_
)) {
359 btorf("%d or %d %d %d\n", nid1
, sid
, nid_a
, nid_b
);
360 btorf("%d and %d %d %d\n", nid2
, sid
, nid1
, nid_c
);
361 btorf("%d not %d %d%s\n", nid3
, sid
, nid2
, getinfo(cell
).c_str());
364 if (cell
->type
== ID($_AOI3_
)) {
365 btorf("%d and %d %d %d\n", nid1
, sid
, nid_a
, nid_b
);
366 btorf("%d or %d %d %d\n", nid2
, sid
, nid1
, nid_c
);
367 btorf("%d not %d %d%s\n", nid3
, sid
, nid2
, getinfo(cell
).c_str());
370 SigSpec sig
= sigmap(cell
->getPort(ID::Y
));
371 add_nid_sig(nid3
, sig
);
375 if (cell
->type
.in(ID($_OAI4_
), ID($_AOI4_
)))
377 int sid
= get_bv_sid(1);
378 int nid_a
= get_sig_nid(cell
->getPort(ID::A
));
379 int nid_b
= get_sig_nid(cell
->getPort(ID::B
));
380 int nid_c
= get_sig_nid(cell
->getPort(ID::C
));
381 int nid_d
= get_sig_nid(cell
->getPort(ID::D
));
383 int nid1
= next_nid
++;
384 int nid2
= next_nid
++;
385 int nid3
= next_nid
++;
386 int nid4
= next_nid
++;
388 if (cell
->type
== ID($_OAI4_
)) {
389 btorf("%d or %d %d %d\n", nid1
, sid
, nid_a
, nid_b
);
390 btorf("%d or %d %d %d\n", nid2
, sid
, nid_c
, nid_d
);
391 btorf("%d and %d %d %d\n", nid3
, sid
, nid1
, nid2
);
392 btorf("%d not %d %d%s\n", nid4
, sid
, nid3
, getinfo(cell
).c_str());
395 if (cell
->type
== ID($_AOI4_
)) {
396 btorf("%d and %d %d %d\n", nid1
, sid
, nid_a
, nid_b
);
397 btorf("%d and %d %d %d\n", nid2
, sid
, nid_c
, nid_d
);
398 btorf("%d or %d %d %d\n", nid3
, sid
, nid1
, nid2
);
399 btorf("%d not %d %d%s\n", nid4
, sid
, nid3
, getinfo(cell
).c_str());
402 SigSpec sig
= sigmap(cell
->getPort(ID::Y
));
403 add_nid_sig(nid4
, sig
);
407 if (cell
->type
.in(ID($lt
), ID($le
), ID($eq
), ID($eqx
), ID($ne
), ID($nex
), ID($ge
), ID($gt
)))
410 if (cell
->type
== ID($lt
)) btor_op
= "lt";
411 if (cell
->type
== ID($le
)) btor_op
= "lte";
412 if (cell
->type
.in(ID($eq
), ID($eqx
))) btor_op
= "eq";
413 if (cell
->type
.in(ID($ne
), ID($nex
))) btor_op
= "neq";
414 if (cell
->type
== ID($ge
)) btor_op
= "gte";
415 if (cell
->type
== ID($gt
)) btor_op
= "gt";
416 log_assert(!btor_op
.empty());
419 width
= std::max(width
, GetSize(cell
->getPort(ID::A
)));
420 width
= std::max(width
, GetSize(cell
->getPort(ID::B
)));
422 bool a_signed
= cell
->hasParam(ID::A_SIGNED
) ? cell
->getParam(ID::A_SIGNED
).as_bool() : false;
423 bool b_signed
= cell
->hasParam(ID::B_SIGNED
) ? cell
->getParam(ID::B_SIGNED
).as_bool() : false;
425 int sid
= get_bv_sid(1);
426 int nid_a
= get_sig_nid(cell
->getPort(ID::A
), width
, a_signed
);
427 int nid_b
= get_sig_nid(cell
->getPort(ID::B
), width
, b_signed
);
429 int nid
= next_nid
++;
430 if (cell
->type
.in(ID($lt
), ID($le
), ID($ge
), ID($gt
))) {
431 btorf("%d %c%s %d %d %d%s\n", nid
, a_signed
|| b_signed
? 's' : 'u', btor_op
.c_str(), sid
, nid_a
, nid_b
, getinfo(cell
).c_str());
433 btorf("%d %s %d %d %d%s\n", nid
, btor_op
.c_str(), sid
, nid_a
, nid_b
, getinfo(cell
).c_str());
436 SigSpec sig
= sigmap(cell
->getPort(ID::Y
));
438 if (GetSize(sig
) > 1) {
439 int sid
= get_bv_sid(GetSize(sig
));
440 int nid2
= next_nid
++;
441 btorf("%d uext %d %d %d\n", nid2
, sid
, nid
, GetSize(sig
) - 1);
445 add_nid_sig(nid
, sig
);
449 if (cell
->type
.in(ID($
not), ID($neg
), ID($_NOT_
)))
452 if (cell
->type
.in(ID($
not), ID($_NOT_
))) btor_op
= "not";
453 if (cell
->type
== ID($neg
)) btor_op
= "neg";
454 log_assert(!btor_op
.empty());
456 int width
= std::max(GetSize(cell
->getPort(ID::A
)), GetSize(cell
->getPort(ID::Y
)));
458 bool a_signed
= cell
->hasParam(ID::A_SIGNED
) ? cell
->getParam(ID::A_SIGNED
).as_bool() : false;
460 int sid
= get_bv_sid(width
);
461 int nid_a
= get_sig_nid(cell
->getPort(ID::A
), width
, a_signed
);
463 int nid
= next_nid
++;
464 btorf("%d %s %d %d%s\n", nid
, btor_op
.c_str(), sid
, nid_a
, getinfo(cell
).c_str());
466 SigSpec sig
= sigmap(cell
->getPort(ID::Y
));
468 if (GetSize(sig
) < width
) {
469 int sid
= get_bv_sid(GetSize(sig
));
470 int nid2
= next_nid
++;
471 btorf("%d slice %d %d %d 0\n", nid2
, sid
, nid
, GetSize(sig
)-1);
475 add_nid_sig(nid
, sig
);
479 if (cell
->type
.in(ID($logic_and
), ID($logic_or
), ID($logic_not
)))
482 if (cell
->type
== ID($logic_and
)) btor_op
= "and";
483 if (cell
->type
== ID($logic_or
)) btor_op
= "or";
484 if (cell
->type
== ID($logic_not
)) btor_op
= "not";
485 log_assert(!btor_op
.empty());
487 int sid
= get_bv_sid(1);
488 int nid_a
= get_sig_nid(cell
->getPort(ID::A
));
489 int nid_b
= btor_op
!= "not" ? get_sig_nid(cell
->getPort(ID::B
)) : 0;
491 if (GetSize(cell
->getPort(ID::A
)) > 1) {
492 int nid_red_a
= next_nid
++;
493 btorf("%d redor %d %d\n", nid_red_a
, sid
, nid_a
);
497 if (btor_op
!= "not" && GetSize(cell
->getPort(ID::B
)) > 1) {
498 int nid_red_b
= next_nid
++;
499 btorf("%d redor %d %d\n", nid_red_b
, sid
, nid_b
);
503 int nid
= next_nid
++;
504 if (btor_op
!= "not")
505 btorf("%d %s %d %d %d%s\n", nid
, btor_op
.c_str(), sid
, nid_a
, nid_b
, getinfo(cell
).c_str());
507 btorf("%d %s %d %d%s\n", nid
, btor_op
.c_str(), sid
, nid_a
, getinfo(cell
).c_str());
509 SigSpec sig
= sigmap(cell
->getPort(ID::Y
));
511 if (GetSize(sig
) > 1) {
512 int sid
= get_bv_sid(GetSize(sig
));
513 int zeros_nid
= get_sig_nid(Const(0, GetSize(sig
)-1));
514 int nid2
= next_nid
++;
515 btorf("%d concat %d %d %d\n", nid2
, sid
, zeros_nid
, nid
);
519 add_nid_sig(nid
, sig
);
523 if (cell
->type
.in(ID($reduce_and
), ID($reduce_or
), ID($reduce_bool
), ID($reduce_xor
), ID($reduce_xnor
)))
526 if (cell
->type
== ID($reduce_and
)) btor_op
= "redand";
527 if (cell
->type
.in(ID($reduce_or
), ID($reduce_bool
))) btor_op
= "redor";
528 if (cell
->type
.in(ID($reduce_xor
), ID($reduce_xnor
))) btor_op
= "redxor";
529 log_assert(!btor_op
.empty());
531 int sid
= get_bv_sid(1);
532 int nid_a
= get_sig_nid(cell
->getPort(ID::A
));
534 int nid
= next_nid
++;
536 if (cell
->type
== ID($reduce_xnor
)) {
537 int nid2
= next_nid
++;
538 btorf("%d %s %d %d%s\n", nid
, btor_op
.c_str(), sid
, nid_a
, getinfo(cell
).c_str());
539 btorf("%d not %d %d\n", nid2
, sid
, nid
);
542 btorf("%d %s %d %d%s\n", nid
, btor_op
.c_str(), sid
, nid_a
, getinfo(cell
).c_str());
545 SigSpec sig
= sigmap(cell
->getPort(ID::Y
));
547 if (GetSize(sig
) > 1) {
548 int sid
= get_bv_sid(GetSize(sig
));
549 int zeros_nid
= get_sig_nid(Const(0, GetSize(sig
)-1));
550 int nid2
= next_nid
++;
551 btorf("%d concat %d %d %d\n", nid2
, sid
, zeros_nid
, nid
);
555 add_nid_sig(nid
, sig
);
559 if (cell
->type
.in(ID($mux
), ID($_MUX_
), ID($_NMUX_
)))
561 SigSpec sig_a
= sigmap(cell
->getPort(ID::A
));
562 SigSpec sig_b
= sigmap(cell
->getPort(ID::B
));
563 SigSpec sig_s
= sigmap(cell
->getPort(ID::S
));
564 SigSpec sig_y
= sigmap(cell
->getPort(ID::Y
));
566 int nid_a
= get_sig_nid(sig_a
);
567 int nid_b
= get_sig_nid(sig_b
);
568 int nid_s
= get_sig_nid(sig_s
);
570 int sid
= get_bv_sid(GetSize(sig_y
));
571 int nid
= next_nid
++;
573 if (cell
->type
== ID($_NMUX_
)) {
576 btorf("%d ite %d %d %d %d\n", tmp
, sid
, nid_s
, nid_b
, nid_a
);
577 btorf("%d not %d %d%s\n", nid
, sid
, tmp
, getinfo(cell
).c_str());
579 btorf("%d ite %d %d %d %d%s\n", nid
, sid
, nid_s
, nid_b
, nid_a
, getinfo(cell
).c_str());
582 add_nid_sig(nid
, sig_y
);
586 if (cell
->type
== ID($pmux
))
588 SigSpec sig_a
= sigmap(cell
->getPort(ID::A
));
589 SigSpec sig_b
= sigmap(cell
->getPort(ID::B
));
590 SigSpec sig_s
= sigmap(cell
->getPort(ID::S
));
591 SigSpec sig_y
= sigmap(cell
->getPort(ID::Y
));
593 int width
= GetSize(sig_a
);
594 int sid
= get_bv_sid(width
);
595 int nid
= get_sig_nid(sig_a
);
597 for (int i
= 0; i
< GetSize(sig_s
); i
++) {
598 int nid_b
= get_sig_nid(sig_b
.extract(i
*width
, width
));
599 int nid_s
= get_sig_nid(sig_s
.extract(i
));
600 int nid2
= next_nid
++;
601 if (i
== GetSize(sig_s
)-1)
602 btorf("%d ite %d %d %d %d%s\n", nid2
, sid
, nid_s
, nid_b
, nid
, getinfo(cell
).c_str());
604 btorf("%d ite %d %d %d %d\n", nid2
, sid
, nid_s
, nid_b
, nid
);
608 add_nid_sig(nid
, sig_y
);
612 if (cell
->type
.in(ID($dff
), ID($ff
), ID($_DFF_P_
), ID($_DFF_N
), ID($_FF_
)))
614 SigSpec sig_d
= sigmap(cell
->getPort(ID::D
));
615 SigSpec sig_q
= sigmap(cell
->getPort(ID::Q
));
617 if (!info_filename
.empty() && cell
->type
.in(ID($dff
), ID($_DFF_P_
), ID($_DFF_N_
)))
619 SigSpec sig_c
= sigmap(cell
->getPort(cell
->type
== ID($dff
) ? ID::CLK
: ID::C
));
620 int nid
= get_sig_nid(sig_c
);
621 bool negedge
= false;
623 if (cell
->type
== ID($_DFF_N_
))
626 if (cell
->type
== ID($dff
) && !cell
->getParam(ID::CLK_POLARITY
).as_bool())
629 info_clocks
[nid
] |= negedge
? 2 : 1;
634 if (sig_q
.is_wire()) {
635 Wire
*w
= sig_q
.as_wire();
636 if (w
->port_id
== 0) {
637 statewires
.insert(w
);
643 for (int i
= 0; i
< GetSize(sig_q
); i
++)
644 if (initbits
.count(sig_q
[i
]))
645 initval
.bits
.push_back(initbits
.at(sig_q
[i
]) ? State::S1
: State::S0
);
647 initval
.bits
.push_back(State::Sx
);
649 int nid_init_val
= -1;
651 if (!initval
.is_fully_undef())
652 nid_init_val
= get_sig_nid(initval
, -1, false, true);
654 int sid
= get_bv_sid(GetSize(sig_q
));
655 int nid
= next_nid
++;
657 if (symbol
.empty() || (!print_internal_names
&& symbol
[0] == '$'))
658 btorf("%d state %d\n", nid
, sid
);
660 btorf("%d state %d %s\n", nid
, sid
, log_id(symbol
));
662 if (nid_init_val
>= 0) {
663 int nid_init
= next_nid
++;
665 btorf("; initval = %s\n", log_signal(initval
));
666 btorf("%d init %d %d %d\n", nid_init
, sid
, nid
, nid_init_val
);
669 ff_todo
.push_back(make_pair(nid
, cell
));
670 add_nid_sig(nid
, sig_q
);
674 if (cell
->type
.in(ID($anyconst
), ID($anyseq
)))
676 SigSpec sig_y
= sigmap(cell
->getPort(ID::Y
));
678 int sid
= get_bv_sid(GetSize(sig_y
));
679 int nid
= next_nid
++;
681 btorf("%d state %d%s\n", nid
, sid
, getinfo(cell
).c_str());
683 if (cell
->type
== ID($anyconst
)) {
684 int nid2
= next_nid
++;
685 btorf("%d next %d %d %d\n", nid2
, sid
, nid
, nid
);
688 add_nid_sig(nid
, sig_y
);
692 if (cell
->type
== ID($initstate
))
694 SigSpec sig_y
= sigmap(cell
->getPort(ID::Y
));
696 if (initstate_nid
< 0)
698 int sid
= get_bv_sid(1);
699 int one_nid
= get_sig_nid(State::S1
);
700 int zero_nid
= get_sig_nid(State::S0
);
701 initstate_nid
= next_nid
++;
702 btorf("%d state %d%s\n", initstate_nid
, sid
, getinfo(cell
).c_str());
703 btorf("%d init %d %d %d\n", next_nid
++, sid
, initstate_nid
, one_nid
);
704 btorf("%d next %d %d %d\n", next_nid
++, sid
, initstate_nid
, zero_nid
);
707 add_nid_sig(initstate_nid
, sig_y
);
711 if (cell
->is_mem_cell())
713 Mem
*mem
= mem_cells
[cell
];
715 int abits
= ceil_log2(mem
->size
);
717 bool asyncwr
= false;
720 for (auto &port
: mem
->wr_ports
) {
727 if (asyncwr
&& syncwr
)
728 log_error("Memory %s.%s has mixed async/sync write ports.\n",
729 log_id(module
), log_id(mem
->memid
));
731 for (auto &port
: mem
->rd_ports
) {
733 log_error("Memory %s.%s has sync read ports. Please use memory_nordff to convert them first.\n",
734 log_id(module
), log_id(mem
->memid
));
737 int data_sid
= get_bv_sid(mem
->width
);
738 int bool_sid
= get_bv_sid(1);
739 int sid
= get_mem_sid(abits
, mem
->width
);
741 int nid_init_val
= -1;
743 if (!mem
->inits
.empty())
745 Const initdata
= mem
->get_init_data();
746 bool constword
= true;
747 Const firstword
= initdata
.extract(0, mem
->width
);
749 for (int i
= 1; i
< mem
->size
; i
++) {
750 Const thisword
= initdata
.extract(i
*mem
->width
, mem
->width
);
751 if (thisword
!= firstword
) {
760 btorf("; initval = %s\n", log_signal(firstword
));
761 nid_init_val
= get_sig_nid(firstword
, -1, false, true);
765 nid_init_val
= next_nid
++;
766 btorf("%d state %d\n", nid_init_val
, sid
);
768 for (int i
= 0; i
< mem
->size
; i
++) {
769 Const thisword
= initdata
.extract(i
*mem
->width
, mem
->width
);
770 if (thisword
.is_fully_undef())
772 Const
thisaddr(i
, abits
);
773 int nid_thisword
= get_sig_nid(thisword
, -1, false, true);
774 int nid_thisaddr
= get_sig_nid(thisaddr
, -1, false, true);
775 int last_nid_init_val
= nid_init_val
;
776 nid_init_val
= next_nid
++;
778 btorf("; initval[%d] = %s\n", i
, log_signal(thisword
));
779 btorf("%d write %d %d %d %d\n", nid_init_val
, sid
, last_nid_init_val
, nid_thisaddr
, nid_thisword
);
785 int nid
= next_nid
++;
788 if (mem
->memid
[0] == '$')
789 btorf("%d state %d\n", nid
, sid
);
791 btorf("%d state %d %s\n", nid
, sid
, log_id(mem
->memid
));
793 if (nid_init_val
>= 0)
795 int nid_init
= next_nid
++;
796 btorf("%d init %d %d %d\n", nid_init
, sid
, nid
, nid_init_val
);
801 for (auto &port
: mem
->wr_ports
)
803 SigSpec wa
= port
.addr
;
806 int wa_nid
= get_sig_nid(wa
);
807 int wd_nid
= get_sig_nid(port
.data
);
808 int we_nid
= get_sig_nid(port
.en
);
810 int nid2
= next_nid
++;
811 btorf("%d read %d %d %d\n", nid2
, data_sid
, nid_head
, wa_nid
);
813 int nid3
= next_nid
++;
814 btorf("%d not %d %d\n", nid3
, data_sid
, we_nid
);
816 int nid4
= next_nid
++;
817 btorf("%d and %d %d %d\n", nid4
, data_sid
, nid2
, nid3
);
819 int nid5
= next_nid
++;
820 btorf("%d and %d %d %d\n", nid5
, data_sid
, wd_nid
, we_nid
);
822 int nid6
= next_nid
++;
823 btorf("%d or %d %d %d\n", nid6
, data_sid
, nid5
, nid4
);
825 int nid7
= next_nid
++;
826 btorf("%d write %d %d %d %d\n", nid7
, sid
, nid_head
, wa_nid
, nid6
);
828 int nid8
= next_nid
++;
829 btorf("%d redor %d %d\n", nid8
, bool_sid
, we_nid
);
831 int nid9
= next_nid
++;
832 btorf("%d ite %d %d %d %d\n", nid9
, sid
, nid8
, nid7
, nid_head
);
838 for (auto &port
: mem
->rd_ports
)
840 SigSpec ra
= port
.addr
;
843 int ra_nid
= get_sig_nid(ra
);
844 int rd_nid
= next_nid
++;
846 btorf("%d read %d %d %d\n", rd_nid
, data_sid
, nid_head
, ra_nid
);
848 add_nid_sig(rd_nid
, port
.data
);
853 mem_todo
.push_back(make_pair(nid
, mem
));
857 int nid2
= next_nid
++;
858 btorf("%d next %d %d %d\n", nid2
, sid
, nid
, nid_head
);
864 if (cell
->type
.in(ID($dffe
), ID($sdff
), ID($sdffe
), ID($sdffce
)) || cell
->type
.str().substr(0, 6) == "$_SDFF" || (cell
->type
.str().substr(0, 6) == "$_DFFE" && cell
->type
.str().size() == 10)) {
865 log_error("Unsupported cell type %s for cell %s.%s -- please run `dffunmap` before `write_btor`.\n",
866 log_id(cell
->type
), log_id(module
), log_id(cell
));
868 if (cell
->type
.in(ID($adff
), ID($adffe
), ID($aldff
), ID($aldffe
), ID($dffsr
), ID($dffsre
)) || cell
->type
.str().substr(0, 5) == "$_DFF" || cell
->type
.str().substr(0, 7) == "$_ALDFF") {
869 log_error("Unsupported cell type %s for cell %s.%s -- please run `async2sync; dffunmap` or `clk2fflogic` before `write_btor`.\n",
870 log_id(cell
->type
), log_id(module
), log_id(cell
));
872 if (cell
->type
.in(ID($sr
), ID($dlatch
), ID($adlatch
), ID($dlatchsr
)) || cell
->type
.str().substr(0, 8) == "$_DLATCH" || cell
->type
.str().substr(0, 5) == "$_SR_") {
873 log_error("Unsupported cell type %s for cell %s.%s -- please run `clk2fflogic` before `write_btor`.\n",
874 log_id(cell
->type
), log_id(module
), log_id(cell
));
876 log_error("Unsupported cell type %s for cell %s.%s.\n",
877 log_id(cell
->type
), log_id(module
), log_id(cell
));
880 btorf_pop(log_id(cell
));
881 cell_recursion_guard
.erase(cell
);
884 int get_sig_nid(SigSpec sig
, int to_width
= -1, bool is_signed
= false, bool is_init
= false)
890 if (bit
== State::Sx
)
896 SigSpec sig_mask_undef
, sig_noundef
;
897 int first_undef
= -1;
899 for (int i
= 0; i
< GetSize(sig
); i
++)
900 if (sig
[i
] == State::Sx
) {
903 sig_mask_undef
.append(State::S1
);
904 sig_noundef
.append(State::S0
);
906 sig_mask_undef
.append(State::S0
);
907 sig_noundef
.append(sig
[i
]);
910 if (to_width
< 0 || first_undef
< to_width
)
912 int sid
= get_bv_sid(GetSize(sig
));
914 int nid_input
= next_nid
++;
916 btorf("%d state %d\n", nid_input
, sid
);
918 btorf("%d input %d\n", nid_input
, sid
);
920 int nid_masked_input
;
921 if (sig_mask_undef
.is_fully_ones()) {
922 nid_masked_input
= nid_input
;
924 int nid_mask_undef
= get_sig_nid(sig_mask_undef
);
925 nid_masked_input
= next_nid
++;
926 btorf("%d and %d %d %d\n", nid_masked_input
, sid
, nid_input
, nid_mask_undef
);
929 if (sig_noundef
.is_fully_zero()) {
930 nid
= nid_masked_input
;
932 int nid_noundef
= get_sig_nid(sig_noundef
);
934 btorf("%d or %d %d %d\n", nid
, sid
, nid_masked_input
, nid_noundef
);
943 if (sig_nid
.count(sig
) == 0)
946 vector
<pair
<int, int>> nidbits
;
949 for (int i
= 0; i
< GetSize(sig
); i
++)
953 if (bit_nid
.count(bit
) == 0)
955 if (bit
.wire
== nullptr)
959 while (i
+GetSize(c
) < GetSize(sig
) && sig
[i
+GetSize(c
)].wire
== nullptr)
960 c
.bits
.push_back(sig
[i
+GetSize(c
)].data
);
962 if (consts
.count(c
) == 0) {
963 int sid
= get_bv_sid(GetSize(c
));
964 int nid
= next_nid
++;
965 btorf("%d const %d %s\n", nid
, sid
, c
.as_string().c_str());
967 nid_width
[nid
] = GetSize(c
);
970 int nid
= consts
.at(c
);
972 for (int j
= 0; j
< GetSize(c
); j
++)
973 nidbits
.push_back(make_pair(nid
, j
));
980 if (bit_cell
.count(bit
) == 0)
984 while (i
+GetSize(s
) < GetSize(sig
) && sig
[i
+GetSize(s
)].wire
!= nullptr &&
985 bit_cell
.count(sig
[i
+GetSize(s
)]) == 0)
986 s
.append(sig
[i
+GetSize(s
)]);
988 log_warning("No driver for signal %s.\n", log_signal(s
));
990 int sid
= get_bv_sid(GetSize(s
));
991 int nid
= next_nid
++;
992 btorf("%d input %d\n", nid
, sid
);
993 nid_width
[nid
] = GetSize(s
);
995 for (int j
= 0; j
< GetSize(s
); j
++)
996 nidbits
.push_back(make_pair(nid
, j
));
1003 export_cell(bit_cell
.at(bit
));
1004 log_assert(bit_nid
.count(bit
));
1009 nidbits
.push_back(bit_nid
.at(bit
));
1015 // group bits and emit slice-concat chain
1016 for (int i
= 0; i
< GetSize(nidbits
); i
++)
1018 int nid2
= nidbits
[i
].first
;
1019 int lower
= nidbits
[i
].second
;
1022 while (i
+1 < GetSize(nidbits
) && nidbits
[i
+1].first
== nidbits
[i
].first
&&
1023 nidbits
[i
+1].second
== nidbits
[i
].second
+1)
1028 if (lower
!= 0 || upper
+1 != nid_width
.at(nid2
)) {
1029 int sid
= get_bv_sid(upper
-lower
+1);
1031 btorf("%d slice %d %d %d %d\n", nid3
, sid
, nid2
, upper
, lower
);
1037 int sid
= get_bv_sid(width
+upper
-lower
+1);
1039 btorf("%d concat %d %d %d\n", nid4
, sid
, nid3
, nid
);
1042 width
+= upper
-lower
+1;
1047 nid_width
[nid
] = width
;
1050 nid
= sig_nid
.at(sig
);
1053 if (to_width
>= 0 && to_width
!= GetSize(sig
))
1055 if (to_width
< GetSize(sig
))
1057 int sid
= get_bv_sid(to_width
);
1058 int nid2
= next_nid
++;
1059 btorf("%d slice %d %d %d 0\n", nid2
, sid
, nid
, to_width
-1);
1064 int sid
= get_bv_sid(to_width
);
1065 int nid2
= next_nid
++;
1066 btorf("%d %s %d %d %d\n", nid2
, is_signed
? "sext" : "uext",
1067 sid
, nid
, to_width
- GetSize(sig
));
1075 BtorWorker(std::ostream
&f
, RTLIL::Module
*module
, bool verbose
, bool single_bad
, bool cover_mode
, bool print_internal_names
, string info_filename
) :
1076 f(f
), sigmap(module
), module(module
), verbose(verbose
), single_bad(single_bad
), cover_mode(cover_mode
), print_internal_names(print_internal_names
), info_filename(info_filename
)
1078 if (!info_filename
.empty())
1079 infof("name %s\n", log_id(module
));
1081 memories
= Mem::get_all_memories(module
);
1083 dict
<IdString
, Mem
*> mem_dict
;
1084 for (auto &mem
: memories
) {
1086 mem_dict
[mem
.memid
] = &mem
;
1088 for (auto cell
: module
->cells())
1089 if (cell
->is_mem_cell())
1090 mem_cells
[cell
] = mem_dict
[cell
->parameters
.at(ID::MEMID
).decode_string()];
1092 btorf_push("inputs");
1094 for (auto wire
: module
->wires())
1096 if (wire
->attributes
.count(ID::init
)) {
1097 Const attrval
= wire
->attributes
.at(ID::init
);
1098 for (int i
= 0; i
< GetSize(wire
) && i
< GetSize(attrval
); i
++)
1099 if (attrval
[i
] == State::S0
|| attrval
[i
] == State::S1
)
1100 initbits
[sigmap(SigBit(wire
, i
))] = (attrval
[i
] == State::S1
);
1103 if (!wire
->port_id
|| !wire
->port_input
)
1106 SigSpec sig
= sigmap(wire
);
1107 int sid
= get_bv_sid(GetSize(sig
));
1108 int nid
= next_nid
++;
1110 btorf("%d input %d%s\n", nid
, sid
, getinfo(wire
).c_str());
1111 add_nid_sig(nid
, sig
);
1114 btorf_pop("inputs");
1116 for (auto cell
: module
->cells())
1117 for (auto &conn
: cell
->connections())
1119 if (!cell
->output(conn
.first
))
1122 for (auto bit
: sigmap(conn
.second
))
1123 bit_cell
[bit
] = cell
;
1126 for (auto wire
: module
->wires())
1128 if (!wire
->port_id
|| !wire
->port_output
)
1131 btorf_push(stringf("output %s", log_id(wire
)));
1133 int nid
= get_sig_nid(wire
);
1134 btorf("%d output %d%s\n", next_nid
++, nid
, getinfo(wire
).c_str());
1136 btorf_pop(stringf("output %s", log_id(wire
)));
1139 for (auto cell
: module
->cells())
1141 if (cell
->type
== ID($assume
))
1143 btorf_push(log_id(cell
));
1145 int sid
= get_bv_sid(1);
1146 int nid_a
= get_sig_nid(cell
->getPort(ID::A
));
1147 int nid_en
= get_sig_nid(cell
->getPort(ID::EN
));
1148 int nid_not_en
= next_nid
++;
1149 int nid_a_or_not_en
= next_nid
++;
1150 int nid
= next_nid
++;
1152 btorf("%d not %d %d\n", nid_not_en
, sid
, nid_en
);
1153 btorf("%d or %d %d %d\n", nid_a_or_not_en
, sid
, nid_a
, nid_not_en
);
1154 btorf("%d constraint %d\n", nid
, nid_a_or_not_en
);
1156 btorf_pop(log_id(cell
));
1159 if (cell
->type
== ID($
assert))
1161 btorf_push(log_id(cell
));
1163 int sid
= get_bv_sid(1);
1164 int nid_a
= get_sig_nid(cell
->getPort(ID::A
));
1165 int nid_en
= get_sig_nid(cell
->getPort(ID::EN
));
1166 int nid_not_a
= next_nid
++;
1167 int nid_en_and_not_a
= next_nid
++;
1169 btorf("%d not %d %d\n", nid_not_a
, sid
, nid_a
);
1170 btorf("%d and %d %d %d\n", nid_en_and_not_a
, sid
, nid_en
, nid_not_a
);
1172 if (single_bad
&& !cover_mode
) {
1173 bad_properties
.push_back(nid_en_and_not_a
);
1176 infof("bad %d%s\n", nid_en_and_not_a
, getinfo(cell
, true).c_str());
1178 int nid
= next_nid
++;
1179 btorf("%d bad %d%s\n", nid
, nid_en_and_not_a
, getinfo(cell
, true).c_str());
1183 btorf_pop(log_id(cell
));
1186 if (cell
->type
== ID($cover
) && cover_mode
)
1188 btorf_push(log_id(cell
));
1190 int sid
= get_bv_sid(1);
1191 int nid_a
= get_sig_nid(cell
->getPort(ID::A
));
1192 int nid_en
= get_sig_nid(cell
->getPort(ID::EN
));
1193 int nid_en_and_a
= next_nid
++;
1195 btorf("%d and %d %d %d\n", nid_en_and_a
, sid
, nid_en
, nid_a
);
1198 bad_properties
.push_back(nid_en_and_a
);
1200 int nid
= next_nid
++;
1201 btorf("%d bad %d%s\n", nid
, nid_en_and_a
, getinfo(cell
, true).c_str());
1204 btorf_pop(log_id(cell
));
1208 for (auto wire
: module
->wires())
1210 if (wire
->port_id
|| wire
->name
[0] == '$')
1213 btorf_push(stringf("wire %s", log_id(wire
)));
1215 int sid
= get_bv_sid(GetSize(wire
));
1216 int nid
= get_sig_nid(sigmap(wire
));
1218 if (statewires
.count(wire
))
1221 int this_nid
= next_nid
++;
1222 btorf("%d uext %d %d %d%s\n", this_nid
, sid
, nid
, 0, getinfo(wire
).c_str());
1224 btorf_pop(stringf("wire %s", log_id(wire
)));
1228 while (!ff_todo
.empty() || !mem_todo
.empty())
1230 vector
<pair
<int, Cell
*>> todo
;
1233 for (auto &it
: todo
)
1236 Cell
*cell
= it
.second
;
1238 btorf_push(stringf("next %s", log_id(cell
)));
1240 SigSpec sig
= sigmap(cell
->getPort(ID::D
));
1241 int nid_q
= get_sig_nid(sig
);
1242 int sid
= get_bv_sid(GetSize(sig
));
1243 btorf("%d next %d %d %d%s\n", next_nid
++, sid
, nid
, nid_q
, getinfo(cell
).c_str());
1245 btorf_pop(stringf("next %s", log_id(cell
)));
1248 vector
<pair
<int, Mem
*>> mtodo
;
1249 mtodo
.swap(mem_todo
);
1251 for (auto &it
: mtodo
)
1254 Mem
*mem
= it
.second
;
1256 btorf_push(stringf("next %s", log_id(mem
->memid
)));
1258 int abits
= ceil_log2(mem
->size
);
1260 int data_sid
= get_bv_sid(mem
->width
);
1261 int bool_sid
= get_bv_sid(1);
1262 int sid
= get_mem_sid(abits
, mem
->width
);
1265 for (auto &port
: mem
->wr_ports
)
1267 SigSpec wa
= port
.addr
;
1268 wa
.extend_u0(abits
);
1270 int wa_nid
= get_sig_nid(wa
);
1271 int wd_nid
= get_sig_nid(port
.data
);
1272 int we_nid
= get_sig_nid(port
.en
);
1274 int nid2
= next_nid
++;
1275 btorf("%d read %d %d %d\n", nid2
, data_sid
, nid_head
, wa_nid
);
1277 int nid3
= next_nid
++;
1278 btorf("%d not %d %d\n", nid3
, data_sid
, we_nid
);
1280 int nid4
= next_nid
++;
1281 btorf("%d and %d %d %d\n", nid4
, data_sid
, nid2
, nid3
);
1283 int nid5
= next_nid
++;
1284 btorf("%d and %d %d %d\n", nid5
, data_sid
, wd_nid
, we_nid
);
1286 int nid6
= next_nid
++;
1287 btorf("%d or %d %d %d\n", nid6
, data_sid
, nid5
, nid4
);
1289 int nid7
= next_nid
++;
1290 btorf("%d write %d %d %d %d\n", nid7
, sid
, nid_head
, wa_nid
, nid6
);
1292 int nid8
= next_nid
++;
1293 btorf("%d redor %d %d\n", nid8
, bool_sid
, we_nid
);
1295 int nid9
= next_nid
++;
1296 btorf("%d ite %d %d %d %d\n", nid9
, sid
, nid8
, nid7
, nid_head
);
1301 int nid2
= next_nid
++;
1302 btorf("%d next %d %d %d%s\n", nid2
, sid
, nid
, nid_head
, (mem
->cell
? getinfo(mem
->cell
) : getinfo(mem
->mem
)).c_str());
1304 btorf_pop(stringf("next %s", log_id(mem
->memid
)));
1308 while (!bad_properties
.empty())
1311 bad_properties
.swap(todo
);
1313 int sid
= get_bv_sid(1);
1316 while (cursor
+1 < GetSize(todo
))
1318 int nid_a
= todo
[cursor
++];
1319 int nid_b
= todo
[cursor
++];
1320 int nid
= next_nid
++;
1322 bad_properties
.push_back(nid
);
1323 btorf("%d or %d %d %d\n", nid
, sid
, nid_a
, nid_b
);
1326 if (!bad_properties
.empty()) {
1327 if (cursor
< GetSize(todo
))
1328 bad_properties
.push_back(todo
[cursor
++]);
1329 log_assert(cursor
== GetSize(todo
));
1331 int nid
= next_nid
++;
1332 log_assert(cursor
== 0);
1333 log_assert(GetSize(todo
) == 1);
1334 btorf("%d bad %d\n", nid
, todo
[cursor
]);
1338 if (!info_filename
.empty())
1340 for (auto &it
: info_clocks
)
1345 infof("posedge %d\n", it
.first
);
1348 infof("negedge %d\n", it
.first
);
1351 infof("event %d\n", it
.first
);
1359 f
.open(info_filename
.c_str(), std::ofstream::trunc
);
1361 log_error("Can't open file `%s' for writing: %s\n", info_filename
.c_str(), strerror(errno
));
1362 for (auto &it
: info_lines
)
1369 struct BtorBackend
: public Backend
{
1370 BtorBackend() : Backend("btor", "write design to BTOR file") { }
1371 void help() override
1373 // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
1375 log(" write_btor [options] [filename]\n");
1377 log("Write a BTOR description of the current design.\n");
1380 log(" Add comments and indentation to BTOR output file\n");
1383 log(" Output only a single bad property for all asserts\n");
1386 log(" Output cover properties using 'bad' statements instead of asserts\n");
1388 log(" -i <filename>\n");
1389 log(" Create additional info file with auxiliary information\n");
1392 log(" Output symbols for internal netnames (starting with '$')\n");
1395 void execute(std::ostream
*&f
, std::string filename
, std::vector
<std::string
> args
, RTLIL::Design
*design
) override
1397 bool verbose
= false, single_bad
= false, cover_mode
= false, print_internal_names
= false;
1398 string info_filename
;
1400 log_header(design
, "Executing BTOR backend.\n");
1403 Pass::call(design
, "bmuxmap");
1404 Pass::call(design
, "demuxmap");
1408 for (argidx
= 1; argidx
< args
.size(); argidx
++)
1410 if (args
[argidx
] == "-v") {
1414 if (args
[argidx
] == "-s") {
1418 if (args
[argidx
] == "-c") {
1422 if (args
[argidx
] == "-i" && argidx
+1 < args
.size()) {
1423 info_filename
= args
[++argidx
];
1426 if (args
[argidx
] == "-x") {
1427 print_internal_names
= true;
1432 extra_args(f
, filename
, args
, argidx
);
1434 RTLIL::Module
*topmod
= design
->top_module();
1436 if (topmod
== nullptr)
1437 log_cmd_error("No top module found.\n");
1439 *f
<< stringf("; BTOR description generated by %s for module %s.\n",
1440 yosys_version_str
, log_id(topmod
));
1442 BtorWorker(*f
, topmod
, verbose
, single_bad
, cover_mode
, print_internal_names
, info_filename
);
1444 *f
<< stringf("; end of yosys output\n");
1448 PRIVATE_NAMESPACE_END