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
;
45 int initstate_nid
= -1;
48 dict
<int, int> sorts_bv
;
50 // (<address-width>, <data-width>) => <sid>
51 dict
<pair
<int, int>, int> sorts_mem
;
53 // SigBit => (<nid>, <bitidx>)
54 dict
<SigBit
, pair
<int, int>> bit_nid
;
57 dict
<int, int> nid_width
;
60 dict
<SigSpec
, int> sig_nid
;
62 // bit to driving cell
63 dict
<SigBit
, Cell
*> bit_cell
;
66 dict
<Const
, int> consts
;
68 // ff inputs that need to be evaluated (<nid>, <ff_cell>)
69 vector
<pair
<int, Cell
*>> ff_todo
;
71 pool
<Cell
*> cell_recursion_guard
;
72 vector
<int> bad_properties
;
73 dict
<SigBit
, bool> initbits
;
74 pool
<Wire
*> statewires
;
75 pool
<string
> srcsymbols
;
77 string indent
, info_filename
;
78 vector
<string
> info_lines
;
79 dict
<int, int> info_clocks
;
81 void btorf(const char *fmt
, ...)
85 f
<< indent
<< vstringf(fmt
, ap
);
89 void infof(const char *fmt
, ...)
93 info_lines
.push_back(vstringf(fmt
, ap
));
98 string
getinfo(T
*obj
, bool srcsym
= false)
100 string infostr
= log_id(obj
);
101 if (obj
->attributes
.count("\\src")) {
102 string src
= obj
->attributes
.at("\\src").decode_string().c_str();
103 if (srcsym
&& infostr
[0] == '$') {
104 std::replace(src
.begin(), src
.end(), ' ', '_');
105 if (srcsymbols
.count(src
) || module
->count_id("\\" + src
)) {
106 for (int i
= 1;; i
++) {
107 string s
= stringf("%s-%d", src
.c_str(), i
);
108 if (!srcsymbols
.count(s
) && !module
->count_id("\\" + s
)) {
114 srcsymbols
.insert(src
);
117 infostr
+= " ; " + src
;
123 void btorf_push(const string
&id
)
126 f
<< indent
<< stringf(" ; begin %s\n", id
.c_str());
131 void btorf_pop(const string
&id
)
134 indent
= indent
.substr(4);
135 f
<< indent
<< stringf(" ; end %s\n", id
.c_str());
139 int get_bv_sid(int width
)
141 if (sorts_bv
.count(width
) == 0) {
142 int nid
= next_nid
++;
143 btorf("%d sort bitvec %d\n", nid
, width
);
144 sorts_bv
[width
] = nid
;
146 return sorts_bv
.at(width
);
149 int get_mem_sid(int abits
, int dbits
)
151 pair
<int, int> key(abits
, dbits
);
152 if (sorts_mem
.count(key
) == 0) {
153 int addr_sid
= get_bv_sid(abits
);
154 int data_sid
= get_bv_sid(dbits
);
155 int nid
= next_nid
++;
156 btorf("%d sort array %d %d\n", nid
, addr_sid
, data_sid
);
157 sorts_mem
[key
] = nid
;
159 return sorts_mem
.at(key
);
162 void add_nid_sig(int nid
, const SigSpec
&sig
)
165 f
<< indent
<< stringf("; %d %s\n", nid
, log_signal(sig
));
167 for (int i
= 0; i
< GetSize(sig
); i
++)
168 bit_nid
[sig
[i
]] = make_pair(nid
, i
);
171 nid_width
[nid
] = GetSize(sig
);
174 void export_cell(Cell
*cell
)
176 if (cell_recursion_guard
.count(cell
)) {
178 for (auto c
: cell_recursion_guard
)
179 cell_list
+= stringf("\n %s", log_id(c
));
180 log_error("Found topological loop while processing cell %s. Active cells:%s\n", log_id(cell
), cell_list
.c_str());
183 cell_recursion_guard
.insert(cell
);
184 btorf_push(log_id(cell
));
186 if (cell
->type
.in("$add", "$sub", "$mul", "$and", "$or", "$xor", "$xnor", "$shl", "$sshl", "$shr", "$sshr", "$shift", "$shiftx",
187 "$concat", "$_AND_", "$_NAND_", "$_OR_", "$_NOR_", "$_XOR_", "$_XNOR_"))
190 if (cell
->type
== "$add") btor_op
= "add";
191 if (cell
->type
== "$sub") btor_op
= "sub";
192 if (cell
->type
== "$mul") btor_op
= "mul";
193 if (cell
->type
.in("$shl", "$sshl")) btor_op
= "sll";
194 if (cell
->type
== "$shr") btor_op
= "srl";
195 if (cell
->type
== "$sshr") btor_op
= "sra";
196 if (cell
->type
.in("$shift", "$shiftx")) btor_op
= "shift";
197 if (cell
->type
.in("$and", "$_AND_")) btor_op
= "and";
198 if (cell
->type
.in("$or", "$_OR_")) btor_op
= "or";
199 if (cell
->type
.in("$xor", "$_XOR_")) btor_op
= "xor";
200 if (cell
->type
== "$concat") btor_op
= "concat";
201 if (cell
->type
== "$_NAND_") btor_op
= "nand";
202 if (cell
->type
== "$_NOR_") btor_op
= "nor";
203 if (cell
->type
.in("$xnor", "$_XNOR_")) btor_op
= "xnor";
204 log_assert(!btor_op
.empty());
206 int width
= GetSize(cell
->getPort("\\Y"));
207 width
= std::max(width
, GetSize(cell
->getPort("\\A")));
208 width
= std::max(width
, GetSize(cell
->getPort("\\B")));
210 bool a_signed
= cell
->hasParam("\\A_SIGNED") ? cell
->getParam("\\A_SIGNED").as_bool() : false;
211 bool b_signed
= cell
->hasParam("\\B_SIGNED") ? cell
->getParam("\\B_SIGNED").as_bool() : false;
213 if (btor_op
== "shift" && !b_signed
)
216 if (cell
->type
.in("$shl", "$sshl", "$shr", "$sshr"))
219 if (cell
->type
== "$sshr" && !a_signed
)
222 int sid
= get_bv_sid(width
);
225 if (btor_op
== "shift")
227 int nid_a
= get_sig_nid(cell
->getPort("\\A"), width
, false);
228 int nid_b
= get_sig_nid(cell
->getPort("\\B"), width
, b_signed
);
230 int nid_r
= next_nid
++;
231 btorf("%d srl %d %d %d\n", nid_r
, sid
, nid_a
, nid_b
);
233 int nid_b_neg
= next_nid
++;
234 btorf("%d neg %d %d\n", nid_b_neg
, sid
, nid_b
);
236 int nid_l
= next_nid
++;
237 btorf("%d sll %d %d %d\n", nid_l
, sid
, nid_a
, nid_b_neg
);
239 int sid_bit
= get_bv_sid(1);
240 int nid_zero
= get_sig_nid(Const(0, width
));
241 int nid_b_ltz
= next_nid
++;
242 btorf("%d slt %d %d %d\n", nid_b_ltz
, sid_bit
, nid_b
, nid_zero
);
245 btorf("%d ite %d %d %d %d %s\n", nid
, sid
, nid_b_ltz
, nid_l
, nid_r
, getinfo(cell
).c_str());
249 int nid_a
= get_sig_nid(cell
->getPort("\\A"), width
, a_signed
);
250 int nid_b
= get_sig_nid(cell
->getPort("\\B"), width
, b_signed
);
253 btorf("%d %s %d %d %d %s\n", nid
, btor_op
.c_str(), sid
, nid_a
, nid_b
, getinfo(cell
).c_str());
256 SigSpec sig
= sigmap(cell
->getPort("\\Y"));
258 if (GetSize(sig
) < width
) {
259 int sid
= get_bv_sid(GetSize(sig
));
260 int nid2
= next_nid
++;
261 btorf("%d slice %d %d %d 0\n", nid2
, sid
, nid
, GetSize(sig
)-1);
265 add_nid_sig(nid
, sig
);
269 if (cell
->type
.in("$div", "$mod"))
272 if (cell
->type
== "$div") btor_op
= "div";
273 if (cell
->type
== "$mod") btor_op
= "rem";
274 log_assert(!btor_op
.empty());
276 int width
= GetSize(cell
->getPort("\\Y"));
277 width
= std::max(width
, GetSize(cell
->getPort("\\A")));
278 width
= std::max(width
, GetSize(cell
->getPort("\\B")));
280 bool a_signed
= cell
->hasParam("\\A_SIGNED") ? cell
->getParam("\\A_SIGNED").as_bool() : false;
281 bool b_signed
= cell
->hasParam("\\B_SIGNED") ? cell
->getParam("\\B_SIGNED").as_bool() : false;
283 int nid_a
= get_sig_nid(cell
->getPort("\\A"), width
, a_signed
);
284 int nid_b
= get_sig_nid(cell
->getPort("\\B"), width
, b_signed
);
286 int sid
= get_bv_sid(width
);
287 int nid
= next_nid
++;
288 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());
290 SigSpec sig
= sigmap(cell
->getPort("\\Y"));
292 if (GetSize(sig
) < width
) {
293 int sid
= get_bv_sid(GetSize(sig
));
294 int nid2
= next_nid
++;
295 btorf("%d slice %d %d %d 0\n", nid2
, sid
, nid
, GetSize(sig
)-1);
299 add_nid_sig(nid
, sig
);
303 if (cell
->type
.in("$_ANDNOT_", "$_ORNOT_"))
305 int sid
= get_bv_sid(1);
306 int nid_a
= get_sig_nid(cell
->getPort("\\A"));
307 int nid_b
= get_sig_nid(cell
->getPort("\\B"));
309 int nid1
= next_nid
++;
310 int nid2
= next_nid
++;
312 if (cell
->type
== "$_ANDNOT_") {
313 btorf("%d not %d %d\n", nid1
, sid
, nid_b
);
314 btorf("%d and %d %d %d %s\n", nid2
, sid
, nid_a
, nid1
, getinfo(cell
).c_str());
317 if (cell
->type
== "$_ORNOT_") {
318 btorf("%d not %d %d\n", nid1
, sid
, nid_b
);
319 btorf("%d or %d %d %d %s\n", nid2
, sid
, nid_a
, nid1
, getinfo(cell
).c_str());
322 SigSpec sig
= sigmap(cell
->getPort("\\Y"));
323 add_nid_sig(nid2
, sig
);
327 if (cell
->type
.in("$_OAI3_", "$_AOI3_"))
329 int sid
= get_bv_sid(1);
330 int nid_a
= get_sig_nid(cell
->getPort("\\A"));
331 int nid_b
= get_sig_nid(cell
->getPort("\\B"));
332 int nid_c
= get_sig_nid(cell
->getPort("\\C"));
334 int nid1
= next_nid
++;
335 int nid2
= next_nid
++;
336 int nid3
= next_nid
++;
338 if (cell
->type
== "$_OAI3_") {
339 btorf("%d or %d %d %d\n", nid1
, sid
, nid_a
, nid_b
);
340 btorf("%d and %d %d %d\n", nid2
, sid
, nid1
, nid_c
);
341 btorf("%d not %d %d %s\n", nid3
, sid
, nid2
, getinfo(cell
).c_str());
344 if (cell
->type
== "$_AOI3_") {
345 btorf("%d and %d %d %d\n", nid1
, sid
, nid_a
, nid_b
);
346 btorf("%d or %d %d %d\n", nid2
, sid
, nid1
, nid_c
);
347 btorf("%d not %d %d %s\n", nid3
, sid
, nid2
, getinfo(cell
).c_str());
350 SigSpec sig
= sigmap(cell
->getPort("\\Y"));
351 add_nid_sig(nid3
, sig
);
355 if (cell
->type
.in("$_OAI4_", "$_AOI4_"))
357 int sid
= get_bv_sid(1);
358 int nid_a
= get_sig_nid(cell
->getPort("\\A"));
359 int nid_b
= get_sig_nid(cell
->getPort("\\B"));
360 int nid_c
= get_sig_nid(cell
->getPort("\\C"));
361 int nid_d
= get_sig_nid(cell
->getPort("\\D"));
363 int nid1
= next_nid
++;
364 int nid2
= next_nid
++;
365 int nid3
= next_nid
++;
366 int nid4
= next_nid
++;
368 if (cell
->type
== "$_OAI4_") {
369 btorf("%d or %d %d %d\n", nid1
, sid
, nid_a
, nid_b
);
370 btorf("%d or %d %d %d\n", nid2
, sid
, nid_c
, nid_d
);
371 btorf("%d and %d %d %d\n", nid3
, sid
, nid1
, nid2
);
372 btorf("%d not %d %d %s\n", nid4
, sid
, nid3
, getinfo(cell
).c_str());
375 if (cell
->type
== "$_AOI4_") {
376 btorf("%d and %d %d %d\n", nid1
, sid
, nid_a
, nid_b
);
377 btorf("%d and %d %d %d\n", nid2
, sid
, nid_c
, nid_d
);
378 btorf("%d or %d %d %d\n", nid3
, sid
, nid1
, nid2
);
379 btorf("%d not %d %d %s\n", nid4
, sid
, nid3
, getinfo(cell
).c_str());
382 SigSpec sig
= sigmap(cell
->getPort("\\Y"));
383 add_nid_sig(nid4
, sig
);
387 if (cell
->type
.in("$lt", "$le", "$eq", "$eqx", "$ne", "$nex", "$ge", "$gt"))
390 if (cell
->type
== "$lt") btor_op
= "lt";
391 if (cell
->type
== "$le") btor_op
= "lte";
392 if (cell
->type
.in("$eq", "$eqx")) btor_op
= "eq";
393 if (cell
->type
.in("$ne", "$nex")) btor_op
= "neq";
394 if (cell
->type
== "$ge") btor_op
= "gte";
395 if (cell
->type
== "$gt") btor_op
= "gt";
396 log_assert(!btor_op
.empty());
399 width
= std::max(width
, GetSize(cell
->getPort("\\A")));
400 width
= std::max(width
, GetSize(cell
->getPort("\\B")));
402 bool a_signed
= cell
->hasParam("\\A_SIGNED") ? cell
->getParam("\\A_SIGNED").as_bool() : false;
403 bool b_signed
= cell
->hasParam("\\B_SIGNED") ? cell
->getParam("\\B_SIGNED").as_bool() : false;
405 int sid
= get_bv_sid(1);
406 int nid_a
= get_sig_nid(cell
->getPort("\\A"), width
, a_signed
);
407 int nid_b
= get_sig_nid(cell
->getPort("\\B"), width
, b_signed
);
409 int nid
= next_nid
++;
410 if (cell
->type
.in("$lt", "$le", "$ge", "$gt")) {
411 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());
413 btorf("%d %s %d %d %d %s\n", nid
, btor_op
.c_str(), sid
, nid_a
, nid_b
, getinfo(cell
).c_str());
416 SigSpec sig
= sigmap(cell
->getPort("\\Y"));
418 if (GetSize(sig
) > 1) {
419 int sid
= get_bv_sid(GetSize(sig
));
420 int nid2
= next_nid
++;
421 btorf("%d uext %d %d %d\n", nid2
, sid
, nid
, GetSize(sig
) - 1);
425 add_nid_sig(nid
, sig
);
429 if (cell
->type
.in("$not", "$neg", "$_NOT_"))
432 if (cell
->type
.in("$not", "$_NOT_")) btor_op
= "not";
433 if (cell
->type
== "$neg") btor_op
= "neg";
434 log_assert(!btor_op
.empty());
436 int width
= GetSize(cell
->getPort("\\Y"));
437 width
= std::max(width
, GetSize(cell
->getPort("\\A")));
439 bool a_signed
= cell
->hasParam("\\A_SIGNED") ? cell
->getParam("\\A_SIGNED").as_bool() : false;
441 int sid
= get_bv_sid(width
);
442 int nid_a
= get_sig_nid(cell
->getPort("\\A"), width
, a_signed
);
444 int nid
= next_nid
++;
445 btorf("%d %s %d %d\n", nid
, btor_op
.c_str(), sid
, nid_a
, getinfo(cell
).c_str());
447 SigSpec sig
= sigmap(cell
->getPort("\\Y"));
449 if (GetSize(sig
) < width
) {
450 int sid
= get_bv_sid(GetSize(sig
));
451 int nid2
= next_nid
++;
452 btorf("%d slice %d %d %d 0\n", nid2
, sid
, nid
, GetSize(sig
)-1);
456 add_nid_sig(nid
, sig
);
460 if (cell
->type
.in("$logic_and", "$logic_or", "$logic_not"))
463 if (cell
->type
== "$logic_and") btor_op
= "and";
464 if (cell
->type
== "$logic_or") btor_op
= "or";
465 if (cell
->type
== "$logic_not") btor_op
= "not";
466 log_assert(!btor_op
.empty());
468 int sid
= get_bv_sid(1);
469 int nid_a
= get_sig_nid(cell
->getPort("\\A"));
470 int nid_b
= btor_op
!= "not" ? get_sig_nid(cell
->getPort("\\B")) : 0;
472 if (GetSize(cell
->getPort("\\A")) > 1) {
473 int nid_red_a
= next_nid
++;
474 btorf("%d redor %d %d\n", nid_red_a
, sid
, nid_a
);
478 if (btor_op
!= "not" && GetSize(cell
->getPort("\\B")) > 1) {
479 int nid_red_b
= next_nid
++;
480 btorf("%d redor %d %d\n", nid_red_b
, sid
, nid_b
);
484 int nid
= next_nid
++;
485 if (btor_op
!= "not")
486 btorf("%d %s %d %d %d\n", nid
, btor_op
.c_str(), sid
, nid_a
, nid_b
, getinfo(cell
).c_str());
488 btorf("%d %s %d %d\n", nid
, btor_op
.c_str(), sid
, nid_a
, getinfo(cell
).c_str());
490 SigSpec sig
= sigmap(cell
->getPort("\\Y"));
492 if (GetSize(sig
) > 1) {
493 int sid
= get_bv_sid(GetSize(sig
));
494 int zeros_nid
= get_sig_nid(Const(0, GetSize(sig
)-1));
495 int nid2
= next_nid
++;
496 btorf("%d concat %d %d %d\n", nid2
, sid
, zeros_nid
, nid
);
500 add_nid_sig(nid
, sig
);
504 if (cell
->type
.in("$reduce_and", "$reduce_or", "$reduce_bool", "$reduce_xor", "$reduce_xnor"))
507 if (cell
->type
== "$reduce_and") btor_op
= "redand";
508 if (cell
->type
.in("$reduce_or", "$reduce_bool")) btor_op
= "redor";
509 if (cell
->type
.in("$reduce_xor", "$reduce_xnor")) btor_op
= "redxor";
510 log_assert(!btor_op
.empty());
512 int sid
= get_bv_sid(1);
513 int nid_a
= get_sig_nid(cell
->getPort("\\A"));
515 int nid
= next_nid
++;
517 if (cell
->type
== "$reduce_xnor") {
518 int nid2
= next_nid
++;
519 btorf("%d %s %d %d %s\n", nid
, btor_op
.c_str(), sid
, nid_a
, getinfo(cell
).c_str());
520 btorf("%d not %d %d %d\n", nid2
, sid
, nid
);
523 btorf("%d %s %d %d %s\n", nid
, btor_op
.c_str(), sid
, nid_a
, getinfo(cell
).c_str());
526 SigSpec sig
= sigmap(cell
->getPort("\\Y"));
528 if (GetSize(sig
) > 1) {
529 int sid
= get_bv_sid(GetSize(sig
));
530 int zeros_nid
= get_sig_nid(Const(0, GetSize(sig
)-1));
531 int nid2
= next_nid
++;
532 btorf("%d concat %d %d %d\n", nid2
, sid
, zeros_nid
, nid
);
536 add_nid_sig(nid
, sig
);
540 if (cell
->type
.in("$mux", "$_MUX_", "$_NMUX_"))
542 SigSpec sig_a
= sigmap(cell
->getPort("\\A"));
543 SigSpec sig_b
= sigmap(cell
->getPort("\\B"));
544 SigSpec sig_s
= sigmap(cell
->getPort("\\S"));
545 SigSpec sig_y
= sigmap(cell
->getPort("\\Y"));
547 int nid_a
= get_sig_nid(sig_a
);
548 int nid_b
= get_sig_nid(sig_b
);
549 int nid_s
= get_sig_nid(sig_s
);
551 int sid
= get_bv_sid(GetSize(sig_y
));
552 int nid
= next_nid
++;
554 if (cell
->type
== "$_NMUX_") {
557 btorf("%d ite %d %d %d %d\n", tmp
, sid
, nid_s
, nid_b
, nid_a
);
558 btorf("%d not %d %d %s\n", nid
, sid
, tmp
, getinfo(cell
).c_str());
560 btorf("%d ite %d %d %d %d %s\n", nid
, sid
, nid_s
, nid_b
, nid_a
, getinfo(cell
).c_str());
563 add_nid_sig(nid
, sig_y
);
567 if (cell
->type
== "$pmux")
569 SigSpec sig_a
= sigmap(cell
->getPort("\\A"));
570 SigSpec sig_b
= sigmap(cell
->getPort("\\B"));
571 SigSpec sig_s
= sigmap(cell
->getPort("\\S"));
572 SigSpec sig_y
= sigmap(cell
->getPort("\\Y"));
574 int width
= GetSize(sig_a
);
575 int sid
= get_bv_sid(width
);
576 int nid
= get_sig_nid(sig_a
);
578 for (int i
= 0; i
< GetSize(sig_s
); i
++) {
579 int nid_b
= get_sig_nid(sig_b
.extract(i
*width
, width
));
580 int nid_s
= get_sig_nid(sig_s
.extract(i
));
581 int nid2
= next_nid
++;
582 if (i
== GetSize(sig_s
)-1)
583 btorf("%d ite %d %d %d %d %s\n", nid2
, sid
, nid_s
, nid_b
, nid
, getinfo(cell
).c_str());
585 btorf("%d ite %d %d %d %d\n", nid2
, sid
, nid_s
, nid_b
, nid
);
589 add_nid_sig(nid
, sig_y
);
593 if (cell
->type
.in("$dff", "$ff", "$_DFF_P_", "$_DFF_N_", "$_FF_"))
595 SigSpec sig_d
= sigmap(cell
->getPort("\\D"));
596 SigSpec sig_q
= sigmap(cell
->getPort("\\Q"));
598 if (!info_filename
.empty() && cell
->type
.in("$dff", "$_DFF_P_", "$_DFF_N_"))
600 SigSpec sig_c
= sigmap(cell
->getPort(cell
->type
== "$dff" ? "\\CLK" : "\\C"));
601 int nid
= get_sig_nid(sig_c
);
602 bool negedge
= false;
604 if (cell
->type
== "$_DFF_N_")
607 if (cell
->type
== "$dff" && !cell
->getParam("\\CLK_POLARITY").as_bool())
610 info_clocks
[nid
] |= negedge
? 2 : 1;
615 if (sig_q
.is_wire()) {
616 Wire
*w
= sig_q
.as_wire();
617 if (w
->port_id
== 0) {
618 statewires
.insert(w
);
624 for (int i
= 0; i
< GetSize(sig_q
); i
++)
625 if (initbits
.count(sig_q
[i
]))
626 initval
.bits
.push_back(initbits
.at(sig_q
[i
]) ? State::S1
: State::S0
);
628 initval
.bits
.push_back(State::Sx
);
630 int nid_init_val
= -1;
632 if (!initval
.is_fully_undef())
633 nid_init_val
= get_sig_nid(initval
, -1, false, true);
635 int sid
= get_bv_sid(GetSize(sig_q
));
636 int nid
= next_nid
++;
639 btorf("%d state %d\n", nid
, sid
);
641 btorf("%d state %d %s\n", nid
, sid
, log_id(symbol
));
643 if (nid_init_val
>= 0) {
644 int nid_init
= next_nid
++;
646 btorf("; initval = %s\n", log_signal(initval
));
647 btorf("%d init %d %d %d\n", nid_init
, sid
, nid
, nid_init_val
);
650 ff_todo
.push_back(make_pair(nid
, cell
));
651 add_nid_sig(nid
, sig_q
);
655 if (cell
->type
.in("$anyconst", "$anyseq"))
657 SigSpec sig_y
= sigmap(cell
->getPort("\\Y"));
659 int sid
= get_bv_sid(GetSize(sig_y
));
660 int nid
= next_nid
++;
662 btorf("%d state %d\n", nid
, sid
);
664 if (cell
->type
== "$anyconst") {
665 int nid2
= next_nid
++;
666 btorf("%d next %d %d %d\n", nid2
, sid
, nid
, nid
);
669 add_nid_sig(nid
, sig_y
);
673 if (cell
->type
== "$initstate")
675 SigSpec sig_y
= sigmap(cell
->getPort("\\Y"));
677 if (initstate_nid
< 0)
679 int sid
= get_bv_sid(1);
680 int one_nid
= get_sig_nid(State::S1
);
681 int zero_nid
= get_sig_nid(State::S0
);
682 initstate_nid
= next_nid
++;
683 btorf("%d state %d\n", initstate_nid
, sid
);
684 btorf("%d init %d %d %d\n", next_nid
++, sid
, initstate_nid
, one_nid
);
685 btorf("%d next %d %d %d\n", next_nid
++, sid
, initstate_nid
, zero_nid
);
688 add_nid_sig(initstate_nid
, sig_y
);
692 if (cell
->type
== "$mem")
694 int abits
= cell
->getParam("\\ABITS").as_int();
695 int width
= cell
->getParam("\\WIDTH").as_int();
696 int nwords
= cell
->getParam("\\SIZE").as_int();
697 int rdports
= cell
->getParam("\\RD_PORTS").as_int();
698 int wrports
= cell
->getParam("\\WR_PORTS").as_int();
700 Const wr_clk_en
= cell
->getParam("\\WR_CLK_ENABLE");
701 Const rd_clk_en
= cell
->getParam("\\RD_CLK_ENABLE");
703 bool asyncwr
= wr_clk_en
.is_fully_zero();
705 if (!asyncwr
&& !wr_clk_en
.is_fully_ones())
706 log_error("Memory %s.%s has mixed async/sync write ports.\n",
707 log_id(module
), log_id(cell
));
709 if (!rd_clk_en
.is_fully_zero())
710 log_error("Memory %s.%s has sync read ports.\n",
711 log_id(module
), log_id(cell
));
713 SigSpec sig_rd_addr
= sigmap(cell
->getPort("\\RD_ADDR"));
714 SigSpec sig_rd_data
= sigmap(cell
->getPort("\\RD_DATA"));
716 SigSpec sig_wr_addr
= sigmap(cell
->getPort("\\WR_ADDR"));
717 SigSpec sig_wr_data
= sigmap(cell
->getPort("\\WR_DATA"));
718 SigSpec sig_wr_en
= sigmap(cell
->getPort("\\WR_EN"));
720 int data_sid
= get_bv_sid(width
);
721 int bool_sid
= get_bv_sid(1);
722 int sid
= get_mem_sid(abits
, width
);
724 Const initdata
= cell
->getParam("\\INIT");
725 initdata
.exts(nwords
*width
);
726 int nid_init_val
= -1;
728 if (!initdata
.is_fully_undef())
730 bool constword
= true;
731 Const firstword
= initdata
.extract(0, width
);
733 for (int i
= 1; i
< nwords
; i
++) {
734 Const thisword
= initdata
.extract(i
*width
, width
);
735 if (thisword
!= firstword
) {
744 btorf("; initval = %s\n", log_signal(firstword
));
745 nid_init_val
= get_sig_nid(firstword
, -1, false, true);
749 nid_init_val
= next_nid
++;
750 btorf("%d state %d\n", nid_init_val
, sid
);
752 for (int i
= 0; i
< nwords
; i
++) {
753 Const thisword
= initdata
.extract(i
*width
, width
);
754 if (thisword
.is_fully_undef())
756 Const
thisaddr(i
, abits
);
757 int nid_thisword
= get_sig_nid(thisword
, -1, false, true);
758 int nid_thisaddr
= get_sig_nid(thisaddr
, -1, false, true);
759 int last_nid_init_val
= nid_init_val
;
760 nid_init_val
= next_nid
++;
762 btorf("; initval[%d] = %s\n", i
, log_signal(thisword
));
763 btorf("%d write %d %d %d %d\n", nid_init_val
, sid
, last_nid_init_val
, nid_thisaddr
, nid_thisword
);
769 int nid
= next_nid
++;
772 if (cell
->name
[0] == '$')
773 btorf("%d state %d\n", nid
, sid
);
775 btorf("%d state %d %s\n", nid
, sid
, log_id(cell
));
777 if (nid_init_val
>= 0)
779 int nid_init
= next_nid
++;
780 btorf("%d init %d %d %d\n", nid_init
, sid
, nid
, nid_init_val
);
785 for (int port
= 0; port
< wrports
; port
++)
787 SigSpec wa
= sig_wr_addr
.extract(port
*abits
, abits
);
788 SigSpec wd
= sig_wr_data
.extract(port
*width
, width
);
789 SigSpec we
= sig_wr_en
.extract(port
*width
, width
);
791 int wa_nid
= get_sig_nid(wa
);
792 int wd_nid
= get_sig_nid(wd
);
793 int we_nid
= get_sig_nid(we
);
795 int nid2
= next_nid
++;
796 btorf("%d read %d %d %d\n", nid2
, data_sid
, nid_head
, wa_nid
);
798 int nid3
= next_nid
++;
799 btorf("%d not %d %d\n", nid3
, data_sid
, we_nid
);
801 int nid4
= next_nid
++;
802 btorf("%d and %d %d %d\n", nid4
, data_sid
, nid2
, nid3
);
804 int nid5
= next_nid
++;
805 btorf("%d and %d %d %d\n", nid5
, data_sid
, wd_nid
, we_nid
);
807 int nid6
= next_nid
++;
808 btorf("%d or %d %d %d\n", nid6
, data_sid
, nid5
, nid4
);
810 int nid7
= next_nid
++;
811 btorf("%d write %d %d %d %d\n", nid7
, sid
, nid_head
, wa_nid
, nid6
);
813 int nid8
= next_nid
++;
814 btorf("%d redor %d %d\n", nid8
, bool_sid
, we_nid
);
816 int nid9
= next_nid
++;
817 btorf("%d ite %d %d %d %d\n", nid9
, sid
, nid8
, nid7
, nid_head
);
823 for (int port
= 0; port
< rdports
; port
++)
825 SigSpec ra
= sig_rd_addr
.extract(port
*abits
, abits
);
826 SigSpec rd
= sig_rd_data
.extract(port
*width
, width
);
828 int ra_nid
= get_sig_nid(ra
);
829 int rd_nid
= next_nid
++;
831 btorf("%d read %d %d %d\n", rd_nid
, data_sid
, nid_head
, ra_nid
);
833 add_nid_sig(rd_nid
, rd
);
838 ff_todo
.push_back(make_pair(nid
, cell
));
842 int nid2
= next_nid
++;
843 btorf("%d next %d %d %d\n", nid2
, sid
, nid
, nid_head
);
849 log_error("Unsupported cell type: %s (%s)\n", log_id(cell
->type
), log_id(cell
));
852 btorf_pop(log_id(cell
));
853 cell_recursion_guard
.erase(cell
);
856 int get_sig_nid(SigSpec sig
, int to_width
= -1, bool is_signed
= false, bool is_init
= false)
862 if (bit
== State::Sx
)
868 SigSpec sig_mask_undef
, sig_noundef
;
869 int first_undef
= -1;
871 for (int i
= 0; i
< GetSize(sig
); i
++)
872 if (sig
[i
] == State::Sx
) {
875 sig_mask_undef
.append(State::S1
);
876 sig_noundef
.append(State::S0
);
878 sig_mask_undef
.append(State::S0
);
879 sig_noundef
.append(sig
[i
]);
882 if (to_width
< 0 || first_undef
< to_width
)
884 int sid
= get_bv_sid(GetSize(sig
));
886 int nid_input
= next_nid
++;
888 btorf("%d state %d\n", nid_input
, sid
);
890 btorf("%d input %d\n", nid_input
, sid
);
892 int nid_masked_input
;
893 if (sig_mask_undef
.is_fully_ones()) {
894 nid_masked_input
= nid_input
;
896 int nid_mask_undef
= get_sig_nid(sig_mask_undef
);
897 nid_masked_input
= next_nid
++;
898 btorf("%d and %d %d %d\n", nid_masked_input
, sid
, nid_input
, nid_mask_undef
);
901 if (sig_noundef
.is_fully_zero()) {
902 nid
= nid_masked_input
;
904 int nid_noundef
= get_sig_nid(sig_noundef
);
906 btorf("%d or %d %d %d\n", nid
, sid
, nid_masked_input
, nid_noundef
);
915 if (sig_nid
.count(sig
) == 0)
918 vector
<pair
<int, int>> nidbits
;
921 for (int i
= 0; i
< GetSize(sig
); i
++)
925 if (bit_nid
.count(bit
) == 0)
927 if (bit
.wire
== nullptr)
931 while (i
+GetSize(c
) < GetSize(sig
) && sig
[i
+GetSize(c
)].wire
== nullptr)
932 c
.bits
.push_back(sig
[i
+GetSize(c
)].data
);
934 if (consts
.count(c
) == 0) {
935 int sid
= get_bv_sid(GetSize(c
));
936 int nid
= next_nid
++;
937 btorf("%d const %d %s\n", nid
, sid
, c
.as_string().c_str());
939 nid_width
[nid
] = GetSize(c
);
942 int nid
= consts
.at(c
);
944 for (int j
= 0; j
< GetSize(c
); j
++)
945 nidbits
.push_back(make_pair(nid
, j
));
952 if (bit_cell
.count(bit
) == 0)
956 while (i
+GetSize(s
) < GetSize(sig
) && sig
[i
+GetSize(s
)].wire
!= nullptr &&
957 bit_cell
.count(sig
[i
+GetSize(s
)]) == 0)
958 s
.append(sig
[i
+GetSize(s
)]);
960 log_warning("No driver for signal %s.\n", log_signal(s
));
962 int sid
= get_bv_sid(GetSize(s
));
963 int nid
= next_nid
++;
964 btorf("%d input %d\n", nid
, sid
);
965 nid_width
[nid
] = GetSize(s
);
967 for (int j
= 0; j
< GetSize(s
); j
++)
968 nidbits
.push_back(make_pair(nid
, j
));
975 export_cell(bit_cell
.at(bit
));
976 log_assert(bit_nid
.count(bit
));
981 nidbits
.push_back(bit_nid
.at(bit
));
987 // group bits and emit slice-concat chain
988 for (int i
= 0; i
< GetSize(nidbits
); i
++)
990 int nid2
= nidbits
[i
].first
;
991 int lower
= nidbits
[i
].second
;
994 while (i
+1 < GetSize(nidbits
) && nidbits
[i
+1].first
== nidbits
[i
].first
&&
995 nidbits
[i
+1].second
== nidbits
[i
].second
+1)
1000 if (lower
!= 0 || upper
+1 != nid_width
.at(nid2
)) {
1001 int sid
= get_bv_sid(upper
-lower
+1);
1003 btorf("%d slice %d %d %d %d\n", nid3
, sid
, nid2
, upper
, lower
);
1009 int sid
= get_bv_sid(width
+upper
-lower
+1);
1011 btorf("%d concat %d %d %d\n", nid4
, sid
, nid3
, nid
);
1014 width
+= upper
-lower
+1;
1019 nid_width
[nid
] = width
;
1022 nid
= sig_nid
.at(sig
);
1025 if (to_width
>= 0 && to_width
!= GetSize(sig
))
1027 if (to_width
< GetSize(sig
))
1029 int sid
= get_bv_sid(to_width
);
1030 int nid2
= next_nid
++;
1031 btorf("%d slice %d %d %d 0\n", nid2
, sid
, nid
, to_width
-1);
1036 int sid
= get_bv_sid(to_width
);
1037 int nid2
= next_nid
++;
1038 btorf("%d %s %d %d %d\n", nid2
, is_signed
? "sext" : "uext",
1039 sid
, nid
, to_width
- GetSize(sig
));
1047 BtorWorker(std::ostream
&f
, RTLIL::Module
*module
, bool verbose
, bool single_bad
, bool cover_mode
, string info_filename
) :
1048 f(f
), sigmap(module
), module(module
), verbose(verbose
), single_bad(single_bad
), cover_mode(cover_mode
), info_filename(info_filename
)
1050 if (!info_filename
.empty())
1051 infof("name %s\n", log_id(module
));
1053 btorf_push("inputs");
1055 for (auto wire
: module
->wires())
1057 if (wire
->attributes
.count("\\init")) {
1058 Const attrval
= wire
->attributes
.at("\\init");
1059 for (int i
= 0; i
< GetSize(wire
) && i
< GetSize(attrval
); i
++)
1060 if (attrval
[i
] == State::S0
|| attrval
[i
] == State::S1
)
1061 initbits
[sigmap(SigBit(wire
, i
))] = (attrval
[i
] == State::S1
);
1064 if (!wire
->port_id
|| !wire
->port_input
)
1067 SigSpec sig
= sigmap(wire
);
1068 int sid
= get_bv_sid(GetSize(sig
));
1069 int nid
= next_nid
++;
1071 btorf("%d input %d %s\n", nid
, sid
, getinfo(wire
).c_str());
1072 add_nid_sig(nid
, sig
);
1075 btorf_pop("inputs");
1077 for (auto cell
: module
->cells())
1078 for (auto &conn
: cell
->connections())
1080 if (!cell
->output(conn
.first
))
1083 for (auto bit
: sigmap(conn
.second
))
1084 bit_cell
[bit
] = cell
;
1087 for (auto wire
: module
->wires())
1089 if (!wire
->port_id
|| !wire
->port_output
)
1092 btorf_push(stringf("output %s", log_id(wire
)));
1094 int nid
= get_sig_nid(wire
);
1095 btorf("%d output %d %s\n", next_nid
++, nid
, getinfo(wire
).c_str());
1097 btorf_pop(stringf("output %s", log_id(wire
)));
1100 for (auto cell
: module
->cells())
1102 if (cell
->type
== "$assume")
1104 btorf_push(log_id(cell
));
1106 int sid
= get_bv_sid(1);
1107 int nid_a
= get_sig_nid(cell
->getPort("\\A"));
1108 int nid_en
= get_sig_nid(cell
->getPort("\\EN"));
1109 int nid_not_en
= next_nid
++;
1110 int nid_a_or_not_en
= next_nid
++;
1111 int nid
= next_nid
++;
1113 btorf("%d not %d %d\n", nid_not_en
, sid
, nid_en
);
1114 btorf("%d or %d %d %d\n", nid_a_or_not_en
, sid
, nid_a
, nid_not_en
);
1115 btorf("%d constraint %d\n", nid
, nid_a_or_not_en
);
1117 btorf_pop(log_id(cell
));
1120 if (cell
->type
== "$assert")
1122 btorf_push(log_id(cell
));
1124 int sid
= get_bv_sid(1);
1125 int nid_a
= get_sig_nid(cell
->getPort("\\A"));
1126 int nid_en
= get_sig_nid(cell
->getPort("\\EN"));
1127 int nid_not_a
= next_nid
++;
1128 int nid_en_and_not_a
= next_nid
++;
1130 btorf("%d not %d %d\n", nid_not_a
, sid
, nid_a
);
1131 btorf("%d and %d %d %d\n", nid_en_and_not_a
, sid
, nid_en
, nid_not_a
);
1133 if (single_bad
&& !cover_mode
) {
1134 bad_properties
.push_back(nid_en_and_not_a
);
1137 infof("bad %d %s\n", nid_en_and_not_a
, getinfo(cell
, true).c_str());
1139 int nid
= next_nid
++;
1140 btorf("%d bad %d %s\n", nid
, nid_en_and_not_a
, getinfo(cell
, true).c_str());
1144 btorf_pop(log_id(cell
));
1147 if (cell
->type
== "$cover" && cover_mode
)
1149 btorf_push(log_id(cell
));
1151 int sid
= get_bv_sid(1);
1152 int nid_a
= get_sig_nid(cell
->getPort("\\A"));
1153 int nid_en
= get_sig_nid(cell
->getPort("\\EN"));
1154 int nid_en_and_a
= next_nid
++;
1156 btorf("%d and %d %d %d\n", nid_en_and_a
, sid
, nid_en
, nid_a
);
1159 bad_properties
.push_back(nid_en_and_a
);
1161 int nid
= next_nid
++;
1162 btorf("%d bad %d %s\n", nid
, nid_en_and_a
, getinfo(cell
, true).c_str());
1165 btorf_pop(log_id(cell
));
1169 for (auto wire
: module
->wires())
1171 if (wire
->port_id
|| wire
->name
[0] == '$')
1174 btorf_push(stringf("wire %s", log_id(wire
)));
1176 int sid
= get_bv_sid(GetSize(wire
));
1177 int nid
= get_sig_nid(sigmap(wire
));
1179 if (statewires
.count(wire
))
1182 int this_nid
= next_nid
++;
1183 btorf("%d uext %d %d %d %s\n", this_nid
, sid
, nid
, 0, getinfo(wire
).c_str());
1185 btorf_pop(stringf("wire %s", log_id(wire
)));
1189 while (!ff_todo
.empty())
1191 vector
<pair
<int, Cell
*>> todo
;
1194 for (auto &it
: todo
)
1197 Cell
*cell
= it
.second
;
1199 btorf_push(stringf("next %s", log_id(cell
)));
1201 if (cell
->type
== "$mem")
1203 int abits
= cell
->getParam("\\ABITS").as_int();
1204 int width
= cell
->getParam("\\WIDTH").as_int();
1205 int wrports
= cell
->getParam("\\WR_PORTS").as_int();
1207 SigSpec sig_wr_addr
= sigmap(cell
->getPort("\\WR_ADDR"));
1208 SigSpec sig_wr_data
= sigmap(cell
->getPort("\\WR_DATA"));
1209 SigSpec sig_wr_en
= sigmap(cell
->getPort("\\WR_EN"));
1211 int data_sid
= get_bv_sid(width
);
1212 int bool_sid
= get_bv_sid(1);
1213 int sid
= get_mem_sid(abits
, width
);
1216 for (int port
= 0; port
< wrports
; port
++)
1218 SigSpec wa
= sig_wr_addr
.extract(port
*abits
, abits
);
1219 SigSpec wd
= sig_wr_data
.extract(port
*width
, width
);
1220 SigSpec we
= sig_wr_en
.extract(port
*width
, width
);
1222 int wa_nid
= get_sig_nid(wa
);
1223 int wd_nid
= get_sig_nid(wd
);
1224 int we_nid
= get_sig_nid(we
);
1226 int nid2
= next_nid
++;
1227 btorf("%d read %d %d %d\n", nid2
, data_sid
, nid_head
, wa_nid
);
1229 int nid3
= next_nid
++;
1230 btorf("%d not %d %d\n", nid3
, data_sid
, we_nid
);
1232 int nid4
= next_nid
++;
1233 btorf("%d and %d %d %d\n", nid4
, data_sid
, nid2
, nid3
);
1235 int nid5
= next_nid
++;
1236 btorf("%d and %d %d %d\n", nid5
, data_sid
, wd_nid
, we_nid
);
1238 int nid6
= next_nid
++;
1239 btorf("%d or %d %d %d\n", nid6
, data_sid
, nid5
, nid4
);
1241 int nid7
= next_nid
++;
1242 btorf("%d write %d %d %d %d\n", nid7
, sid
, nid_head
, wa_nid
, nid6
);
1244 int nid8
= next_nid
++;
1245 btorf("%d redor %d %d\n", nid8
, bool_sid
, we_nid
);
1247 int nid9
= next_nid
++;
1248 btorf("%d ite %d %d %d %d\n", nid9
, sid
, nid8
, nid7
, nid_head
);
1253 int nid2
= next_nid
++;
1254 btorf("%d next %d %d %d %s\n", nid2
, sid
, nid
, nid_head
, getinfo(cell
).c_str());
1258 SigSpec sig
= sigmap(cell
->getPort("\\D"));
1259 int nid_q
= get_sig_nid(sig
);
1260 int sid
= get_bv_sid(GetSize(sig
));
1261 btorf("%d next %d %d %d %s\n", next_nid
++, sid
, nid
, nid_q
, getinfo(cell
).c_str());
1264 btorf_pop(stringf("next %s", log_id(cell
)));
1268 while (!bad_properties
.empty())
1271 bad_properties
.swap(todo
);
1273 int sid
= get_bv_sid(1);
1276 while (cursor
+1 < GetSize(todo
))
1278 int nid_a
= todo
[cursor
++];
1279 int nid_b
= todo
[cursor
++];
1280 int nid
= next_nid
++;
1282 bad_properties
.push_back(nid
);
1283 btorf("%d or %d %d %d\n", nid
, sid
, nid_a
, nid_b
);
1286 if (!bad_properties
.empty()) {
1287 if (cursor
< GetSize(todo
))
1288 bad_properties
.push_back(todo
[cursor
++]);
1289 log_assert(cursor
== GetSize(todo
));
1291 int nid
= next_nid
++;
1292 log_assert(cursor
== 0);
1293 log_assert(GetSize(todo
) == 1);
1294 btorf("%d bad %d\n", nid
, todo
[cursor
]);
1298 if (!info_filename
.empty())
1300 for (auto &it
: info_clocks
)
1305 infof("posedge %d\n", it
.first
);
1308 infof("negedge %d\n", it
.first
);
1311 infof("event %d\n", it
.first
);
1319 f
.open(info_filename
.c_str(), std::ofstream::trunc
);
1321 log_error("Can't open file `%s' for writing: %s\n", info_filename
.c_str(), strerror(errno
));
1322 for (auto &it
: info_lines
)
1329 struct BtorBackend
: public Backend
{
1330 BtorBackend() : Backend("btor", "write design to BTOR file") { }
1331 void help() YS_OVERRIDE
1333 // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
1335 log(" write_btor [options] [filename]\n");
1337 log("Write a BTOR description of the current design.\n");
1340 log(" Add comments and indentation to BTOR output file\n");
1343 log(" Output only a single bad property for all asserts\n");
1346 log(" Output cover properties using 'bad' statements instead of asserts\n");
1348 log(" -i <filename>\n");
1349 log(" Create additional info file with auxiliary information\n");
1352 void execute(std::ostream
*&f
, std::string filename
, std::vector
<std::string
> args
, RTLIL::Design
*design
) YS_OVERRIDE
1354 bool verbose
= false, single_bad
= false, cover_mode
= false;
1355 string info_filename
;
1357 log_header(design
, "Executing BTOR backend.\n");
1360 for (argidx
= 1; argidx
< args
.size(); argidx
++)
1362 if (args
[argidx
] == "-v") {
1366 if (args
[argidx
] == "-s") {
1370 if (args
[argidx
] == "-c") {
1374 if (args
[argidx
] == "-i" && argidx
+1 < args
.size()) {
1375 info_filename
= args
[++argidx
];
1380 extra_args(f
, filename
, args
, argidx
);
1382 RTLIL::Module
*topmod
= design
->top_module();
1384 if (topmod
== nullptr)
1385 log_cmd_error("No top module found.\n");
1387 *f
<< stringf("; BTOR description generated by %s for module %s.\n",
1388 yosys_version_str
, log_id(topmod
));
1390 BtorWorker(*f
, topmod
, verbose
, single_bad
, cover_mode
, info_filename
);
1392 *f
<< stringf("; end of yosys output\n");
1396 PRIVATE_NAMESPACE_END