Add support for more cell types to btor back-end
[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 #include "kernel/rtlil.h"
21 #include "kernel/register.h"
22 #include "kernel/sigtools.h"
23 #include "kernel/celltypes.h"
24 #include "kernel/log.h"
25 #include <string>
26
27 USING_YOSYS_NAMESPACE
28 PRIVATE_NAMESPACE_BEGIN
29
30 struct BtorWorker
31 {
32 std::ostream &f;
33 SigMap sigmap;
34 RTLIL::Module *module;
35 bool verbose;
36
37 int next_nid = 1;
38 int initstate_nid = -1;
39
40 // <width> => <sid>
41 dict<int, int> sorts_bv;
42
43 // (<address-width>, <data-width>) => <sid>
44 dict<pair<int, int>, int> sorts_mem;
45
46 // SigBit => (<nid>, <bitidx>)
47 dict<SigBit, pair<int, int>> bit_nid;
48
49 // <nid> => <bvwidth>
50 dict<int, int> nid_width;
51
52 // SigSpec => <nid>
53 dict<SigSpec, int> sig_nid;
54
55 // bit to driving cell
56 dict<SigBit, Cell*> bit_cell;
57
58 // nids for constants
59 dict<Const, int> consts;
60
61 // ff inputs that need to be evaluated (<nid>, <ff_cell>)
62 vector<pair<int, Cell*>> ff_todo;
63
64 pool<Cell*> cell_recursion_guard;
65 pool<string> output_symbols;
66 string indent;
67
68 void btorf(const char *fmt, ...)
69 {
70 va_list ap;
71 va_start(ap, fmt);
72 f << indent << vstringf(fmt, ap);
73 va_end(ap);
74 }
75
76 void btorf_push(const string &id)
77 {
78 if (verbose) {
79 f << indent << stringf(" ; begin %s\n", id.c_str());
80 indent += " ";
81 }
82 }
83
84 void btorf_pop(const string &id)
85 {
86 if (verbose) {
87 indent = indent.substr(4);
88 f << indent << stringf(" ; end %s\n", id.c_str());
89 }
90 }
91
92 int get_bv_sid(int width)
93 {
94 if (sorts_bv.count(width) == 0) {
95 int nid = next_nid++;
96 btorf("%d sort bitvec %d\n", nid, width);
97 sorts_bv[width] = nid;
98 }
99 return sorts_bv.at(width);
100 }
101
102 void add_nid_sig(int nid, const SigSpec &sig)
103 {
104 for (int i = 0; i < GetSize(sig); i++)
105 bit_nid[sig[i]] = make_pair(nid, i);
106
107 sig_nid[sig] = nid;
108 nid_width[nid] = GetSize(sig);
109 }
110
111 void export_cell(Cell *cell)
112 {
113 log_assert(cell_recursion_guard.count(cell) == 0);
114 cell_recursion_guard.insert(cell);
115 btorf_push(log_id(cell));
116
117 if (cell->type.in("$add", "$sub", "$and", "$or", "$xor", "$xnor", "$shl", "$sshl", "$shr", "$sshr",
118 "$_AND_", "$_NAND_", "$_OR_", "$_NOR_", "$_XOR_", "$_XNOR_"))
119 {
120 string btor_op;
121 if (cell->type == "$add") btor_op = "add";
122 if (cell->type == "$sub") btor_op = "sub";
123 if (cell->type.in("$shl", "$sshl")) btor_op = "sll";
124 if (cell->type == "$shr") btor_op = "srl";
125 if (cell->type == "$sshr") btor_op = "sra";
126 if (cell->type.in("$and", "$_AND_")) btor_op = "and";
127 if (cell->type.in("$or", "$_OR_")) btor_op = "or";
128 if (cell->type.in("$xor", "$_XOR_")) btor_op = "xor";
129 if (cell->type == "$_NAND_") btor_op = "nand";
130 if (cell->type == "$_NOR_") btor_op = "nor";
131 if (cell->type.in("$xnor", "$_XNOR_")) btor_op = "xnor";
132 log_assert(!btor_op.empty());
133
134 int width = GetSize(cell->getPort("\\Y"));
135 width = std::max(width, GetSize(cell->getPort("\\A")));
136 width = std::max(width, GetSize(cell->getPort("\\B")));
137
138 bool a_signed = cell->hasParam("\\A_SIGNED") ? cell->getParam("\\A_SIGNED").as_bool() : false;
139 bool b_signed = cell->hasParam("\\B_SIGNED") ? cell->getParam("\\B_SIGNED").as_bool() : false;
140
141 if (cell->type.in("$shl", "$shr")) {
142 a_signed = false;
143 b_signed = false;
144 }
145
146 int sid = get_bv_sid(width);
147 int nid_a = get_sig_nid(cell->getPort("\\A"), width, a_signed);
148 int nid_b = get_sig_nid(cell->getPort("\\B"), width, b_signed);
149
150 int nid = next_nid++;
151 btorf("%d %s %d %d %d\n", nid, btor_op.c_str(), sid, nid_a, nid_b);
152
153 SigSpec sig = sigmap(cell->getPort("\\Y"));
154
155 if (GetSize(sig) < width) {
156 int sid = get_bv_sid(GetSize(sig));
157 int nid2 = next_nid++;
158 btorf("%d slice %d %d %d 0\n", nid2, sid, nid, GetSize(sig)-1);
159 nid = nid2;
160 }
161
162 add_nid_sig(nid, sig);
163 goto okay;
164 }
165
166 if (cell->type.in("$_ANDNOT_", "$_ORNOT_"))
167 {
168 int sid = get_bv_sid(1);
169 int nid_a = get_sig_nid(cell->getPort("\\A"));
170 int nid_b = get_sig_nid(cell->getPort("\\B"));
171
172 int nid1 = next_nid++;
173 int nid2 = next_nid++;
174
175 if (cell->type == "$_ANDNOT_") {
176 btorf("%d not %d %d\n", nid1, sid, nid_b);
177 btorf("%d and %d %d %d\n", nid2, sid, nid_a, nid1);
178 }
179
180 if (cell->type == "$_ORNOT_") {
181 btorf("%d not %d %d\n", nid1, sid, nid_b);
182 btorf("%d or %d %d %d\n", nid2, sid, nid_a, nid1);
183 }
184
185 SigSpec sig = sigmap(cell->getPort("\\Y"));
186 add_nid_sig(nid2, sig);
187 goto okay;
188 }
189
190 if (cell->type.in("$_OAI3_", "$_AOI3_"))
191 {
192 int sid = get_bv_sid(1);
193 int nid_a = get_sig_nid(cell->getPort("\\A"));
194 int nid_b = get_sig_nid(cell->getPort("\\B"));
195 int nid_c = get_sig_nid(cell->getPort("\\C"));
196
197 int nid1 = next_nid++;
198 int nid2 = next_nid++;
199 int nid3 = next_nid++;
200
201 if (cell->type == "$_OAI3_") {
202 btorf("%d or %d %d %d\n", nid1, sid, nid_a, nid_b);
203 btorf("%d and %d %d %d\n", nid2, sid, nid1, nid_c);
204 btorf("%d not %d %d\n", nid3, sid, nid2);
205 }
206
207 if (cell->type == "$_AOI3_") {
208 btorf("%d and %d %d %d\n", nid1, sid, nid_a, nid_b);
209 btorf("%d or %d %d %d\n", nid2, sid, nid1, nid_c);
210 btorf("%d not %d %d\n", nid3, sid, nid2);
211 }
212
213 SigSpec sig = sigmap(cell->getPort("\\Y"));
214 add_nid_sig(nid3, sig);
215 goto okay;
216 }
217
218 if (cell->type.in("$_OAI4_", "$_AOI4_"))
219 {
220 int sid = get_bv_sid(1);
221 int nid_a = get_sig_nid(cell->getPort("\\A"));
222 int nid_b = get_sig_nid(cell->getPort("\\B"));
223 int nid_c = get_sig_nid(cell->getPort("\\C"));
224 int nid_d = get_sig_nid(cell->getPort("\\D"));
225
226 int nid1 = next_nid++;
227 int nid2 = next_nid++;
228 int nid3 = next_nid++;
229 int nid4 = next_nid++;
230
231 if (cell->type == "$_OAI4_") {
232 btorf("%d or %d %d %d\n", nid1, sid, nid_a, nid_b);
233 btorf("%d or %d %d %d\n", nid2, sid, nid_c, nid_d);
234 btorf("%d and %d %d %d\n", nid3, sid, nid1, nid2);
235 btorf("%d not %d %d\n", nid4, sid, nid3);
236 }
237
238 if (cell->type == "$_AOI4_") {
239 btorf("%d and %d %d %d\n", nid1, sid, nid_a, nid_b);
240 btorf("%d and %d %d %d\n", nid2, sid, nid_c, nid_d);
241 btorf("%d or %d %d %d\n", nid3, sid, nid1, nid2);
242 btorf("%d not %d %d\n", nid4, sid, nid3);
243 }
244
245 SigSpec sig = sigmap(cell->getPort("\\Y"));
246 add_nid_sig(nid4, sig);
247 goto okay;
248 }
249
250 if (cell->type.in("$lt", "$le", "$eq", "$eqx", "$ne", "$nex", "$ge", "$gt"))
251 {
252 string btor_op;
253 if (cell->type == "$lt") btor_op = "lt";
254 if (cell->type == "$le") btor_op = "lte";
255 if (cell->type.in("$eq", "$eqx")) btor_op = "eq";
256 if (cell->type.in("$ne", "$nex")) btor_op = "ne";
257 if (cell->type == "$ge") btor_op = "gte";
258 if (cell->type == "$gt") btor_op = "gt";
259 log_assert(!btor_op.empty());
260
261 int width = 1;
262 width = std::max(width, GetSize(cell->getPort("\\A")));
263 width = std::max(width, GetSize(cell->getPort("\\B")));
264
265 bool a_signed = cell->hasParam("\\A_SIGNED") ? cell->getParam("\\A_SIGNED").as_bool() : false;
266 bool b_signed = cell->hasParam("\\B_SIGNED") ? cell->getParam("\\B_SIGNED").as_bool() : false;
267
268 int sid = get_bv_sid(1);
269 int nid_a = get_sig_nid(cell->getPort("\\A"), width, a_signed);
270 int nid_b = get_sig_nid(cell->getPort("\\B"), width, b_signed);
271
272 int nid = next_nid++;
273 if (cell->type.in("$lt", "$le", "$ge", "$gt")) {
274 btorf("%d %c%s %d %d %d\n", nid, a_signed || b_signed ? 's' : 'u', btor_op.c_str(), sid, nid_a, nid_b);
275 } else {
276 btorf("%d %s %d %d %d\n", nid, btor_op.c_str(), sid, nid_a, nid_b);
277 }
278
279 SigSpec sig = sigmap(cell->getPort("\\Y"));
280
281 if (GetSize(sig) > 1) {
282 int sid = get_bv_sid(GetSize(sig));
283 int nid2 = next_nid++;
284 btorf("%d uext %d %d %d\n", nid2, sid, nid, GetSize(sig) - 1);
285 nid = nid2;
286 }
287
288 add_nid_sig(nid, sig);
289 goto okay;
290 }
291
292 if (cell->type.in("$not", "$neg", "$_NOT_"))
293 {
294 string btor_op;
295 if (cell->type.in("$not", "$_NOT_")) btor_op = "not";
296 if (cell->type == "$neg") btor_op = "neg";
297 log_assert(!btor_op.empty());
298
299 int width = GetSize(cell->getPort("\\Y"));
300 width = std::max(width, GetSize(cell->getPort("\\A")));
301
302 bool a_signed = cell->hasParam("\\A_SIGNED") ? cell->getParam("\\A_SIGNED").as_bool() : false;
303
304 int sid = get_bv_sid(width);
305 int nid_a = get_sig_nid(cell->getPort("\\A"), width, a_signed);
306
307 int nid = next_nid++;
308 btorf("%d %s %d %d\n", nid, btor_op.c_str(), sid, nid_a);
309
310 SigSpec sig = sigmap(cell->getPort("\\Y"));
311
312 if (GetSize(sig) < width) {
313 int sid = get_bv_sid(GetSize(sig));
314 int nid2 = next_nid++;
315 btorf("%d slice %d %d %d 0\n", nid2, sid, nid, GetSize(sig)-1);
316 nid = nid2;
317 }
318
319 add_nid_sig(nid, sig);
320 goto okay;
321 }
322
323 if (cell->type.in("$logic_and", "$logic_or", "$logic_not"))
324 {
325 string btor_op;
326 if (cell->type == "$logic_and") btor_op = "and";
327 if (cell->type == "$logic_or") btor_op = "or";
328 if (cell->type == "$logic_not") btor_op = "not";
329 log_assert(!btor_op.empty());
330
331 int sid = get_bv_sid(1);
332 int nid_a = get_sig_nid(cell->getPort("\\A"));
333 int nid_b = btor_op != "not" ? get_sig_nid(cell->getPort("\\B")) : 0;
334
335 if (GetSize(cell->getPort("\\A")) > 1) {
336 int nid_red_a = next_nid++;
337 btorf("%d redor %d %d\n", nid_red_a, sid, nid_a);
338 nid_a = nid_red_a;
339 }
340
341 if (btor_op != "not" && GetSize(cell->getPort("\\B")) > 1) {
342 int nid_red_b = next_nid++;
343 btorf("%d redor %d %d\n", nid_red_b, sid, nid_b);
344 nid_b = nid_red_b;
345 }
346
347 int nid = next_nid++;
348 if (btor_op != "not")
349 btorf("%d %s %d %d %d\n", nid, btor_op.c_str(), sid, nid_a, nid_b);
350 else
351 btorf("%d %s %d %d\n", nid, btor_op.c_str(), sid, nid_a);
352
353 SigSpec sig = sigmap(cell->getPort("\\Y"));
354
355 if (GetSize(sig) > 1) {
356 int sid = get_bv_sid(GetSize(sig));
357 int zeros_nid = get_sig_nid(Const(0, GetSize(sig)-1));
358 int nid2 = next_nid++;
359 btorf("%d concat %d %d %d\n", nid2, sid, zeros_nid, nid);
360 nid = nid2;
361 }
362
363 add_nid_sig(nid, sig);
364 goto okay;
365 }
366
367 if (cell->type.in("$reduce_and", "$reduce_or", "$reduce_bool", "$reduce_xor", "$reduce_xnor"))
368 {
369 string btor_op;
370 if (cell->type == "$reduce_and") btor_op = "redand";
371 if (cell->type.in("$reduce_or", "$reduce_bool")) btor_op = "redor";
372 if (cell->type.in("$reduce_xor", "$reduce_xnor")) btor_op = "redxor";
373 log_assert(!btor_op.empty());
374
375 int sid = get_bv_sid(1);
376 int nid_a = get_sig_nid(cell->getPort("\\A"));
377
378 int nid = next_nid++;
379 btorf("%d %s %d %d\n", nid, btor_op.c_str(), sid, nid_a);
380
381 if (cell->type == "$reduce_xnor") {
382 int nid2 = next_nid++;
383 btorf("%d not %d %d %d\n", nid2, sid, nid);
384 nid = nid2;
385 }
386
387 SigSpec sig = sigmap(cell->getPort("\\Y"));
388
389 if (GetSize(sig) > 1) {
390 int sid = get_bv_sid(GetSize(sig));
391 int zeros_nid = get_sig_nid(Const(0, GetSize(sig)-1));
392 int nid2 = next_nid++;
393 btorf("%d concat %d %d %d\n", nid2, sid, zeros_nid, nid);
394 nid = nid2;
395 }
396
397 add_nid_sig(nid, sig);
398 goto okay;
399 }
400
401 if (cell->type.in("$mux", "$_MUX_"))
402 {
403 SigSpec sig_a = sigmap(cell->getPort("\\A"));
404 SigSpec sig_b = sigmap(cell->getPort("\\B"));
405 SigSpec sig_s = sigmap(cell->getPort("\\S"));
406 SigSpec sig_y = sigmap(cell->getPort("\\Y"));
407
408 int nid_a = get_sig_nid(sig_a);
409 int nid_b = get_sig_nid(sig_b);
410 int nid_s = get_sig_nid(sig_s);
411
412 int sid = get_bv_sid(GetSize(sig_y));
413 int nid = next_nid++;
414 btorf("%d ite %d %d %d %d\n", nid, sid, nid_s, nid_b, nid_a);
415
416 add_nid_sig(nid, sig_y);
417 goto okay;
418 }
419
420 if (cell->type.in("$dff", "$ff", "$_DFF_P_", "$_DFF_N", "$_FF_"))
421 {
422 SigSpec sig_d = sigmap(cell->getPort("\\D"));
423 SigSpec sig_q = sigmap(cell->getPort("\\Q"));
424
425 string symbol = log_signal(sig_q);
426 if (symbol.find(' ') != string::npos)
427 symbol = log_id(cell);
428
429 if (symbol[0] == '\\')
430 symbol = symbol.substr(1);
431
432 int sid = get_bv_sid(GetSize(sig_q));
433 int nid = next_nid++;
434
435 if (output_symbols.count(symbol))
436 btorf("%d state %d\n", nid, sid);
437 else
438 btorf("%d state %d %s\n", nid, sid, symbol.c_str());
439
440 ff_todo.push_back(make_pair(nid, cell));
441 add_nid_sig(nid, sig_q);
442 goto okay;
443 }
444
445 if (cell->type == "$initstate")
446 {
447 SigSpec sig_y = sigmap(cell->getPort("\\Y"));
448
449 if (initstate_nid < 0)
450 {
451 int sid = get_bv_sid(1);
452 int one_nid = get_sig_nid(Const(1, 1));
453 int zero_nid = get_sig_nid(Const(0, 1));
454 initstate_nid = next_nid++;
455 btorf("%d state %d\n", initstate_nid, sid);
456 btorf("%d init %d %d %d\n", next_nid++, sid, initstate_nid, one_nid);
457 btorf("%d next %d %d %d\n", next_nid++, sid, initstate_nid, zero_nid);
458 }
459
460 add_nid_sig(initstate_nid, sig_y);
461 goto okay;
462 }
463
464 log_error("Unsupported cell type: %s (%s)\n", log_id(cell->type), log_id(cell));
465
466 okay:
467 btorf_pop(log_id(cell));
468 cell_recursion_guard.erase(cell);
469 }
470
471 int get_sig_nid(SigSpec sig, int to_width = -1, bool is_signed = false)
472 {
473 sigmap.apply(sig);
474
475 if (sig_nid.count(sig) == 0)
476 {
477 // <nid>, <bitidx>
478 vector<pair<int, int>> nidbits;
479
480 // collect all bits
481 for (int i = 0; i < GetSize(sig); i++)
482 {
483 SigBit bit = sig[i];
484
485 if (bit_nid.count(bit) == 0)
486 {
487 if (bit.wire == nullptr)
488 {
489 Const c(bit.data);
490
491 while (i+GetSize(c) < GetSize(sig) && sig[i+GetSize(c)].wire == nullptr)
492 c.bits.push_back(sig[i+GetSize(c)].data);
493
494 if (consts.count(c) == 0) {
495 int sid = get_bv_sid(GetSize(c));
496 int nid = next_nid++;
497 btorf("%d const %d %s\n", nid, sid, c.as_string().c_str());
498 consts[c] = nid;
499 nid_width[nid] = GetSize(c);
500 }
501
502 int nid = consts.at(c);
503
504 for (int j = 0; j < GetSize(c); j++)
505 nidbits.push_back(make_pair(nid, j));
506
507 i += GetSize(c)-1;
508 continue;
509 }
510 else
511 {
512 export_cell(bit_cell.at(bit));
513 log_assert(bit_nid.count(bit));
514 }
515 }
516
517 nidbits.push_back(bit_nid.at(bit));
518 }
519
520 int width = 0;
521 int nid = -1;
522
523 // group bits and emit slice-concat chain
524 for (int i = 0; i < GetSize(nidbits); i++)
525 {
526 int nid2 = nidbits[i].first;
527 int lower = nidbits[i].second;
528 int upper = lower;
529
530 while (i+1 < GetSize(nidbits) && nidbits[i+1].first == nidbits[i].first &&
531 nidbits[i+1].second == nidbits[i].second+1)
532 upper++, i++;
533
534 int nid3 = nid2;
535
536 if (lower != 0 || upper+1 != nid_width.at(nid2)) {
537 int sid = get_bv_sid(upper-lower+1);
538 nid3 = next_nid++;
539 btorf("%d slice %d %d %d %d\n", nid3, sid, nid2, upper, lower);
540 }
541
542 int nid4 = nid3;
543
544 if (nid >= 0) {
545 int sid = get_bv_sid(width+upper-lower+1);
546 nid4 = next_nid++;
547 btorf("%d concat %d %d %d\n", nid4, sid, nid3, nid);
548 }
549
550 width += upper-lower+1;
551 nid = nid4;
552 }
553
554 sig_nid[sig] = nid;
555 nid_width[nid] = width;
556 }
557
558 int nid = sig_nid.at(sig);
559
560 if (to_width >= 0 && to_width != GetSize(sig))
561 {
562 if (to_width < GetSize(sig))
563 {
564 int sid = get_bv_sid(to_width);
565 int nid2 = next_nid++;
566 btorf("%d slice %d %d %d 0\n", nid2, sid, nid, to_width-1);
567 nid = nid2;
568 }
569 else
570 {
571 int sid = get_bv_sid(to_width);
572 int nid2 = next_nid++;
573 btorf("%d %s %d %d %d\n", nid2, is_signed ? "sext" : "uext",
574 sid, nid, to_width - GetSize(sig));
575 nid = nid2;
576 }
577 }
578
579 return nid;
580 }
581
582 BtorWorker(std::ostream &f, RTLIL::Module *module, bool verbose) :
583 f(f), sigmap(module), module(module), verbose(verbose)
584 {
585 btorf_push("inputs");
586
587 for (auto wire : module->wires())
588 {
589 if (!wire->port_id || !wire->port_input)
590 continue;
591
592 SigSpec sig = sigmap(wire);
593 int sid = get_bv_sid(GetSize(sig));
594 int nid = next_nid++;
595
596 btorf("%d input %d %s\n", nid, sid, log_id(wire));
597 add_nid_sig(nid, sig);
598 }
599
600 btorf_pop("inputs");
601
602 for (auto cell : module->cells())
603 for (auto &conn : cell->connections())
604 {
605 if (!cell->output(conn.first))
606 continue;
607
608 for (auto bit : sigmap(conn.second))
609 bit_cell[bit] = cell;
610 }
611
612 for (auto wire : module->wires())
613 if (wire->port_output)
614 output_symbols.insert(log_id(wire));
615
616 for (auto wire : module->wires())
617 {
618 if (!wire->port_id || !wire->port_output)
619 continue;
620
621 btorf_push(stringf("output %s", log_id(wire)));
622
623 int sid = get_bv_sid(GetSize(wire));
624 int nid = get_sig_nid(wire);
625 btorf("%d output %d %d %s\n", next_nid++, sid, nid, log_id(wire));
626
627 btorf_pop(stringf("output %s", log_id(wire)));
628 }
629
630 for (auto cell : module->cells())
631 {
632 if (cell->type == "$assume")
633 {
634 btorf_push(log_id(cell));
635
636 int sid = get_bv_sid(1);
637 int nid_a = get_sig_nid(cell->getPort("\\A"));
638 int nid_en = get_sig_nid(cell->getPort("\\EN"));
639 int nid_not_en = next_nid++;
640 int nid_a_or_not_en = next_nid++;
641 int nid = next_nid++;
642
643 btorf("%d not %d %d\n", nid_not_en, sid, nid_en);
644 btorf("%d or %d %d %d\n", nid_a_or_not_en, sid, nid_a, nid_not_en);
645 btorf("%d constraint %d\n", nid, nid_a_or_not_en);
646
647 btorf_pop(log_id(cell));
648 }
649
650 if (cell->type == "$assert")
651 {
652 btorf_push(log_id(cell));
653
654 int sid = get_bv_sid(1);
655 int nid_a = get_sig_nid(cell->getPort("\\A"));
656 int nid_en = get_sig_nid(cell->getPort("\\EN"));
657 int nid_not_a = next_nid++;
658 int nid_en_and_not_a = next_nid++;
659 int nid = next_nid++;
660
661 btorf("%d not %d %d\n", nid_not_a, sid, nid_a);
662 btorf("%d and %d %d %d\n", nid_en_and_not_a, sid, nid_en, nid_not_a);
663 btorf("%d bad %d\n", nid, nid_en_and_not_a);
664
665 btorf_pop(log_id(cell));
666 }
667 }
668
669 while (!ff_todo.empty())
670 {
671 vector<pair<int, Cell*>> todo;
672 todo.swap(ff_todo);
673
674 for (auto &it : todo)
675 {
676 btorf_push(stringf("next %s", log_id(it.second)));
677
678 SigSpec sig = sigmap(it.second->getPort("\\D"));
679
680 int nid = get_sig_nid(sig);
681 int sid = get_bv_sid(GetSize(sig));
682 btorf("%d next %d %d %d\n", next_nid++, sid, it.first, nid);
683
684 btorf_pop(stringf("next %s", log_id(it.second)));
685 }
686 }
687 }
688 };
689
690 struct BtorBackend : public Backend {
691 BtorBackend() : Backend("btor", "write design to BTOR file") { }
692 virtual void help()
693 {
694 // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
695 log("\n");
696 log(" write_btor [options] [filename]\n");
697 log("\n");
698 log("Write a BTOR description of the current design.\n");
699 log("\n");
700 log(" -v\n");
701 log(" Add comments and indentation to BTOR output file\n");
702 log("\n");
703 }
704 virtual void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design)
705 {
706 bool verbose = false;
707
708 log_header(design, "Executing BTOR backend.\n");
709
710 size_t argidx;
711 for (argidx = 1; argidx < args.size(); argidx++)
712 {
713 if (args[argidx] == "-v") {
714 verbose = true;
715 continue;
716 }
717 break;
718 }
719 extra_args(f, filename, args, argidx);
720
721 RTLIL::Module *topmod = design->top_module();
722
723 if (topmod == nullptr)
724 log_cmd_error("No top module found.\n");
725
726 *f << stringf("; BTOR description generated by %s for module %s.\n",
727 yosys_version_str, log_id(topmod));
728
729 BtorWorker(*f, topmod, verbose);
730
731 *f << stringf("; end of yosys output\n");
732 }
733 } BtorBackend;
734
735 PRIVATE_NAMESPACE_END