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
;
43 bool print_internal_names
;
46 int initstate_nid
= -1;
49 dict
<int, int> sorts_bv
;
51 // (<address-width>, <data-width>) => <sid>
52 dict
<pair
<int, int>, int> sorts_mem
;
54 // SigBit => (<nid>, <bitidx>)
55 dict
<SigBit
, pair
<int, int>> bit_nid
;
58 dict
<int, int> nid_width
;
61 dict
<SigSpec
, int> sig_nid
;
63 // bit to driving cell
64 dict
<SigBit
, Cell
*> bit_cell
;
67 dict
<Const
, int> consts
;
69 // ff inputs that need to be evaluated (<nid>, <ff_cell>)
70 vector
<pair
<int, Cell
*>> ff_todo
;
72 pool
<Cell
*> cell_recursion_guard
;
73 vector
<int> bad_properties
;
74 dict
<SigBit
, bool> initbits
;
75 pool
<Wire
*> statewires
;
76 pool
<string
> srcsymbols
;
78 string indent
, info_filename
;
79 vector
<string
> info_lines
;
80 dict
<int, int> info_clocks
;
82 void btorf(const char *fmt
, ...) YS_ATTRIBUTE(format(printf
, 2, 3))
86 f
<< indent
<< vstringf(fmt
, ap
);
90 void infof(const char *fmt
, ...) YS_ATTRIBUTE(format(printf
, 2, 3))
94 info_lines
.push_back(vstringf(fmt
, ap
));
99 string
getinfo(T
*obj
, bool srcsym
= false)
101 string infostr
= log_id(obj
);
102 if (!srcsym
&& !print_internal_names
&& infostr
[0] == '$') return "";
103 if (obj
->attributes
.count(ID::src
)) {
104 string src
= obj
->attributes
.at(ID::src
).decode_string().c_str();
105 if (srcsym
&& infostr
[0] == '$') {
106 std::replace(src
.begin(), src
.end(), ' ', '_');
107 if (srcsymbols
.count(src
) || module
->count_id("\\" + src
)) {
108 for (int i
= 1;; i
++) {
109 string s
= stringf("%s-%d", src
.c_str(), i
);
110 if (!srcsymbols
.count(s
) && !module
->count_id("\\" + s
)) {
116 srcsymbols
.insert(src
);
119 infostr
+= " ; " + src
;
122 return " " + infostr
;
125 void btorf_push(const string
&id
)
128 f
<< indent
<< stringf(" ; begin %s\n", id
.c_str());
133 void btorf_pop(const string
&id
)
136 indent
= indent
.substr(4);
137 f
<< indent
<< stringf(" ; end %s\n", id
.c_str());
141 int get_bv_sid(int width
)
143 if (sorts_bv
.count(width
) == 0) {
144 int nid
= next_nid
++;
145 btorf("%d sort bitvec %d\n", nid
, width
);
146 sorts_bv
[width
] = nid
;
148 return sorts_bv
.at(width
);
151 int get_mem_sid(int abits
, int dbits
)
153 pair
<int, int> key(abits
, dbits
);
154 if (sorts_mem
.count(key
) == 0) {
155 int addr_sid
= get_bv_sid(abits
);
156 int data_sid
= get_bv_sid(dbits
);
157 int nid
= next_nid
++;
158 btorf("%d sort array %d %d\n", nid
, addr_sid
, data_sid
);
159 sorts_mem
[key
] = nid
;
161 return sorts_mem
.at(key
);
164 void add_nid_sig(int nid
, const SigSpec
&sig
)
167 f
<< indent
<< stringf("; %d %s\n", nid
, log_signal(sig
));
169 for (int i
= 0; i
< GetSize(sig
); i
++)
170 bit_nid
[sig
[i
]] = make_pair(nid
, i
);
173 nid_width
[nid
] = GetSize(sig
);
176 void export_cell(Cell
*cell
)
178 if (cell_recursion_guard
.count(cell
)) {
180 for (auto c
: cell_recursion_guard
)
181 cell_list
+= stringf("\n %s", log_id(c
));
182 log_error("Found topological loop while processing cell %s. Active cells:%s\n", log_id(cell
), cell_list
.c_str());
185 cell_recursion_guard
.insert(cell
);
186 btorf_push(log_id(cell
));
188 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
),
189 ID($concat
), ID($_AND_
), ID($_NAND_
), ID($_OR_
), ID($_NOR_
), ID($_XOR_
), ID($_XNOR_
)))
192 if (cell
->type
== ID($add
)) btor_op
= "add";
193 if (cell
->type
== ID($sub
)) btor_op
= "sub";
194 if (cell
->type
== ID($mul
)) btor_op
= "mul";
195 if (cell
->type
.in(ID($shl
), ID($sshl
))) btor_op
= "sll";
196 if (cell
->type
== ID($shr
)) btor_op
= "srl";
197 if (cell
->type
== ID($sshr
)) btor_op
= "sra";
198 if (cell
->type
.in(ID($shift
), ID($shiftx
))) btor_op
= "shift";
199 if (cell
->type
.in(ID($
and), ID($_AND_
))) btor_op
= "and";
200 if (cell
->type
.in(ID($
or), ID($_OR_
))) btor_op
= "or";
201 if (cell
->type
.in(ID($
xor), ID($_XOR_
))) btor_op
= "xor";
202 if (cell
->type
== ID($concat
)) btor_op
= "concat";
203 if (cell
->type
== ID($_NAND_
)) btor_op
= "nand";
204 if (cell
->type
== ID($_NOR_
)) btor_op
= "nor";
205 if (cell
->type
.in(ID($xnor
), ID($_XNOR_
))) btor_op
= "xnor";
206 log_assert(!btor_op
.empty());
208 int width
= GetSize(cell
->getPort(ID::Y
));
209 width
= std::max(width
, GetSize(cell
->getPort(ID::A
)));
210 width
= std::max(width
, GetSize(cell
->getPort(ID::B
)));
212 bool a_signed
= cell
->hasParam(ID::A_SIGNED
) ? cell
->getParam(ID::A_SIGNED
).as_bool() : false;
213 bool b_signed
= cell
->hasParam(ID::B_SIGNED
) ? cell
->getParam(ID::B_SIGNED
).as_bool() : false;
215 if (btor_op
== "shift" && !b_signed
)
218 if (cell
->type
.in(ID($shl
), ID($sshl
), ID($shr
), ID($sshr
)))
221 if (cell
->type
== ID($sshr
) && !a_signed
)
224 int sid
= get_bv_sid(width
);
227 if (btor_op
== "shift")
229 int nid_a
= get_sig_nid(cell
->getPort(ID::A
), width
, false);
230 int nid_b
= get_sig_nid(cell
->getPort(ID::B
), width
, b_signed
);
232 int nid_r
= next_nid
++;
233 btorf("%d srl %d %d %d\n", nid_r
, sid
, nid_a
, nid_b
);
235 int nid_b_neg
= next_nid
++;
236 btorf("%d neg %d %d\n", nid_b_neg
, sid
, nid_b
);
238 int nid_l
= next_nid
++;
239 btorf("%d sll %d %d %d\n", nid_l
, sid
, nid_a
, nid_b_neg
);
241 int sid_bit
= get_bv_sid(1);
242 int nid_zero
= get_sig_nid(Const(0, width
));
243 int nid_b_ltz
= next_nid
++;
244 btorf("%d slt %d %d %d\n", nid_b_ltz
, sid_bit
, nid_b
, nid_zero
);
247 btorf("%d ite %d %d %d %d%s\n", nid
, sid
, nid_b_ltz
, nid_l
, nid_r
, getinfo(cell
).c_str());
251 int nid_a
= get_sig_nid(cell
->getPort(ID::A
), width
, a_signed
);
252 int nid_b
= get_sig_nid(cell
->getPort(ID::B
), width
, b_signed
);
255 btorf("%d %s %d %d %d%s\n", nid
, btor_op
.c_str(), sid
, nid_a
, nid_b
, getinfo(cell
).c_str());
258 SigSpec sig
= sigmap(cell
->getPort(ID::Y
));
260 if (GetSize(sig
) < width
) {
261 int sid
= get_bv_sid(GetSize(sig
));
262 int nid2
= next_nid
++;
263 btorf("%d slice %d %d %d 0\n", nid2
, sid
, nid
, GetSize(sig
)-1);
267 add_nid_sig(nid
, sig
);
271 if (cell
->type
.in(ID($div
), ID($mod
), ID($modfloor
)))
273 bool a_signed
= cell
->hasParam(ID::A_SIGNED
) ? cell
->getParam(ID::A_SIGNED
).as_bool() : false;
274 bool b_signed
= cell
->hasParam(ID::B_SIGNED
) ? cell
->getParam(ID::B_SIGNED
).as_bool() : false;
277 if (cell
->type
== ID($div
)) btor_op
= "div";
278 // "rem" = truncating modulo
279 if (cell
->type
== ID($mod
)) btor_op
= "rem";
280 // "mod" = flooring modulo
281 if (cell
->type
== ID($modfloor
)) {
282 // "umod" doesn't exist because it's the same as "urem"
283 btor_op
= a_signed
|| b_signed
? "mod" : "rem";
285 log_assert(!btor_op
.empty());
287 int width
= GetSize(cell
->getPort(ID::Y
));
288 width
= std::max(width
, GetSize(cell
->getPort(ID::A
)));
289 width
= std::max(width
, GetSize(cell
->getPort(ID::B
)));
291 int nid_a
= get_sig_nid(cell
->getPort(ID::A
), width
, a_signed
);
292 int nid_b
= get_sig_nid(cell
->getPort(ID::B
), width
, b_signed
);
294 int sid
= get_bv_sid(width
);
295 int nid
= next_nid
++;
296 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());
298 SigSpec sig
= sigmap(cell
->getPort(ID::Y
));
300 if (GetSize(sig
) < width
) {
301 int sid
= get_bv_sid(GetSize(sig
));
302 int nid2
= next_nid
++;
303 btorf("%d slice %d %d %d 0\n", nid2
, sid
, nid
, GetSize(sig
)-1);
307 add_nid_sig(nid
, sig
);
311 if (cell
->type
.in(ID($_ANDNOT_
), ID($_ORNOT_
)))
313 int sid
= get_bv_sid(1);
314 int nid_a
= get_sig_nid(cell
->getPort(ID::A
));
315 int nid_b
= get_sig_nid(cell
->getPort(ID::B
));
317 int nid1
= next_nid
++;
318 int nid2
= next_nid
++;
320 if (cell
->type
== ID($_ANDNOT_
)) {
321 btorf("%d not %d %d\n", nid1
, sid
, nid_b
);
322 btorf("%d and %d %d %d%s\n", nid2
, sid
, nid_a
, nid1
, getinfo(cell
).c_str());
325 if (cell
->type
== ID($_ORNOT_
)) {
326 btorf("%d not %d %d\n", nid1
, sid
, nid_b
);
327 btorf("%d or %d %d %d%s\n", nid2
, sid
, nid_a
, nid1
, getinfo(cell
).c_str());
330 SigSpec sig
= sigmap(cell
->getPort(ID::Y
));
331 add_nid_sig(nid2
, sig
);
335 if (cell
->type
.in(ID($_OAI3_
), ID($_AOI3_
)))
337 int sid
= get_bv_sid(1);
338 int nid_a
= get_sig_nid(cell
->getPort(ID::A
));
339 int nid_b
= get_sig_nid(cell
->getPort(ID::B
));
340 int nid_c
= get_sig_nid(cell
->getPort(ID::C
));
342 int nid1
= next_nid
++;
343 int nid2
= next_nid
++;
344 int nid3
= next_nid
++;
346 if (cell
->type
== ID($_OAI3_
)) {
347 btorf("%d or %d %d %d\n", nid1
, sid
, nid_a
, nid_b
);
348 btorf("%d and %d %d %d\n", nid2
, sid
, nid1
, nid_c
);
349 btorf("%d not %d %d%s\n", nid3
, sid
, nid2
, getinfo(cell
).c_str());
352 if (cell
->type
== ID($_AOI3_
)) {
353 btorf("%d and %d %d %d\n", nid1
, sid
, nid_a
, nid_b
);
354 btorf("%d or %d %d %d\n", nid2
, sid
, nid1
, nid_c
);
355 btorf("%d not %d %d%s\n", nid3
, sid
, nid2
, getinfo(cell
).c_str());
358 SigSpec sig
= sigmap(cell
->getPort(ID::Y
));
359 add_nid_sig(nid3
, sig
);
363 if (cell
->type
.in(ID($_OAI4_
), ID($_AOI4_
)))
365 int sid
= get_bv_sid(1);
366 int nid_a
= get_sig_nid(cell
->getPort(ID::A
));
367 int nid_b
= get_sig_nid(cell
->getPort(ID::B
));
368 int nid_c
= get_sig_nid(cell
->getPort(ID::C
));
369 int nid_d
= get_sig_nid(cell
->getPort(ID::D
));
371 int nid1
= next_nid
++;
372 int nid2
= next_nid
++;
373 int nid3
= next_nid
++;
374 int nid4
= next_nid
++;
376 if (cell
->type
== ID($_OAI4_
)) {
377 btorf("%d or %d %d %d\n", nid1
, sid
, nid_a
, nid_b
);
378 btorf("%d or %d %d %d\n", nid2
, sid
, nid_c
, nid_d
);
379 btorf("%d and %d %d %d\n", nid3
, sid
, nid1
, nid2
);
380 btorf("%d not %d %d%s\n", nid4
, sid
, nid3
, getinfo(cell
).c_str());
383 if (cell
->type
== ID($_AOI4_
)) {
384 btorf("%d and %d %d %d\n", nid1
, sid
, nid_a
, nid_b
);
385 btorf("%d and %d %d %d\n", nid2
, sid
, nid_c
, nid_d
);
386 btorf("%d or %d %d %d\n", nid3
, sid
, nid1
, nid2
);
387 btorf("%d not %d %d%s\n", nid4
, sid
, nid3
, getinfo(cell
).c_str());
390 SigSpec sig
= sigmap(cell
->getPort(ID::Y
));
391 add_nid_sig(nid4
, sig
);
395 if (cell
->type
.in(ID($lt
), ID($le
), ID($eq
), ID($eqx
), ID($ne
), ID($nex
), ID($ge
), ID($gt
)))
398 if (cell
->type
== ID($lt
)) btor_op
= "lt";
399 if (cell
->type
== ID($le
)) btor_op
= "lte";
400 if (cell
->type
.in(ID($eq
), ID($eqx
))) btor_op
= "eq";
401 if (cell
->type
.in(ID($ne
), ID($nex
))) btor_op
= "neq";
402 if (cell
->type
== ID($ge
)) btor_op
= "gte";
403 if (cell
->type
== ID($gt
)) btor_op
= "gt";
404 log_assert(!btor_op
.empty());
407 width
= std::max(width
, GetSize(cell
->getPort(ID::A
)));
408 width
= std::max(width
, GetSize(cell
->getPort(ID::B
)));
410 bool a_signed
= cell
->hasParam(ID::A_SIGNED
) ? cell
->getParam(ID::A_SIGNED
).as_bool() : false;
411 bool b_signed
= cell
->hasParam(ID::B_SIGNED
) ? cell
->getParam(ID::B_SIGNED
).as_bool() : false;
413 int sid
= get_bv_sid(1);
414 int nid_a
= get_sig_nid(cell
->getPort(ID::A
), width
, a_signed
);
415 int nid_b
= get_sig_nid(cell
->getPort(ID::B
), width
, b_signed
);
417 int nid
= next_nid
++;
418 if (cell
->type
.in(ID($lt
), ID($le
), ID($ge
), ID($gt
))) {
419 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());
421 btorf("%d %s %d %d %d%s\n", nid
, btor_op
.c_str(), sid
, nid_a
, nid_b
, getinfo(cell
).c_str());
424 SigSpec sig
= sigmap(cell
->getPort(ID::Y
));
426 if (GetSize(sig
) > 1) {
427 int sid
= get_bv_sid(GetSize(sig
));
428 int nid2
= next_nid
++;
429 btorf("%d uext %d %d %d\n", nid2
, sid
, nid
, GetSize(sig
) - 1);
433 add_nid_sig(nid
, sig
);
437 if (cell
->type
.in(ID($
not), ID($neg
), ID($_NOT_
)))
440 if (cell
->type
.in(ID($
not), ID($_NOT_
))) btor_op
= "not";
441 if (cell
->type
== ID($neg
)) btor_op
= "neg";
442 log_assert(!btor_op
.empty());
444 int width
= std::max(GetSize(cell
->getPort(ID::A
)), GetSize(cell
->getPort(ID::Y
)));
446 bool a_signed
= cell
->hasParam(ID::A_SIGNED
) ? cell
->getParam(ID::A_SIGNED
).as_bool() : false;
448 int sid
= get_bv_sid(width
);
449 int nid_a
= get_sig_nid(cell
->getPort(ID::A
), width
, a_signed
);
451 int nid
= next_nid
++;
452 btorf("%d %s %d %d%s\n", nid
, btor_op
.c_str(), sid
, nid_a
, getinfo(cell
).c_str());
454 SigSpec sig
= sigmap(cell
->getPort(ID::Y
));
456 if (GetSize(sig
) < width
) {
457 int sid
= get_bv_sid(GetSize(sig
));
458 int nid2
= next_nid
++;
459 btorf("%d slice %d %d %d 0\n", nid2
, sid
, nid
, GetSize(sig
)-1);
463 add_nid_sig(nid
, sig
);
467 if (cell
->type
.in(ID($logic_and
), ID($logic_or
), ID($logic_not
)))
470 if (cell
->type
== ID($logic_and
)) btor_op
= "and";
471 if (cell
->type
== ID($logic_or
)) btor_op
= "or";
472 if (cell
->type
== ID($logic_not
)) btor_op
= "not";
473 log_assert(!btor_op
.empty());
475 int sid
= get_bv_sid(1);
476 int nid_a
= get_sig_nid(cell
->getPort(ID::A
));
477 int nid_b
= btor_op
!= "not" ? get_sig_nid(cell
->getPort(ID::B
)) : 0;
479 if (GetSize(cell
->getPort(ID::A
)) > 1) {
480 int nid_red_a
= next_nid
++;
481 btorf("%d redor %d %d\n", nid_red_a
, sid
, nid_a
);
485 if (btor_op
!= "not" && GetSize(cell
->getPort(ID::B
)) > 1) {
486 int nid_red_b
= next_nid
++;
487 btorf("%d redor %d %d\n", nid_red_b
, sid
, nid_b
);
491 int nid
= next_nid
++;
492 if (btor_op
!= "not")
493 btorf("%d %s %d %d %d%s\n", nid
, btor_op
.c_str(), sid
, nid_a
, nid_b
, getinfo(cell
).c_str());
495 btorf("%d %s %d %d%s\n", nid
, btor_op
.c_str(), sid
, nid_a
, getinfo(cell
).c_str());
497 SigSpec sig
= sigmap(cell
->getPort(ID::Y
));
499 if (GetSize(sig
) > 1) {
500 int sid
= get_bv_sid(GetSize(sig
));
501 int zeros_nid
= get_sig_nid(Const(0, GetSize(sig
)-1));
502 int nid2
= next_nid
++;
503 btorf("%d concat %d %d %d\n", nid2
, sid
, zeros_nid
, nid
);
507 add_nid_sig(nid
, sig
);
511 if (cell
->type
.in(ID($reduce_and
), ID($reduce_or
), ID($reduce_bool
), ID($reduce_xor
), ID($reduce_xnor
)))
514 if (cell
->type
== ID($reduce_and
)) btor_op
= "redand";
515 if (cell
->type
.in(ID($reduce_or
), ID($reduce_bool
))) btor_op
= "redor";
516 if (cell
->type
.in(ID($reduce_xor
), ID($reduce_xnor
))) btor_op
= "redxor";
517 log_assert(!btor_op
.empty());
519 int sid
= get_bv_sid(1);
520 int nid_a
= get_sig_nid(cell
->getPort(ID::A
));
522 int nid
= next_nid
++;
524 if (cell
->type
== ID($reduce_xnor
)) {
525 int nid2
= next_nid
++;
526 btorf("%d %s %d %d%s\n", nid
, btor_op
.c_str(), sid
, nid_a
, getinfo(cell
).c_str());
527 btorf("%d not %d %d\n", nid2
, sid
, nid
);
530 btorf("%d %s %d %d%s\n", nid
, btor_op
.c_str(), sid
, nid_a
, getinfo(cell
).c_str());
533 SigSpec sig
= sigmap(cell
->getPort(ID::Y
));
535 if (GetSize(sig
) > 1) {
536 int sid
= get_bv_sid(GetSize(sig
));
537 int zeros_nid
= get_sig_nid(Const(0, GetSize(sig
)-1));
538 int nid2
= next_nid
++;
539 btorf("%d concat %d %d %d\n", nid2
, sid
, zeros_nid
, nid
);
543 add_nid_sig(nid
, sig
);
547 if (cell
->type
.in(ID($mux
), ID($_MUX_
), ID($_NMUX_
)))
549 SigSpec sig_a
= sigmap(cell
->getPort(ID::A
));
550 SigSpec sig_b
= sigmap(cell
->getPort(ID::B
));
551 SigSpec sig_s
= sigmap(cell
->getPort(ID::S
));
552 SigSpec sig_y
= sigmap(cell
->getPort(ID::Y
));
554 int nid_a
= get_sig_nid(sig_a
);
555 int nid_b
= get_sig_nid(sig_b
);
556 int nid_s
= get_sig_nid(sig_s
);
558 int sid
= get_bv_sid(GetSize(sig_y
));
559 int nid
= next_nid
++;
561 if (cell
->type
== ID($_NMUX_
)) {
564 btorf("%d ite %d %d %d %d\n", tmp
, sid
, nid_s
, nid_b
, nid_a
);
565 btorf("%d not %d %d%s\n", nid
, sid
, tmp
, getinfo(cell
).c_str());
567 btorf("%d ite %d %d %d %d%s\n", nid
, sid
, nid_s
, nid_b
, nid_a
, getinfo(cell
).c_str());
570 add_nid_sig(nid
, sig_y
);
574 if (cell
->type
== ID($pmux
))
576 SigSpec sig_a
= sigmap(cell
->getPort(ID::A
));
577 SigSpec sig_b
= sigmap(cell
->getPort(ID::B
));
578 SigSpec sig_s
= sigmap(cell
->getPort(ID::S
));
579 SigSpec sig_y
= sigmap(cell
->getPort(ID::Y
));
581 int width
= GetSize(sig_a
);
582 int sid
= get_bv_sid(width
);
583 int nid
= get_sig_nid(sig_a
);
585 for (int i
= 0; i
< GetSize(sig_s
); i
++) {
586 int nid_b
= get_sig_nid(sig_b
.extract(i
*width
, width
));
587 int nid_s
= get_sig_nid(sig_s
.extract(i
));
588 int nid2
= next_nid
++;
589 if (i
== GetSize(sig_s
)-1)
590 btorf("%d ite %d %d %d %d%s\n", nid2
, sid
, nid_s
, nid_b
, nid
, getinfo(cell
).c_str());
592 btorf("%d ite %d %d %d %d\n", nid2
, sid
, nid_s
, nid_b
, nid
);
596 add_nid_sig(nid
, sig_y
);
600 if (cell
->type
.in(ID($dff
), ID($ff
), ID($_DFF_P_
), ID($_DFF_N
), ID($_FF_
)))
602 SigSpec sig_d
= sigmap(cell
->getPort(ID::D
));
603 SigSpec sig_q
= sigmap(cell
->getPort(ID::Q
));
605 if (!info_filename
.empty() && cell
->type
.in(ID($dff
), ID($_DFF_P_
), ID($_DFF_N_
)))
607 SigSpec sig_c
= sigmap(cell
->getPort(cell
->type
== ID($dff
) ? ID::CLK
: ID::C
));
608 int nid
= get_sig_nid(sig_c
);
609 bool negedge
= false;
611 if (cell
->type
== ID($_DFF_N_
))
614 if (cell
->type
== ID($dff
) && !cell
->getParam(ID::CLK_POLARITY
).as_bool())
617 info_clocks
[nid
] |= negedge
? 2 : 1;
622 if (sig_q
.is_wire()) {
623 Wire
*w
= sig_q
.as_wire();
624 if (w
->port_id
== 0) {
625 statewires
.insert(w
);
631 for (int i
= 0; i
< GetSize(sig_q
); i
++)
632 if (initbits
.count(sig_q
[i
]))
633 initval
.bits
.push_back(initbits
.at(sig_q
[i
]) ? State::S1
: State::S0
);
635 initval
.bits
.push_back(State::Sx
);
637 int nid_init_val
= -1;
639 if (!initval
.is_fully_undef())
640 nid_init_val
= get_sig_nid(initval
, -1, false, true);
642 int sid
= get_bv_sid(GetSize(sig_q
));
643 int nid
= next_nid
++;
645 if (symbol
.empty() || (!print_internal_names
&& symbol
[0] == '$'))
646 btorf("%d state %d\n", nid
, sid
);
648 btorf("%d state %d %s\n", nid
, sid
, log_id(symbol
));
650 if (nid_init_val
>= 0) {
651 int nid_init
= next_nid
++;
653 btorf("; initval = %s\n", log_signal(initval
));
654 btorf("%d init %d %d %d\n", nid_init
, sid
, nid
, nid_init_val
);
657 ff_todo
.push_back(make_pair(nid
, cell
));
658 add_nid_sig(nid
, sig_q
);
662 if (cell
->type
.in(ID($anyconst
), ID($anyseq
)))
664 SigSpec sig_y
= sigmap(cell
->getPort(ID::Y
));
666 int sid
= get_bv_sid(GetSize(sig_y
));
667 int nid
= next_nid
++;
669 btorf("%d state %d\n", nid
, sid
);
671 if (cell
->type
== ID($anyconst
)) {
672 int nid2
= next_nid
++;
673 btorf("%d next %d %d %d\n", nid2
, sid
, nid
, nid
);
676 add_nid_sig(nid
, sig_y
);
680 if (cell
->type
== ID($initstate
))
682 SigSpec sig_y
= sigmap(cell
->getPort(ID::Y
));
684 if (initstate_nid
< 0)
686 int sid
= get_bv_sid(1);
687 int one_nid
= get_sig_nid(State::S1
);
688 int zero_nid
= get_sig_nid(State::S0
);
689 initstate_nid
= next_nid
++;
690 btorf("%d state %d\n", initstate_nid
, sid
);
691 btorf("%d init %d %d %d\n", next_nid
++, sid
, initstate_nid
, one_nid
);
692 btorf("%d next %d %d %d\n", next_nid
++, sid
, initstate_nid
, zero_nid
);
695 add_nid_sig(initstate_nid
, sig_y
);
699 if (cell
->type
== ID($mem
))
701 int abits
= cell
->getParam(ID::ABITS
).as_int();
702 int width
= cell
->getParam(ID::WIDTH
).as_int();
703 int nwords
= cell
->getParam(ID::SIZE
).as_int();
704 int rdports
= cell
->getParam(ID::RD_PORTS
).as_int();
705 int wrports
= cell
->getParam(ID::WR_PORTS
).as_int();
707 Const wr_clk_en
= cell
->getParam(ID::WR_CLK_ENABLE
);
708 Const rd_clk_en
= cell
->getParam(ID::RD_CLK_ENABLE
);
710 bool asyncwr
= wr_clk_en
.is_fully_zero();
712 if (!asyncwr
&& !wr_clk_en
.is_fully_ones())
713 log_error("Memory %s.%s has mixed async/sync write ports.\n",
714 log_id(module
), log_id(cell
));
716 if (!rd_clk_en
.is_fully_zero())
717 log_error("Memory %s.%s has sync read ports.\n",
718 log_id(module
), log_id(cell
));
720 SigSpec sig_rd_addr
= sigmap(cell
->getPort(ID::RD_ADDR
));
721 SigSpec sig_rd_data
= sigmap(cell
->getPort(ID::RD_DATA
));
723 SigSpec sig_wr_addr
= sigmap(cell
->getPort(ID::WR_ADDR
));
724 SigSpec sig_wr_data
= sigmap(cell
->getPort(ID::WR_DATA
));
725 SigSpec sig_wr_en
= sigmap(cell
->getPort(ID::WR_EN
));
727 int data_sid
= get_bv_sid(width
);
728 int bool_sid
= get_bv_sid(1);
729 int sid
= get_mem_sid(abits
, width
);
731 Const initdata
= cell
->getParam(ID::INIT
);
732 initdata
.exts(nwords
*width
);
733 int nid_init_val
= -1;
735 if (!initdata
.is_fully_undef())
737 bool constword
= true;
738 Const firstword
= initdata
.extract(0, width
);
740 for (int i
= 1; i
< nwords
; i
++) {
741 Const thisword
= initdata
.extract(i
*width
, width
);
742 if (thisword
!= firstword
) {
751 btorf("; initval = %s\n", log_signal(firstword
));
752 nid_init_val
= get_sig_nid(firstword
, -1, false, true);
756 nid_init_val
= next_nid
++;
757 btorf("%d state %d\n", nid_init_val
, sid
);
759 for (int i
= 0; i
< nwords
; i
++) {
760 Const thisword
= initdata
.extract(i
*width
, width
);
761 if (thisword
.is_fully_undef())
763 Const
thisaddr(i
, abits
);
764 int nid_thisword
= get_sig_nid(thisword
, -1, false, true);
765 int nid_thisaddr
= get_sig_nid(thisaddr
, -1, false, true);
766 int last_nid_init_val
= nid_init_val
;
767 nid_init_val
= next_nid
++;
769 btorf("; initval[%d] = %s\n", i
, log_signal(thisword
));
770 btorf("%d write %d %d %d %d\n", nid_init_val
, sid
, last_nid_init_val
, nid_thisaddr
, nid_thisword
);
776 int nid
= next_nid
++;
779 if (cell
->name
[0] == '$')
780 btorf("%d state %d\n", nid
, sid
);
782 btorf("%d state %d %s\n", nid
, sid
, log_id(cell
));
784 if (nid_init_val
>= 0)
786 int nid_init
= next_nid
++;
787 btorf("%d init %d %d %d\n", nid_init
, sid
, nid
, nid_init_val
);
792 for (int port
= 0; port
< wrports
; port
++)
794 SigSpec wa
= sig_wr_addr
.extract(port
*abits
, abits
);
795 SigSpec wd
= sig_wr_data
.extract(port
*width
, width
);
796 SigSpec we
= sig_wr_en
.extract(port
*width
, width
);
798 int wa_nid
= get_sig_nid(wa
);
799 int wd_nid
= get_sig_nid(wd
);
800 int we_nid
= get_sig_nid(we
);
802 int nid2
= next_nid
++;
803 btorf("%d read %d %d %d\n", nid2
, data_sid
, nid_head
, wa_nid
);
805 int nid3
= next_nid
++;
806 btorf("%d not %d %d\n", nid3
, data_sid
, we_nid
);
808 int nid4
= next_nid
++;
809 btorf("%d and %d %d %d\n", nid4
, data_sid
, nid2
, nid3
);
811 int nid5
= next_nid
++;
812 btorf("%d and %d %d %d\n", nid5
, data_sid
, wd_nid
, we_nid
);
814 int nid6
= next_nid
++;
815 btorf("%d or %d %d %d\n", nid6
, data_sid
, nid5
, nid4
);
817 int nid7
= next_nid
++;
818 btorf("%d write %d %d %d %d\n", nid7
, sid
, nid_head
, wa_nid
, nid6
);
820 int nid8
= next_nid
++;
821 btorf("%d redor %d %d\n", nid8
, bool_sid
, we_nid
);
823 int nid9
= next_nid
++;
824 btorf("%d ite %d %d %d %d\n", nid9
, sid
, nid8
, nid7
, nid_head
);
830 for (int port
= 0; port
< rdports
; port
++)
832 SigSpec ra
= sig_rd_addr
.extract(port
*abits
, abits
);
833 SigSpec rd
= sig_rd_data
.extract(port
*width
, width
);
835 int ra_nid
= get_sig_nid(ra
);
836 int rd_nid
= next_nid
++;
838 btorf("%d read %d %d %d\n", rd_nid
, data_sid
, nid_head
, ra_nid
);
840 add_nid_sig(rd_nid
, rd
);
845 ff_todo
.push_back(make_pair(nid
, cell
));
849 int nid2
= next_nid
++;
850 btorf("%d next %d %d %d\n", nid2
, sid
, nid
, nid_head
);
856 log_error("Unsupported cell type: %s (%s)\n", log_id(cell
->type
), log_id(cell
));
859 btorf_pop(log_id(cell
));
860 cell_recursion_guard
.erase(cell
);
863 int get_sig_nid(SigSpec sig
, int to_width
= -1, bool is_signed
= false, bool is_init
= false)
869 if (bit
== State::Sx
)
875 SigSpec sig_mask_undef
, sig_noundef
;
876 int first_undef
= -1;
878 for (int i
= 0; i
< GetSize(sig
); i
++)
879 if (sig
[i
] == State::Sx
) {
882 sig_mask_undef
.append(State::S1
);
883 sig_noundef
.append(State::S0
);
885 sig_mask_undef
.append(State::S0
);
886 sig_noundef
.append(sig
[i
]);
889 if (to_width
< 0 || first_undef
< to_width
)
891 int sid
= get_bv_sid(GetSize(sig
));
893 int nid_input
= next_nid
++;
895 btorf("%d state %d\n", nid_input
, sid
);
897 btorf("%d input %d\n", nid_input
, sid
);
899 int nid_masked_input
;
900 if (sig_mask_undef
.is_fully_ones()) {
901 nid_masked_input
= nid_input
;
903 int nid_mask_undef
= get_sig_nid(sig_mask_undef
);
904 nid_masked_input
= next_nid
++;
905 btorf("%d and %d %d %d\n", nid_masked_input
, sid
, nid_input
, nid_mask_undef
);
908 if (sig_noundef
.is_fully_zero()) {
909 nid
= nid_masked_input
;
911 int nid_noundef
= get_sig_nid(sig_noundef
);
913 btorf("%d or %d %d %d\n", nid
, sid
, nid_masked_input
, nid_noundef
);
922 if (sig_nid
.count(sig
) == 0)
925 vector
<pair
<int, int>> nidbits
;
928 for (int i
= 0; i
< GetSize(sig
); i
++)
932 if (bit_nid
.count(bit
) == 0)
934 if (bit
.wire
== nullptr)
938 while (i
+GetSize(c
) < GetSize(sig
) && sig
[i
+GetSize(c
)].wire
== nullptr)
939 c
.bits
.push_back(sig
[i
+GetSize(c
)].data
);
941 if (consts
.count(c
) == 0) {
942 int sid
= get_bv_sid(GetSize(c
));
943 int nid
= next_nid
++;
944 btorf("%d const %d %s\n", nid
, sid
, c
.as_string().c_str());
946 nid_width
[nid
] = GetSize(c
);
949 int nid
= consts
.at(c
);
951 for (int j
= 0; j
< GetSize(c
); j
++)
952 nidbits
.push_back(make_pair(nid
, j
));
959 if (bit_cell
.count(bit
) == 0)
963 while (i
+GetSize(s
) < GetSize(sig
) && sig
[i
+GetSize(s
)].wire
!= nullptr &&
964 bit_cell
.count(sig
[i
+GetSize(s
)]) == 0)
965 s
.append(sig
[i
+GetSize(s
)]);
967 log_warning("No driver for signal %s.\n", log_signal(s
));
969 int sid
= get_bv_sid(GetSize(s
));
970 int nid
= next_nid
++;
971 btorf("%d input %d\n", nid
, sid
);
972 nid_width
[nid
] = GetSize(s
);
974 for (int j
= 0; j
< GetSize(s
); j
++)
975 nidbits
.push_back(make_pair(nid
, j
));
982 export_cell(bit_cell
.at(bit
));
983 log_assert(bit_nid
.count(bit
));
988 nidbits
.push_back(bit_nid
.at(bit
));
994 // group bits and emit slice-concat chain
995 for (int i
= 0; i
< GetSize(nidbits
); i
++)
997 int nid2
= nidbits
[i
].first
;
998 int lower
= nidbits
[i
].second
;
1001 while (i
+1 < GetSize(nidbits
) && nidbits
[i
+1].first
== nidbits
[i
].first
&&
1002 nidbits
[i
+1].second
== nidbits
[i
].second
+1)
1007 if (lower
!= 0 || upper
+1 != nid_width
.at(nid2
)) {
1008 int sid
= get_bv_sid(upper
-lower
+1);
1010 btorf("%d slice %d %d %d %d\n", nid3
, sid
, nid2
, upper
, lower
);
1016 int sid
= get_bv_sid(width
+upper
-lower
+1);
1018 btorf("%d concat %d %d %d\n", nid4
, sid
, nid3
, nid
);
1021 width
+= upper
-lower
+1;
1026 nid_width
[nid
] = width
;
1029 nid
= sig_nid
.at(sig
);
1032 if (to_width
>= 0 && to_width
!= GetSize(sig
))
1034 if (to_width
< GetSize(sig
))
1036 int sid
= get_bv_sid(to_width
);
1037 int nid2
= next_nid
++;
1038 btorf("%d slice %d %d %d 0\n", nid2
, sid
, nid
, to_width
-1);
1043 int sid
= get_bv_sid(to_width
);
1044 int nid2
= next_nid
++;
1045 btorf("%d %s %d %d %d\n", nid2
, is_signed
? "sext" : "uext",
1046 sid
, nid
, to_width
- GetSize(sig
));
1054 BtorWorker(std::ostream
&f
, RTLIL::Module
*module
, bool verbose
, bool single_bad
, bool cover_mode
, bool print_internal_names
, string info_filename
) :
1055 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
)
1057 if (!info_filename
.empty())
1058 infof("name %s\n", log_id(module
));
1060 btorf_push("inputs");
1062 for (auto wire
: module
->wires())
1064 if (wire
->attributes
.count(ID::init
)) {
1065 Const attrval
= wire
->attributes
.at(ID::init
);
1066 for (int i
= 0; i
< GetSize(wire
) && i
< GetSize(attrval
); i
++)
1067 if (attrval
[i
] == State::S0
|| attrval
[i
] == State::S1
)
1068 initbits
[sigmap(SigBit(wire
, i
))] = (attrval
[i
] == State::S1
);
1071 if (!wire
->port_id
|| !wire
->port_input
)
1074 SigSpec sig
= sigmap(wire
);
1075 int sid
= get_bv_sid(GetSize(sig
));
1076 int nid
= next_nid
++;
1078 btorf("%d input %d%s\n", nid
, sid
, getinfo(wire
).c_str());
1079 add_nid_sig(nid
, sig
);
1082 btorf_pop("inputs");
1084 for (auto cell
: module
->cells())
1085 for (auto &conn
: cell
->connections())
1087 if (!cell
->output(conn
.first
))
1090 for (auto bit
: sigmap(conn
.second
))
1091 bit_cell
[bit
] = cell
;
1094 for (auto wire
: module
->wires())
1096 if (!wire
->port_id
|| !wire
->port_output
)
1099 btorf_push(stringf("output %s", log_id(wire
)));
1101 int nid
= get_sig_nid(wire
);
1102 btorf("%d output %d%s\n", next_nid
++, nid
, getinfo(wire
).c_str());
1104 btorf_pop(stringf("output %s", log_id(wire
)));
1107 for (auto cell
: module
->cells())
1109 if (cell
->type
== ID($assume
))
1111 btorf_push(log_id(cell
));
1113 int sid
= get_bv_sid(1);
1114 int nid_a
= get_sig_nid(cell
->getPort(ID::A
));
1115 int nid_en
= get_sig_nid(cell
->getPort(ID::EN
));
1116 int nid_not_en
= next_nid
++;
1117 int nid_a_or_not_en
= next_nid
++;
1118 int nid
= next_nid
++;
1120 btorf("%d not %d %d\n", nid_not_en
, sid
, nid_en
);
1121 btorf("%d or %d %d %d\n", nid_a_or_not_en
, sid
, nid_a
, nid_not_en
);
1122 btorf("%d constraint %d\n", nid
, nid_a_or_not_en
);
1124 btorf_pop(log_id(cell
));
1127 if (cell
->type
== ID($
assert))
1129 btorf_push(log_id(cell
));
1131 int sid
= get_bv_sid(1);
1132 int nid_a
= get_sig_nid(cell
->getPort(ID::A
));
1133 int nid_en
= get_sig_nid(cell
->getPort(ID::EN
));
1134 int nid_not_a
= next_nid
++;
1135 int nid_en_and_not_a
= next_nid
++;
1137 btorf("%d not %d %d\n", nid_not_a
, sid
, nid_a
);
1138 btorf("%d and %d %d %d\n", nid_en_and_not_a
, sid
, nid_en
, nid_not_a
);
1140 if (single_bad
&& !cover_mode
) {
1141 bad_properties
.push_back(nid_en_and_not_a
);
1144 infof("bad %d%s\n", nid_en_and_not_a
, getinfo(cell
, true).c_str());
1146 int nid
= next_nid
++;
1147 btorf("%d bad %d%s\n", nid
, nid_en_and_not_a
, getinfo(cell
, true).c_str());
1151 btorf_pop(log_id(cell
));
1154 if (cell
->type
== ID($cover
) && cover_mode
)
1156 btorf_push(log_id(cell
));
1158 int sid
= get_bv_sid(1);
1159 int nid_a
= get_sig_nid(cell
->getPort(ID::A
));
1160 int nid_en
= get_sig_nid(cell
->getPort(ID::EN
));
1161 int nid_en_and_a
= next_nid
++;
1163 btorf("%d and %d %d %d\n", nid_en_and_a
, sid
, nid_en
, nid_a
);
1166 bad_properties
.push_back(nid_en_and_a
);
1168 int nid
= next_nid
++;
1169 btorf("%d bad %d%s\n", nid
, nid_en_and_a
, getinfo(cell
, true).c_str());
1172 btorf_pop(log_id(cell
));
1176 for (auto wire
: module
->wires())
1178 if (wire
->port_id
|| wire
->name
[0] == '$')
1181 btorf_push(stringf("wire %s", log_id(wire
)));
1183 int sid
= get_bv_sid(GetSize(wire
));
1184 int nid
= get_sig_nid(sigmap(wire
));
1186 if (statewires
.count(wire
))
1189 int this_nid
= next_nid
++;
1190 btorf("%d uext %d %d %d%s\n", this_nid
, sid
, nid
, 0, getinfo(wire
).c_str());
1192 btorf_pop(stringf("wire %s", log_id(wire
)));
1196 while (!ff_todo
.empty())
1198 vector
<pair
<int, Cell
*>> todo
;
1201 for (auto &it
: todo
)
1204 Cell
*cell
= it
.second
;
1206 btorf_push(stringf("next %s", log_id(cell
)));
1208 if (cell
->type
== ID($mem
))
1210 int abits
= cell
->getParam(ID::ABITS
).as_int();
1211 int width
= cell
->getParam(ID::WIDTH
).as_int();
1212 int wrports
= cell
->getParam(ID::WR_PORTS
).as_int();
1214 SigSpec sig_wr_addr
= sigmap(cell
->getPort(ID::WR_ADDR
));
1215 SigSpec sig_wr_data
= sigmap(cell
->getPort(ID::WR_DATA
));
1216 SigSpec sig_wr_en
= sigmap(cell
->getPort(ID::WR_EN
));
1218 int data_sid
= get_bv_sid(width
);
1219 int bool_sid
= get_bv_sid(1);
1220 int sid
= get_mem_sid(abits
, width
);
1223 for (int port
= 0; port
< wrports
; port
++)
1225 SigSpec wa
= sig_wr_addr
.extract(port
*abits
, abits
);
1226 SigSpec wd
= sig_wr_data
.extract(port
*width
, width
);
1227 SigSpec we
= sig_wr_en
.extract(port
*width
, width
);
1229 int wa_nid
= get_sig_nid(wa
);
1230 int wd_nid
= get_sig_nid(wd
);
1231 int we_nid
= get_sig_nid(we
);
1233 int nid2
= next_nid
++;
1234 btorf("%d read %d %d %d\n", nid2
, data_sid
, nid_head
, wa_nid
);
1236 int nid3
= next_nid
++;
1237 btorf("%d not %d %d\n", nid3
, data_sid
, we_nid
);
1239 int nid4
= next_nid
++;
1240 btorf("%d and %d %d %d\n", nid4
, data_sid
, nid2
, nid3
);
1242 int nid5
= next_nid
++;
1243 btorf("%d and %d %d %d\n", nid5
, data_sid
, wd_nid
, we_nid
);
1245 int nid6
= next_nid
++;
1246 btorf("%d or %d %d %d\n", nid6
, data_sid
, nid5
, nid4
);
1248 int nid7
= next_nid
++;
1249 btorf("%d write %d %d %d %d\n", nid7
, sid
, nid_head
, wa_nid
, nid6
);
1251 int nid8
= next_nid
++;
1252 btorf("%d redor %d %d\n", nid8
, bool_sid
, we_nid
);
1254 int nid9
= next_nid
++;
1255 btorf("%d ite %d %d %d %d\n", nid9
, sid
, nid8
, nid7
, nid_head
);
1260 int nid2
= next_nid
++;
1261 btorf("%d next %d %d %d%s\n", nid2
, sid
, nid
, nid_head
, getinfo(cell
).c_str());
1265 SigSpec sig
= sigmap(cell
->getPort(ID::D
));
1266 int nid_q
= get_sig_nid(sig
);
1267 int sid
= get_bv_sid(GetSize(sig
));
1268 btorf("%d next %d %d %d%s\n", next_nid
++, sid
, nid
, nid_q
, getinfo(cell
).c_str());
1271 btorf_pop(stringf("next %s", log_id(cell
)));
1275 while (!bad_properties
.empty())
1278 bad_properties
.swap(todo
);
1280 int sid
= get_bv_sid(1);
1283 while (cursor
+1 < GetSize(todo
))
1285 int nid_a
= todo
[cursor
++];
1286 int nid_b
= todo
[cursor
++];
1287 int nid
= next_nid
++;
1289 bad_properties
.push_back(nid
);
1290 btorf("%d or %d %d %d\n", nid
, sid
, nid_a
, nid_b
);
1293 if (!bad_properties
.empty()) {
1294 if (cursor
< GetSize(todo
))
1295 bad_properties
.push_back(todo
[cursor
++]);
1296 log_assert(cursor
== GetSize(todo
));
1298 int nid
= next_nid
++;
1299 log_assert(cursor
== 0);
1300 log_assert(GetSize(todo
) == 1);
1301 btorf("%d bad %d\n", nid
, todo
[cursor
]);
1305 if (!info_filename
.empty())
1307 for (auto &it
: info_clocks
)
1312 infof("posedge %d\n", it
.first
);
1315 infof("negedge %d\n", it
.first
);
1318 infof("event %d\n", it
.first
);
1326 f
.open(info_filename
.c_str(), std::ofstream::trunc
);
1328 log_error("Can't open file `%s' for writing: %s\n", info_filename
.c_str(), strerror(errno
));
1329 for (auto &it
: info_lines
)
1336 struct BtorBackend
: public Backend
{
1337 BtorBackend() : Backend("btor", "write design to BTOR file") { }
1338 void help() YS_OVERRIDE
1340 // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
1342 log(" write_btor [options] [filename]\n");
1344 log("Write a BTOR description of the current design.\n");
1347 log(" Add comments and indentation to BTOR output file\n");
1350 log(" Output only a single bad property for all asserts\n");
1353 log(" Output cover properties using 'bad' statements instead of asserts\n");
1355 log(" -i <filename>\n");
1356 log(" Create additional info file with auxiliary information\n");
1359 log(" Don't identify internal netnames\n");
1362 void execute(std::ostream
*&f
, std::string filename
, std::vector
<std::string
> args
, RTLIL::Design
*design
) YS_OVERRIDE
1364 bool verbose
= false, single_bad
= false, cover_mode
= false, print_internal_names
= true;
1365 string info_filename
;
1367 log_header(design
, "Executing BTOR backend.\n");
1370 for (argidx
= 1; argidx
< args
.size(); argidx
++)
1372 if (args
[argidx
] == "-v") {
1376 if (args
[argidx
] == "-s") {
1380 if (args
[argidx
] == "-c") {
1384 if (args
[argidx
] == "-i" && argidx
+1 < args
.size()) {
1385 info_filename
= args
[++argidx
];
1388 if (args
[argidx
] == "-n") {
1389 print_internal_names
= false;
1394 extra_args(f
, filename
, args
, argidx
);
1396 RTLIL::Module
*topmod
= design
->top_module();
1398 if (topmod
== nullptr)
1399 log_cmd_error("No top module found.\n");
1401 *f
<< stringf("; BTOR description generated by %s for module %s.\n",
1402 yosys_version_str
, log_id(topmod
));
1404 BtorWorker(*f
, topmod
, verbose
, single_bad
, cover_mode
, print_internal_names
, info_filename
);
1406 *f
<< stringf("; end of yosys output\n");
1410 PRIVATE_NAMESPACE_END