projects / yosys.git / blob
? search:
summary | shortlog | log | commit | commitdiff | tree
history | raw | HEAD
Merge pull request #1846 from dh73/ast_fe
[yosys.git] / backends / btor / btor.cc
1 /*
2 * yosys -- Yosys Open SYnthesis Suite
3 *
4 * Copyright (C) 2012 Clifford Wolf <clifford@clifford.at>
5 *
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.
9 *
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.
17 *
18 */
19
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/
24
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 <string>
31
32 USING_YOSYS_NAMESPACE
33 PRIVATE_NAMESPACE_BEGIN
34
35 struct BtorWorker
36 {
37 std::ostream &f;
38 SigMap sigmap;
39 RTLIL::Module *module;
40 bool verbose;
41 bool single_bad;
42 bool cover_mode;
43
44 int next_nid = 1;
45 int initstate_nid = -1;
46
47 // <width> => <sid>
48 dict<int, int> sorts_bv;
49
50 // (<address-width>, <data-width>) => <sid>
51 dict<pair<int, int>, int> sorts_mem;
52
53 // SigBit => (<nid>, <bitidx>)
54 dict<SigBit, pair<int, int>> bit_nid;
55
56 // <nid> => <bvwidth>
57 dict<int, int> nid_width;
58
59 // SigSpec => <nid>
60 dict<SigSpec, int> sig_nid;
61
62 // bit to driving cell
63 dict<SigBit, Cell*> bit_cell;
64
65 // nids for constants
66 dict<Const, int> consts;
67
68 // ff inputs that need to be evaluated (<nid>, <ff_cell>)
69 vector<pair<int, Cell*>> ff_todo;
70
71 pool<Cell*> cell_recursion_guard;
72 vector<int> bad_properties;
73 dict<SigBit, bool> initbits;
74 pool<Wire*> statewires;
75 pool<string> srcsymbols;
76
77 string indent, info_filename;
78 vector<string> info_lines;
79 dict<int, int> info_clocks;
80
81 void btorf(const char *fmt, ...)
82 {
83 va_list ap;
84 va_start(ap, fmt);
85 f << indent << vstringf(fmt, ap);
86 va_end(ap);
87 }
88
89 void infof(const char *fmt, ...)
90 {
91 va_list ap;
92 va_start(ap, fmt);
93 info_lines.push_back(vstringf(fmt, ap));
94 va_end(ap);
95 }
96
97 template<typename T>
98 string getinfo(T *obj, bool srcsym = false)
99 {
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)) {
109 src = s;
110 break;
111 }
112 }
113 }
114 srcsymbols.insert(src);
115 infostr = src;
116 } else {
117 infostr += " ; " + src;
118 }
119 }
120 return infostr;
121 }
122
123 void btorf_push(const string &id)
124 {
125 if (verbose) {
126 f << indent << stringf(" ; begin %s\n", id.c_str());
127 indent += " ";
128 }
129 }
130
131 void btorf_pop(const string &id)
132 {
133 if (verbose) {
134 indent = indent.substr(4);
135 f << indent << stringf(" ; end %s\n", id.c_str());
136 }
137 }
138
139 int get_bv_sid(int width)
140 {
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;
145 }
146 return sorts_bv.at(width);
147 }
148
149 int get_mem_sid(int abits, int dbits)
150 {
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;
158 }
159 return sorts_mem.at(key);
160 }
161
162 void add_nid_sig(int nid, const SigSpec &sig)
163 {
164 if (verbose)
165 f << indent << stringf("; %d %s\n", nid, log_signal(sig));
166
167 for (int i = 0; i < GetSize(sig); i++)
168 bit_nid[sig[i]] = make_pair(nid, i);
169
170 sig_nid[sig] = nid;
171 nid_width[nid] = GetSize(sig);
172 }
173
174 void export_cell(Cell *cell)
175 {
176 if (cell_recursion_guard.count(cell)) {
177 string cell_list;
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());
181 }
182
183 cell_recursion_guard.insert(cell);
184 btorf_push(log_id(cell));
185
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_"))
188 {
189 string btor_op;
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());
205
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")));
209
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;
212
213 if (btor_op == "shift" && !b_signed)
214 btor_op = "srl";
215
216 if (cell->type.in("$shl", "$sshl", "$shr", "$sshr"))
217 b_signed = false;
218
219 if (cell->type == "$sshr" && !a_signed)
220 btor_op = "srl";
221
222 int sid = get_bv_sid(width);
223 int nid;
224
225 if (btor_op == "shift")
226 {
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);
229
230 int nid_r = next_nid++;
231 btorf("%d srl %d %d %d\n", nid_r, sid, nid_a, nid_b);
232
233 int nid_b_neg = next_nid++;
234 btorf("%d neg %d %d\n", nid_b_neg, sid, nid_b);
235
236 int nid_l = next_nid++;
237 btorf("%d sll %d %d %d\n", nid_l, sid, nid_a, nid_b_neg);
238
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);
243
244 nid = next_nid++;
245 btorf("%d ite %d %d %d %d %s\n", nid, sid, nid_b_ltz, nid_l, nid_r, getinfo(cell).c_str());
246 }
247 else
248 {
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);
251
252 nid = next_nid++;
253 btorf("%d %s %d %d %d %s\n", nid, btor_op.c_str(), sid, nid_a, nid_b, getinfo(cell).c_str());
254 }
255
256 SigSpec sig = sigmap(cell->getPort("\\Y"));
257
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);
262 nid = nid2;
263 }
264
265 add_nid_sig(nid, sig);
266 goto okay;
267 }
268
269 if (cell->type.in("$div", "$mod"))
270 {
271 string btor_op;
272 if (cell->type == "$div") btor_op = "div";
273 if (cell->type == "$mod") btor_op = "rem";
274 log_assert(!btor_op.empty());
275
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")));
279
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;
282
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);
285
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());
289
290 SigSpec sig = sigmap(cell->getPort("\\Y"));
291
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);
296 nid = nid2;
297 }
298
299 add_nid_sig(nid, sig);
300 goto okay;
301 }
302
303 if (cell->type.in("$_ANDNOT_", "$_ORNOT_"))
304 {
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"));
308
309 int nid1 = next_nid++;
310 int nid2 = next_nid++;
311
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());
315 }
316
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());
320 }
321
322 SigSpec sig = sigmap(cell->getPort("\\Y"));
323 add_nid_sig(nid2, sig);
324 goto okay;
325 }
326
327 if (cell->type.in("$_OAI3_", "$_AOI3_"))
328 {
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"));
333
334 int nid1 = next_nid++;
335 int nid2 = next_nid++;
336 int nid3 = next_nid++;
337
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());
342 }
343
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());
348 }
349
350 SigSpec sig = sigmap(cell->getPort("\\Y"));
351 add_nid_sig(nid3, sig);
352 goto okay;
353 }
354
355 if (cell->type.in("$_OAI4_", "$_AOI4_"))
356 {
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"));
362
363 int nid1 = next_nid++;
364 int nid2 = next_nid++;
365 int nid3 = next_nid++;
366 int nid4 = next_nid++;
367
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());
373 }
374
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());
380 }
381
382 SigSpec sig = sigmap(cell->getPort("\\Y"));
383 add_nid_sig(nid4, sig);
384 goto okay;
385 }
386
387 if (cell->type.in("$lt", "$le", "$eq", "$eqx", "$ne", "$nex", "$ge", "$gt"))
388 {
389 string btor_op;
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());
397
398 int width = 1;
399 width = std::max(width, GetSize(cell->getPort("\\A")));
400 width = std::max(width, GetSize(cell->getPort("\\B")));
401
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;
404
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);
408
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());
412 } else {
413 btorf("%d %s %d %d %d %s\n", nid, btor_op.c_str(), sid, nid_a, nid_b, getinfo(cell).c_str());
414 }
415
416 SigSpec sig = sigmap(cell->getPort("\\Y"));
417
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);
422 nid = nid2;
423 }
424
425 add_nid_sig(nid, sig);
426 goto okay;
427 }
428
429 if (cell->type.in("$not", "$neg", "$_NOT_"))
430 {
431 string btor_op;
432 if (cell->type.in("$not", "$_NOT_")) btor_op = "not";
433 if (cell->type == "$neg") btor_op = "neg";
434 log_assert(!btor_op.empty());
435
436 int width = GetSize(cell->getPort("\\Y"));
437 width = std::max(width, GetSize(cell->getPort("\\A")));
438
439 bool a_signed = cell->hasParam("\\A_SIGNED") ? cell->getParam("\\A_SIGNED").as_bool() : false;
440
441 int sid = get_bv_sid(width);
442 int nid_a = get_sig_nid(cell->getPort("\\A"), width, a_signed);
443
444 int nid = next_nid++;
445 btorf("%d %s %d %d\n", nid, btor_op.c_str(), sid, nid_a, getinfo(cell).c_str());
446
447 SigSpec sig = sigmap(cell->getPort("\\Y"));
448
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);
453 nid = nid2;
454 }
455
456 add_nid_sig(nid, sig);
457 goto okay;
458 }
459
460 if (cell->type.in("$logic_and", "$logic_or", "$logic_not"))
461 {
462 string btor_op;
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());
467
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;
471
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);
475 nid_a = nid_red_a;
476 }
477
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);
481 nid_b = nid_red_b;
482 }
483
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());
487 else
488 btorf("%d %s %d %d\n", nid, btor_op.c_str(), sid, nid_a, getinfo(cell).c_str());
489
490 SigSpec sig = sigmap(cell->getPort("\\Y"));
491
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);
497 nid = nid2;
498 }
499
500 add_nid_sig(nid, sig);
501 goto okay;
502 }
503
504 if (cell->type.in("$reduce_and", "$reduce_or", "$reduce_bool", "$reduce_xor", "$reduce_xnor"))
505 {
506 string btor_op;
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());
511
512 int sid = get_bv_sid(1);
513 int nid_a = get_sig_nid(cell->getPort("\\A"));
514
515 int nid = next_nid++;
516
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);
521 nid = nid2;
522 } else {
523 btorf("%d %s %d %d %s\n", nid, btor_op.c_str(), sid, nid_a, getinfo(cell).c_str());
524 }
525
526 SigSpec sig = sigmap(cell->getPort("\\Y"));
527
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);
533 nid = nid2;
534 }
535
536 add_nid_sig(nid, sig);
537 goto okay;
538 }
539
540 if (cell->type.in("$mux", "$_MUX_", "$_NMUX_"))
541 {
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"));
546
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);
550
551 int sid = get_bv_sid(GetSize(sig_y));
552 int nid = next_nid++;
553
554 if (cell->type == "$_NMUX_") {
555 int tmp = nid;
556 nid = next_nid++;
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());
559 } else {
560 btorf("%d ite %d %d %d %d %s\n", nid, sid, nid_s, nid_b, nid_a, getinfo(cell).c_str());
561 }
562
563 add_nid_sig(nid, sig_y);
564 goto okay;
565 }
566
567 if (cell->type == "$pmux")
568 {
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"));
573
574 int width = GetSize(sig_a);
575 int sid = get_bv_sid(width);
576 int nid = get_sig_nid(sig_a);
577
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());
584 else
585 btorf("%d ite %d %d %d %d\n", nid2, sid, nid_s, nid_b, nid);
586 nid = nid2;
587 }
588
589 add_nid_sig(nid, sig_y);
590 goto okay;
591 }
592
593 if (cell->type.in("$dff", "$ff", "$_DFF_P_", "$_DFF_N_", "$_FF_"))
594 {
595 SigSpec sig_d = sigmap(cell->getPort("\\D"));
596 SigSpec sig_q = sigmap(cell->getPort("\\Q"));
597
598 if (!info_filename.empty() && cell->type.in("$dff", "$_DFF_P_", "$_DFF_N_"))
599 {
600 SigSpec sig_c = sigmap(cell->getPort(cell->type == "$dff" ? "\\CLK" : "\\C"));
601 int nid = get_sig_nid(sig_c);
602 bool negedge = false;
603
604 if (cell->type == "$_DFF_N_")
605 negedge = true;
606
607 if (cell->type == "$dff" && !cell->getParam("\\CLK_POLARITY").as_bool())
608 negedge = true;
609
610 info_clocks[nid] |= negedge ? 2 : 1;
611 }
612
613 IdString symbol;
614
615 if (sig_q.is_wire()) {
616 Wire *w = sig_q.as_wire();
617 if (w->port_id == 0) {
618 statewires.insert(w);
619 symbol = w->name;
620 }
621 }
622
623 Const initval;
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);
627 else
628 initval.bits.push_back(State::Sx);
629
630 int nid_init_val = -1;
631
632 if (!initval.is_fully_undef())
633 nid_init_val = get_sig_nid(initval, -1, false, true);
634
635 int sid = get_bv_sid(GetSize(sig_q));
636 int nid = next_nid++;
637
638 if (symbol.empty())
639 btorf("%d state %d\n", nid, sid);
640 else
641 btorf("%d state %d %s\n", nid, sid, log_id(symbol));
642
643 if (nid_init_val >= 0) {
644 int nid_init = next_nid++;
645 if (verbose)
646 btorf("; initval = %s\n", log_signal(initval));
647 btorf("%d init %d %d %d\n", nid_init, sid, nid, nid_init_val);
648 }
649
650 ff_todo.push_back(make_pair(nid, cell));
651 add_nid_sig(nid, sig_q);
652 goto okay;
653 }
654
655 if (cell->type.in("$anyconst", "$anyseq"))
656 {
657 SigSpec sig_y = sigmap(cell->getPort("\\Y"));
658
659 int sid = get_bv_sid(GetSize(sig_y));
660 int nid = next_nid++;
661
662 btorf("%d state %d\n", nid, sid);
663
664 if (cell->type == "$anyconst") {
665 int nid2 = next_nid++;
666 btorf("%d next %d %d %d\n", nid2, sid, nid, nid);
667 }
668
669 add_nid_sig(nid, sig_y);
670 goto okay;
671 }
672
673 if (cell->type == "$initstate")
674 {
675 SigSpec sig_y = sigmap(cell->getPort("\\Y"));
676
677 if (initstate_nid < 0)
678 {
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);
686 }
687
688 add_nid_sig(initstate_nid, sig_y);
689 goto okay;
690 }
691
692 if (cell->type == "$mem")
693 {
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();
699
700 Const wr_clk_en = cell->getParam("\\WR_CLK_ENABLE");
701 Const rd_clk_en = cell->getParam("\\RD_CLK_ENABLE");
702
703 bool asyncwr = wr_clk_en.is_fully_zero();
704
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));
708
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));
712
713 SigSpec sig_rd_addr = sigmap(cell->getPort("\\RD_ADDR"));
714 SigSpec sig_rd_data = sigmap(cell->getPort("\\RD_DATA"));
715
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"));
719
720 int data_sid = get_bv_sid(width);
721 int bool_sid = get_bv_sid(1);
722 int sid = get_mem_sid(abits, width);
723
724 Const initdata = cell->getParam("\\INIT");
725 initdata.exts(nwords*width);
726 int nid_init_val = -1;
727
728 if (!initdata.is_fully_undef())
729 {
730 bool constword = true;
731 Const firstword = initdata.extract(0, width);
732
733 for (int i = 1; i < nwords; i++) {
734 Const thisword = initdata.extract(i*width, width);
735 if (thisword != firstword) {
736 constword = false;
737 break;
738 }
739 }
740
741 if (constword)
742 {
743 if (verbose)
744 btorf("; initval = %s\n", log_signal(firstword));
745 nid_init_val = get_sig_nid(firstword, -1, false, true);
746 }
747 else
748 {
749 nid_init_val = next_nid++;
750 btorf("%d state %d\n", nid_init_val, sid);
751
752 for (int i = 0; i < nwords; i++) {
753 Const thisword = initdata.extract(i*width, width);
754 if (thisword.is_fully_undef())
755 continue;
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++;
761 if (verbose)
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);
764 }
765 }
766 }
767
768
769 int nid = next_nid++;
770 int nid_head = nid;
771
772 if (cell->name[0] == '$')
773 btorf("%d state %d\n", nid, sid);
774 else
775 btorf("%d state %d %s\n", nid, sid, log_id(cell));
776
777 if (nid_init_val >= 0)
778 {
779 int nid_init = next_nid++;
780 btorf("%d init %d %d %d\n", nid_init, sid, nid, nid_init_val);
781 }
782
783 if (asyncwr)
784 {
785 for (int port = 0; port < wrports; port++)
786 {
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);
790
791 int wa_nid = get_sig_nid(wa);
792 int wd_nid = get_sig_nid(wd);
793 int we_nid = get_sig_nid(we);
794
795 int nid2 = next_nid++;
796 btorf("%d read %d %d %d\n", nid2, data_sid, nid_head, wa_nid);
797
798 int nid3 = next_nid++;
799 btorf("%d not %d %d\n", nid3, data_sid, we_nid);
800
801 int nid4 = next_nid++;
802 btorf("%d and %d %d %d\n", nid4, data_sid, nid2, nid3);
803
804 int nid5 = next_nid++;
805 btorf("%d and %d %d %d\n", nid5, data_sid, wd_nid, we_nid);
806
807 int nid6 = next_nid++;
808 btorf("%d or %d %d %d\n", nid6, data_sid, nid5, nid4);
809
810 int nid7 = next_nid++;
811 btorf("%d write %d %d %d %d\n", nid7, sid, nid_head, wa_nid, nid6);
812
813 int nid8 = next_nid++;
814 btorf("%d redor %d %d\n", nid8, bool_sid, we_nid);
815
816 int nid9 = next_nid++;
817 btorf("%d ite %d %d %d %d\n", nid9, sid, nid8, nid7, nid_head);
818
819 nid_head = nid9;
820 }
821 }
822
823 for (int port = 0; port < rdports; port++)
824 {
825 SigSpec ra = sig_rd_addr.extract(port*abits, abits);
826 SigSpec rd = sig_rd_data.extract(port*width, width);
827
828 int ra_nid = get_sig_nid(ra);
829 int rd_nid = next_nid++;
830
831 btorf("%d read %d %d %d\n", rd_nid, data_sid, nid_head, ra_nid);
832
833 add_nid_sig(rd_nid, rd);
834 }
835
836 if (!asyncwr)
837 {
838 ff_todo.push_back(make_pair(nid, cell));
839 }
840 else
841 {
842 int nid2 = next_nid++;
843 btorf("%d next %d %d %d\n", nid2, sid, nid, nid_head);
844 }
845
846 goto okay;
847 }
848
849 log_error("Unsupported cell type: %s (%s)\n", log_id(cell->type), log_id(cell));
850
851 okay:
852 btorf_pop(log_id(cell));
853 cell_recursion_guard.erase(cell);
854 }
855
856 int get_sig_nid(SigSpec sig, int to_width = -1, bool is_signed = false, bool is_init = false)
857 {
858 int nid = -1;
859 sigmap.apply(sig);
860
861 for (auto bit : sig)
862 if (bit == State::Sx)
863 goto has_undef_bits;
864
865 if (0)
866 {
867 has_undef_bits:
868 SigSpec sig_mask_undef, sig_noundef;
869 int first_undef = -1;
870
871 for (int i = 0; i < GetSize(sig); i++)
872 if (sig[i] == State::Sx) {
873 if (first_undef < 0)
874 first_undef = i;
875 sig_mask_undef.append(State::S1);
876 sig_noundef.append(State::S0);
877 } else {
878 sig_mask_undef.append(State::S0);
879 sig_noundef.append(sig[i]);
880 }
881
882 if (to_width < 0 || first_undef < to_width)
883 {
884 int sid = get_bv_sid(GetSize(sig));
885
886 int nid_input = next_nid++;
887 if (is_init)
888 btorf("%d state %d\n", nid_input, sid);
889 else
890 btorf("%d input %d\n", nid_input, sid);
891
892 int nid_masked_input;
893 if (sig_mask_undef.is_fully_ones()) {
894 nid_masked_input = nid_input;
895 } else {
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);
899 }
900
901 if (sig_noundef.is_fully_zero()) {
902 nid = nid_masked_input;
903 } else {
904 int nid_noundef = get_sig_nid(sig_noundef);
905 nid = next_nid++;
906 btorf("%d or %d %d %d\n", nid, sid, nid_masked_input, nid_noundef);
907 }
908
909 goto extend_or_trim;
910 }
911
912 sig = sig_noundef;
913 }
914
915 if (sig_nid.count(sig) == 0)
916 {
917 // <nid>, <bitidx>
918 vector<pair<int, int>> nidbits;
919
920 // collect all bits
921 for (int i = 0; i < GetSize(sig); i++)
922 {
923 SigBit bit = sig[i];
924
925 if (bit_nid.count(bit) == 0)
926 {
927 if (bit.wire == nullptr)
928 {
929 Const c(bit.data);
930
931 while (i+GetSize(c) < GetSize(sig) && sig[i+GetSize(c)].wire == nullptr)
932 c.bits.push_back(sig[i+GetSize(c)].data);
933
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());
938 consts[c] = nid;
939 nid_width[nid] = GetSize(c);
940 }
941
942 int nid = consts.at(c);
943
944 for (int j = 0; j < GetSize(c); j++)
945 nidbits.push_back(make_pair(nid, j));
946
947 i += GetSize(c)-1;
948 continue;
949 }
950 else
951 {
952 if (bit_cell.count(bit) == 0)
953 {
954 SigSpec s = bit;
955
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)]);
959
960 log_warning("No driver for signal %s.\n", log_signal(s));
961
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);
966
967 for (int j = 0; j < GetSize(s); j++)
968 nidbits.push_back(make_pair(nid, j));
969
970 i += GetSize(s)-1;
971 continue;
972 }
973 else
974 {
975 export_cell(bit_cell.at(bit));
976 log_assert(bit_nid.count(bit));
977 }
978 }
979 }
980
981 nidbits.push_back(bit_nid.at(bit));
982 }
983
984 int width = 0;
985 int nid = -1;
986
987 // group bits and emit slice-concat chain
988 for (int i = 0; i < GetSize(nidbits); i++)
989 {
990 int nid2 = nidbits[i].first;
991 int lower = nidbits[i].second;
992 int upper = lower;
993
994 while (i+1 < GetSize(nidbits) && nidbits[i+1].first == nidbits[i].first &&
995 nidbits[i+1].second == nidbits[i].second+1)
996 upper++, i++;
997
998 int nid3 = nid2;
999
1000 if (lower != 0 || upper+1 != nid_width.at(nid2)) {
1001 int sid = get_bv_sid(upper-lower+1);
1002 nid3 = next_nid++;
1003 btorf("%d slice %d %d %d %d\n", nid3, sid, nid2, upper, lower);
1004 }
1005
1006 int nid4 = nid3;
1007
1008 if (nid >= 0) {
1009 int sid = get_bv_sid(width+upper-lower+1);
1010 nid4 = next_nid++;
1011 btorf("%d concat %d %d %d\n", nid4, sid, nid3, nid);
1012 }
1013
1014 width += upper-lower+1;
1015 nid = nid4;
1016 }
1017
1018 sig_nid[sig] = nid;
1019 nid_width[nid] = width;
1020 }
1021
1022 nid = sig_nid.at(sig);
1023
1024 extend_or_trim:
1025 if (to_width >= 0 && to_width != GetSize(sig))
1026 {
1027 if (to_width < GetSize(sig))
1028 {
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);
1032 nid = nid2;
1033 }
1034 else
1035 {
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));
1040 nid = nid2;
1041 }
1042 }
1043
1044 return nid;
1045 }
1046
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)
1049 {
1050 if (!info_filename.empty())
1051 infof("name %s\n", log_id(module));
1052
1053 btorf_push("inputs");
1054
1055 for (auto wire : module->wires())
1056 {
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);
1062 }
1063
1064 if (!wire->port_id || !wire->port_input)
1065 continue;
1066
1067 SigSpec sig = sigmap(wire);
1068 int sid = get_bv_sid(GetSize(sig));
1069 int nid = next_nid++;
1070
1071 btorf("%d input %d %s\n", nid, sid, getinfo(wire).c_str());
1072 add_nid_sig(nid, sig);
1073 }
1074
1075 btorf_pop("inputs");
1076
1077 for (auto cell : module->cells())
1078 for (auto &conn : cell->connections())
1079 {
1080 if (!cell->output(conn.first))
1081 continue;
1082
1083 for (auto bit : sigmap(conn.second))
1084 bit_cell[bit] = cell;
1085 }
1086
1087 for (auto wire : module->wires())
1088 {
1089 if (!wire->port_id || !wire->port_output)
1090 continue;
1091
1092 btorf_push(stringf("output %s", log_id(wire)));
1093
1094 int nid = get_sig_nid(wire);
1095 btorf("%d output %d %s\n", next_nid++, nid, getinfo(wire).c_str());
1096
1097 btorf_pop(stringf("output %s", log_id(wire)));
1098 }
1099
1100 for (auto cell : module->cells())
1101 {
1102 if (cell->type == "$assume")
1103 {
1104 btorf_push(log_id(cell));
1105
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++;
1112
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);
1116
1117 btorf_pop(log_id(cell));
1118 }
1119
1120 if (cell->type == "$assert")
1121 {
1122 btorf_push(log_id(cell));
1123
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++;
1129
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);
1132
1133 if (single_bad && !cover_mode) {
1134 bad_properties.push_back(nid_en_and_not_a);
1135 } else {
1136 if (cover_mode) {
1137 infof("bad %d %s\n", nid_en_and_not_a, getinfo(cell, true).c_str());
1138 } else {
1139 int nid = next_nid++;
1140 btorf("%d bad %d %s\n", nid, nid_en_and_not_a, getinfo(cell, true).c_str());
1141 }
1142 }
1143
1144 btorf_pop(log_id(cell));
1145 }
1146
1147 if (cell->type == "$cover" && cover_mode)
1148 {
1149 btorf_push(log_id(cell));
1150
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++;
1155
1156 btorf("%d and %d %d %d\n", nid_en_and_a, sid, nid_en, nid_a);
1157
1158 if (single_bad) {
1159 bad_properties.push_back(nid_en_and_a);
1160 } else {
1161 int nid = next_nid++;
1162 btorf("%d bad %d %s\n", nid, nid_en_and_a, getinfo(cell, true).c_str());
1163 }
1164
1165 btorf_pop(log_id(cell));
1166 }
1167 }
1168
1169 for (auto wire : module->wires())
1170 {
1171 if (wire->port_id || wire->name[0] == '$')
1172 continue;
1173
1174 btorf_push(stringf("wire %s", log_id(wire)));
1175
1176 int sid = get_bv_sid(GetSize(wire));
1177 int nid = get_sig_nid(sigmap(wire));
1178
1179 if (statewires.count(wire))
1180 continue;
1181
1182 int this_nid = next_nid++;
1183 btorf("%d uext %d %d %d %s\n", this_nid, sid, nid, 0, getinfo(wire).c_str());
1184
1185 btorf_pop(stringf("wire %s", log_id(wire)));
1186 continue;
1187 }
1188
1189 while (!ff_todo.empty())
1190 {
1191 vector<pair<int, Cell*>> todo;
1192 todo.swap(ff_todo);
1193
1194 for (auto &it : todo)
1195 {
1196 int nid = it.first;
1197 Cell *cell = it.second;
1198
1199 btorf_push(stringf("next %s", log_id(cell)));
1200
1201 if (cell->type == "$mem")
1202 {
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();
1206
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"));
1210
1211 int data_sid = get_bv_sid(width);
1212 int bool_sid = get_bv_sid(1);
1213 int sid = get_mem_sid(abits, width);
1214 int nid_head = nid;
1215
1216 for (int port = 0; port < wrports; port++)
1217 {
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);
1221
1222 int wa_nid = get_sig_nid(wa);
1223 int wd_nid = get_sig_nid(wd);
1224 int we_nid = get_sig_nid(we);
1225
1226 int nid2 = next_nid++;
1227 btorf("%d read %d %d %d\n", nid2, data_sid, nid_head, wa_nid);
1228
1229 int nid3 = next_nid++;
1230 btorf("%d not %d %d\n", nid3, data_sid, we_nid);
1231
1232 int nid4 = next_nid++;
1233 btorf("%d and %d %d %d\n", nid4, data_sid, nid2, nid3);
1234
1235 int nid5 = next_nid++;
1236 btorf("%d and %d %d %d\n", nid5, data_sid, wd_nid, we_nid);
1237
1238 int nid6 = next_nid++;
1239 btorf("%d or %d %d %d\n", nid6, data_sid, nid5, nid4);
1240
1241 int nid7 = next_nid++;
1242 btorf("%d write %d %d %d %d\n", nid7, sid, nid_head, wa_nid, nid6);
1243
1244 int nid8 = next_nid++;
1245 btorf("%d redor %d %d\n", nid8, bool_sid, we_nid);
1246
1247 int nid9 = next_nid++;
1248 btorf("%d ite %d %d %d %d\n", nid9, sid, nid8, nid7, nid_head);
1249
1250 nid_head = nid9;
1251 }
1252
1253 int nid2 = next_nid++;
1254 btorf("%d next %d %d %d %s\n", nid2, sid, nid, nid_head, getinfo(cell).c_str());
1255 }
1256 else
1257 {
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());
1262 }
1263
1264 btorf_pop(stringf("next %s", log_id(cell)));
1265 }
1266 }
1267
1268 while (!bad_properties.empty())
1269 {
1270 vector<int> todo;
1271 bad_properties.swap(todo);
1272
1273 int sid = get_bv_sid(1);
1274 int cursor = 0;
1275
1276 while (cursor+1 < GetSize(todo))
1277 {
1278 int nid_a = todo[cursor++];
1279 int nid_b = todo[cursor++];
1280 int nid = next_nid++;
1281
1282 bad_properties.push_back(nid);
1283 btorf("%d or %d %d %d\n", nid, sid, nid_a, nid_b);
1284 }
1285
1286 if (!bad_properties.empty()) {
1287 if (cursor < GetSize(todo))
1288 bad_properties.push_back(todo[cursor++]);
1289 log_assert(cursor == GetSize(todo));
1290 } else {
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]);
1295 }
1296 }
1297
1298 if (!info_filename.empty())
1299 {
1300 for (auto &it : info_clocks)
1301 {
1302 switch (it.second)
1303 {
1304 case 1:
1305 infof("posedge %d\n", it.first);
1306 break;
1307 case 2:
1308 infof("negedge %d\n", it.first);
1309 break;
1310 case 3:
1311 infof("event %d\n", it.first);
1312 break;
1313 default:
1314 log_abort();
1315 }
1316 }
1317
1318 std::ofstream f;
1319 f.open(info_filename.c_str(), std::ofstream::trunc);
1320 if (f.fail())
1321 log_error("Can't open file `%s' for writing: %s\n", info_filename.c_str(), strerror(errno));
1322 for (auto &it : info_lines)
1323 f << it;
1324 f.close();
1325 }
1326 }
1327 };
1328
1329 struct BtorBackend : public Backend {
1330 BtorBackend() : Backend("btor", "write design to BTOR file") { }
1331 void help() YS_OVERRIDE
1332 {
1333 // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
1334 log("\n");
1335 log(" write_btor [options] [filename]\n");
1336 log("\n");
1337 log("Write a BTOR description of the current design.\n");
1338 log("\n");
1339 log(" -v\n");
1340 log(" Add comments and indentation to BTOR output file\n");
1341 log("\n");
1342 log(" -s\n");
1343 log(" Output only a single bad property for all asserts\n");
1344 log("\n");
1345 log(" -c\n");
1346 log(" Output cover properties using 'bad' statements instead of asserts\n");
1347 log("\n");
1348 log(" -i <filename>\n");
1349 log(" Create additional info file with auxiliary information\n");
1350 log("\n");
1351 }
1352 void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
1353 {
1354 bool verbose = false, single_bad = false, cover_mode = false;
1355 string info_filename;
1356
1357 log_header(design, "Executing BTOR backend.\n");
1358
1359 size_t argidx;
1360 for (argidx = 1; argidx < args.size(); argidx++)
1361 {
1362 if (args[argidx] == "-v") {
1363 verbose = true;
1364 continue;
1365 }
1366 if (args[argidx] == "-s") {
1367 single_bad = true;
1368 continue;
1369 }
1370 if (args[argidx] == "-c") {
1371 cover_mode = true;
1372 continue;
1373 }
1374 if (args[argidx] == "-i" && argidx+1 < args.size()) {
1375 info_filename = args[++argidx];
1376 continue;
1377 }
1378 break;
1379 }
1380 extra_args(f, filename, args, argidx);
1381
1382 RTLIL::Module *topmod = design->top_module();
1383
1384 if (topmod == nullptr)
1385 log_cmd_error("No top module found.\n");
1386
1387 *f << stringf("; BTOR description generated by %s for module %s.\n",
1388 yosys_version_str, log_id(topmod));
1389
1390 BtorWorker(*f, topmod, verbose, single_bad, cover_mode, info_filename);
1391
1392 *f << stringf("; end of yosys output\n");
1393 }
1394 } BtorBackend;
1395
1396 PRIVATE_NAMESPACE_END