projects / yosys.git / blob
? search:
summary | shortlog | log | commit | commitdiff | tree
history | raw | HEAD
Merge pull request #3250 from YosysHQ/micko/verific_consistent
[yosys.git] / backends / aiger / aiger.cc
1 /*
2 * yosys -- Yosys Open SYnthesis Suite
3 *
4 * Copyright (C) 2012 Claire Xenia Wolf <claire@yosyshq.com>
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/yosys.h"
21 #include "kernel/sigtools.h"
22
23 USING_YOSYS_NAMESPACE
24 PRIVATE_NAMESPACE_BEGIN
25
26 void aiger_encode(std::ostream &f, int x)
27 {
28 log_assert(x >= 0);
29
30 while (x & ~0x7f) {
31 f.put((x & 0x7f) | 0x80);
32 x = x >> 7;
33 }
34
35 f.put(x);
36 }
37
38 struct AigerWriter
39 {
40 Module *module;
41 bool zinit_mode;
42 SigMap sigmap;
43
44 dict<SigBit, bool> init_map;
45 pool<SigBit> input_bits, output_bits;
46 dict<SigBit, SigBit> not_map, ff_map, alias_map;
47 dict<SigBit, pair<SigBit, SigBit>> and_map;
48 vector<pair<SigBit, SigBit>> asserts, assumes;
49 vector<pair<SigBit, SigBit>> liveness, fairness;
50 pool<SigBit> initstate_bits;
51
52 vector<pair<int, int>> aig_gates;
53 vector<int> aig_latchin, aig_latchinit, aig_outputs;
54 int aig_m = 0, aig_i = 0, aig_l = 0, aig_o = 0, aig_a = 0;
55 int aig_b = 0, aig_c = 0, aig_j = 0, aig_f = 0;
56
57 dict<SigBit, int> aig_map;
58 dict<SigBit, int> ordered_outputs;
59 dict<SigBit, int> ordered_latches;
60
61 dict<SigBit, int> init_inputs;
62 int initstate_ff = 0;
63
64 int mkgate(int a0, int a1)
65 {
66 aig_m++, aig_a++;
67 aig_gates.push_back(a0 > a1 ? make_pair(a0, a1) : make_pair(a1, a0));
68 return 2*aig_m;
69 }
70
71 int bit2aig(SigBit bit)
72 {
73 auto it = aig_map.find(bit);
74 if (it != aig_map.end()) {
75 log_assert(it->second >= 0);
76 return it->second;
77 }
78
79 // NB: Cannot use iterator returned from aig_map.insert()
80 // since this function is called recursively
81
82 int a = -1;
83 if (not_map.count(bit)) {
84 a = bit2aig(not_map.at(bit)) ^ 1;
85 } else
86 if (and_map.count(bit)) {
87 auto args = and_map.at(bit);
88 int a0 = bit2aig(args.first);
89 int a1 = bit2aig(args.second);
90 a = mkgate(a0, a1);
91 } else
92 if (alias_map.count(bit)) {
93 a = bit2aig(alias_map.at(bit));
94 } else
95 if (initstate_bits.count(bit)) {
96 a = initstate_ff;
97 }
98
99 if (bit == State::Sx || bit == State::Sz)
100 log_error("Design contains 'x' or 'z' bits. Use 'setundef' to replace those constants.\n");
101
102 log_assert(a >= 0);
103 aig_map[bit] = a;
104 return a;
105 }
106
107 AigerWriter(Module *module, bool zinit_mode, bool imode, bool omode, bool bmode, bool lmode) : module(module), zinit_mode(zinit_mode), sigmap(module)
108 {
109 pool<SigBit> undriven_bits;
110 pool<SigBit> unused_bits;
111
112 // promote public wires
113 for (auto wire : module->wires())
114 if (wire->name.isPublic())
115 sigmap.add(wire);
116
117 // promote input wires
118 for (auto wire : module->wires())
119 if (wire->port_input)
120 sigmap.add(wire);
121
122 // promote output wires
123 for (auto wire : module->wires())
124 if (wire->port_output)
125 sigmap.add(wire);
126
127 for (auto wire : module->wires())
128 {
129 if (wire->attributes.count(ID::init)) {
130 SigSpec initsig = sigmap(wire);
131 Const initval = wire->attributes.at(ID::init);
132 for (int i = 0; i < GetSize(wire) && i < GetSize(initval); i++)
133 if (initval[i] == State::S0 || initval[i] == State::S1)
134 init_map[initsig[i]] = initval[i] == State::S1;
135 }
136
137 for (int i = 0; i < GetSize(wire); i++)
138 {
139 SigBit wirebit(wire, i);
140 SigBit bit = sigmap(wirebit);
141
142 if (bit.wire == nullptr) {
143 if (wire->port_output) {
144 aig_map[wirebit] = (bit == State::S1) ? 1 : 0;
145 output_bits.insert(wirebit);
146 }
147 continue;
148 }
149
150 undriven_bits.insert(bit);
151 unused_bits.insert(bit);
152
153 if (wire->port_input)
154 input_bits.insert(bit);
155
156 if (wire->port_output) {
157 if (bit != wirebit)
158 alias_map[wirebit] = bit;
159 output_bits.insert(wirebit);
160 }
161 }
162 }
163
164 for (auto bit : input_bits)
165 undriven_bits.erase(bit);
166
167 for (auto bit : output_bits)
168 unused_bits.erase(bit);
169
170 for (auto cell : module->cells())
171 {
172 if (cell->type == ID($_NOT_))
173 {
174 SigBit A = sigmap(cell->getPort(ID::A).as_bit());
175 SigBit Y = sigmap(cell->getPort(ID::Y).as_bit());
176 unused_bits.erase(A);
177 undriven_bits.erase(Y);
178 not_map[Y] = A;
179 continue;
180 }
181
182 if (cell->type.in(ID($_FF_), ID($_DFF_N_), ID($_DFF_P_)))
183 {
184 SigBit D = sigmap(cell->getPort(ID::D).as_bit());
185 SigBit Q = sigmap(cell->getPort(ID::Q).as_bit());
186 unused_bits.erase(D);
187 undriven_bits.erase(Q);
188 ff_map[Q] = D;
189 continue;
190 }
191
192 if (cell->type == ID($_AND_))
193 {
194 SigBit A = sigmap(cell->getPort(ID::A).as_bit());
195 SigBit B = sigmap(cell->getPort(ID::B).as_bit());
196 SigBit Y = sigmap(cell->getPort(ID::Y).as_bit());
197 unused_bits.erase(A);
198 unused_bits.erase(B);
199 undriven_bits.erase(Y);
200 and_map[Y] = make_pair(A, B);
201 continue;
202 }
203
204 if (cell->type == ID($initstate))
205 {
206 SigBit Y = sigmap(cell->getPort(ID::Y).as_bit());
207 undriven_bits.erase(Y);
208 initstate_bits.insert(Y);
209 continue;
210 }
211
212 if (cell->type == ID($assert))
213 {
214 SigBit A = sigmap(cell->getPort(ID::A).as_bit());
215 SigBit EN = sigmap(cell->getPort(ID::EN).as_bit());
216 unused_bits.erase(A);
217 unused_bits.erase(EN);
218 asserts.push_back(make_pair(A, EN));
219 continue;
220 }
221
222 if (cell->type == ID($assume))
223 {
224 SigBit A = sigmap(cell->getPort(ID::A).as_bit());
225 SigBit EN = sigmap(cell->getPort(ID::EN).as_bit());
226 unused_bits.erase(A);
227 unused_bits.erase(EN);
228 assumes.push_back(make_pair(A, EN));
229 continue;
230 }
231
232 if (cell->type == ID($live))
233 {
234 SigBit A = sigmap(cell->getPort(ID::A).as_bit());
235 SigBit EN = sigmap(cell->getPort(ID::EN).as_bit());
236 unused_bits.erase(A);
237 unused_bits.erase(EN);
238 liveness.push_back(make_pair(A, EN));
239 continue;
240 }
241
242 if (cell->type == ID($fair))
243 {
244 SigBit A = sigmap(cell->getPort(ID::A).as_bit());
245 SigBit EN = sigmap(cell->getPort(ID::EN).as_bit());
246 unused_bits.erase(A);
247 unused_bits.erase(EN);
248 fairness.push_back(make_pair(A, EN));
249 continue;
250 }
251
252 if (cell->type == ID($anyconst))
253 {
254 for (auto bit : sigmap(cell->getPort(ID::Y))) {
255 undriven_bits.erase(bit);
256 ff_map[bit] = bit;
257 }
258 continue;
259 }
260
261 if (cell->type == ID($anyseq))
262 {
263 for (auto bit : sigmap(cell->getPort(ID::Y))) {
264 undriven_bits.erase(bit);
265 input_bits.insert(bit);
266 }
267 continue;
268 }
269
270 log_error("Unsupported cell type: %s (%s)\n", log_id(cell->type), log_id(cell));
271 }
272
273 for (auto bit : unused_bits)
274 undriven_bits.erase(bit);
275
276 if (!undriven_bits.empty()) {
277 undriven_bits.sort();
278 for (auto bit : undriven_bits) {
279 log_warning("Treating undriven bit %s.%s like $anyseq.\n", log_id(module), log_signal(bit));
280 input_bits.insert(bit);
281 }
282 log_warning("Treating a total of %d undriven bits in %s like $anyseq.\n", GetSize(undriven_bits), log_id(module));
283 }
284
285 init_map.sort();
286 input_bits.sort();
287 output_bits.sort();
288 not_map.sort();
289 ff_map.sort();
290 and_map.sort();
291
292 aig_map[State::S0] = 0;
293 aig_map[State::S1] = 1;
294
295 for (auto bit : input_bits) {
296 aig_m++, aig_i++;
297 aig_map[bit] = 2*aig_m;
298 }
299
300 if (imode && input_bits.empty()) {
301 aig_m++, aig_i++;
302 }
303
304 if (zinit_mode)
305 {
306 for (auto it : ff_map) {
307 if (init_map.count(it.first))
308 continue;
309 aig_m++, aig_i++;
310 init_inputs[it.first] = 2*aig_m;
311 }
312 }
313
314 int fair_live_inputs_cnt = GetSize(liveness);
315 int fair_live_inputs_m = aig_m;
316
317 aig_m += fair_live_inputs_cnt;
318 aig_i += fair_live_inputs_cnt;
319
320 for (auto it : ff_map) {
321 aig_m++, aig_l++;
322 aig_map[it.first] = 2*aig_m;
323 ordered_latches[it.first] = aig_l-1;
324 if (init_map.count(it.first) == 0)
325 aig_latchinit.push_back(2);
326 else
327 aig_latchinit.push_back(init_map.at(it.first) ? 1 : 0);
328 }
329
330 if (!initstate_bits.empty() || !init_inputs.empty()) {
331 aig_m++, aig_l++;
332 initstate_ff = 2*aig_m+1;
333 aig_latchinit.push_back(0);
334 }
335
336 int fair_live_latches_cnt = GetSize(fairness) + 2*GetSize(liveness);
337 int fair_live_latches_m = aig_m;
338 int fair_live_latches_l = aig_l;
339
340 aig_m += fair_live_latches_cnt;
341 aig_l += fair_live_latches_cnt;
342
343 for (int i = 0; i < fair_live_latches_cnt; i++)
344 aig_latchinit.push_back(0);
345
346 if (zinit_mode)
347 {
348 for (auto it : ff_map)
349 {
350 int l = ordered_latches[it.first];
351
352 if (aig_latchinit.at(l) == 1)
353 aig_map[it.first] ^= 1;
354
355 if (aig_latchinit.at(l) == 2)
356 {
357 int gated_ffout = mkgate(aig_map[it.first], initstate_ff^1);
358 int gated_initin = mkgate(init_inputs[it.first], initstate_ff);
359 aig_map[it.first] = mkgate(gated_ffout^1, gated_initin^1)^1;
360 }
361 }
362 }
363
364 for (auto it : ff_map) {
365 int a = bit2aig(it.second);
366 int l = ordered_latches[it.first];
367 if (zinit_mode && aig_latchinit.at(l) == 1)
368 aig_latchin.push_back(a ^ 1);
369 else
370 aig_latchin.push_back(a);
371 }
372
373 if (lmode && aig_l == 0) {
374 aig_m++, aig_l++;
375 aig_latchinit.push_back(0);
376 aig_latchin.push_back(0);
377 }
378
379 if (!initstate_bits.empty() || !init_inputs.empty())
380 aig_latchin.push_back(1);
381
382 for (auto bit : output_bits) {
383 aig_o++;
384 ordered_outputs[bit] = aig_o-1;
385 aig_outputs.push_back(bit2aig(bit));
386 }
387
388 if (omode && output_bits.empty()) {
389 aig_o++;
390 aig_outputs.push_back(0);
391 }
392
393 for (auto it : asserts) {
394 aig_b++;
395 int bit_a = bit2aig(it.first);
396 int bit_en = bit2aig(it.second);
397 aig_outputs.push_back(mkgate(bit_a^1, bit_en));
398 }
399
400 if (bmode && asserts.empty()) {
401 aig_b++;
402 aig_outputs.push_back(0);
403 }
404
405 for (auto it : assumes) {
406 aig_c++;
407 int bit_a = bit2aig(it.first);
408 int bit_en = bit2aig(it.second);
409 aig_outputs.push_back(mkgate(bit_a^1, bit_en)^1);
410 }
411
412 for (auto it : liveness)
413 {
414 int input_m = ++fair_live_inputs_m;
415 int latch_m1 = ++fair_live_latches_m;
416 int latch_m2 = ++fair_live_latches_m;
417
418 log_assert(GetSize(aig_latchin) == fair_live_latches_l);
419 fair_live_latches_l += 2;
420
421 int bit_a = bit2aig(it.first);
422 int bit_en = bit2aig(it.second);
423 int bit_s = 2*input_m;
424 int bit_q1 = 2*latch_m1;
425 int bit_q2 = 2*latch_m2;
426
427 int bit_d1 = mkgate(mkgate(bit_s, bit_en)^1, bit_q1^1)^1;
428 int bit_d2 = mkgate(mkgate(bit_d1, bit_a)^1, bit_q2^1)^1;
429
430 aig_j++;
431 aig_latchin.push_back(bit_d1);
432 aig_latchin.push_back(bit_d2);
433 aig_outputs.push_back(mkgate(bit_q1, bit_q2^1));
434 }
435
436 for (auto it : fairness)
437 {
438 int latch_m = ++fair_live_latches_m;
439
440 log_assert(GetSize(aig_latchin) == fair_live_latches_l);
441 fair_live_latches_l += 1;
442
443 int bit_a = bit2aig(it.first);
444 int bit_en = bit2aig(it.second);
445 int bit_q = 2*latch_m;
446
447 aig_f++;
448 aig_latchin.push_back(mkgate(mkgate(bit_q^1, bit_en^1)^1, bit_a^1));
449 aig_outputs.push_back(bit_q^1);
450 }
451 }
452
453 void write_aiger(std::ostream &f, bool ascii_mode, bool miter_mode, bool symbols_mode)
454 {
455 int aig_obc = aig_o + aig_b + aig_c;
456 int aig_obcj = aig_obc + aig_j;
457 int aig_obcjf = aig_obcj + aig_f;
458
459 log_assert(aig_m == aig_i + aig_l + aig_a);
460 log_assert(aig_l == GetSize(aig_latchin));
461 log_assert(aig_l == GetSize(aig_latchinit));
462 log_assert(aig_obcjf == GetSize(aig_outputs));
463
464 if (miter_mode) {
465 if (aig_b || aig_c || aig_j || aig_f)
466 log_error("Running AIGER back-end in -miter mode, but design contains $assert, $assume, $live and/or $fair cells!\n");
467 f << stringf("%s %d %d %d 0 %d %d\n", ascii_mode ? "aag" : "aig", aig_m, aig_i, aig_l, aig_a, aig_o);
468 } else {
469 f << stringf("%s %d %d %d %d %d", ascii_mode ? "aag" : "aig", aig_m, aig_i, aig_l, aig_o, aig_a);
470 if (aig_b || aig_c || aig_j || aig_f)
471 f << stringf(" %d %d %d %d", aig_b, aig_c, aig_j, aig_f);
472 f << stringf("\n");
473 }
474
475 if (ascii_mode)
476 {
477 for (int i = 0; i < aig_i; i++)
478 f << stringf("%d\n", 2*i+2);
479
480 for (int i = 0; i < aig_l; i++) {
481 if (zinit_mode || aig_latchinit.at(i) == 0)
482 f << stringf("%d %d\n", 2*(aig_i+i)+2, aig_latchin.at(i));
483 else if (aig_latchinit.at(i) == 1)
484 f << stringf("%d %d 1\n", 2*(aig_i+i)+2, aig_latchin.at(i));
485 else if (aig_latchinit.at(i) == 2)
486 f << stringf("%d %d %d\n", 2*(aig_i+i)+2, aig_latchin.at(i), 2*(aig_i+i)+2);
487 }
488
489 for (int i = 0; i < aig_obc; i++)
490 f << stringf("%d\n", aig_outputs.at(i));
491
492 for (int i = aig_obc; i < aig_obcj; i++)
493 f << stringf("1\n");
494
495 for (int i = aig_obc; i < aig_obcj; i++)
496 f << stringf("%d\n", aig_outputs.at(i));
497
498 for (int i = aig_obcj; i < aig_obcjf; i++)
499 f << stringf("%d\n", aig_outputs.at(i));
500
501 for (int i = 0; i < aig_a; i++)
502 f << stringf("%d %d %d\n", 2*(aig_i+aig_l+i)+2, aig_gates.at(i).first, aig_gates.at(i).second);
503 }
504 else
505 {
506 for (int i = 0; i < aig_l; i++) {
507 if (zinit_mode || aig_latchinit.at(i) == 0)
508 f << stringf("%d\n", aig_latchin.at(i));
509 else if (aig_latchinit.at(i) == 1)
510 f << stringf("%d 1\n", aig_latchin.at(i));
511 else if (aig_latchinit.at(i) == 2)
512 f << stringf("%d %d\n", aig_latchin.at(i), 2*(aig_i+i)+2);
513 }
514
515 for (int i = 0; i < aig_obc; i++)
516 f << stringf("%d\n", aig_outputs.at(i));
517
518 for (int i = aig_obc; i < aig_obcj; i++)
519 f << stringf("1\n");
520
521 for (int i = aig_obc; i < aig_obcj; i++)
522 f << stringf("%d\n", aig_outputs.at(i));
523
524 for (int i = aig_obcj; i < aig_obcjf; i++)
525 f << stringf("%d\n", aig_outputs.at(i));
526
527 for (int i = 0; i < aig_a; i++) {
528 int lhs = 2*(aig_i+aig_l+i)+2;
529 int rhs0 = aig_gates.at(i).first;
530 int rhs1 = aig_gates.at(i).second;
531 int delta0 = lhs - rhs0;
532 int delta1 = rhs0 - rhs1;
533 aiger_encode(f, delta0);
534 aiger_encode(f, delta1);
535 }
536 }
537
538 if (symbols_mode)
539 {
540 dict<string, vector<string>> symbols;
541
542 for (auto wire : module->wires())
543 {
544 if (wire->name[0] == '$')
545 continue;
546
547 SigSpec sig = sigmap(wire);
548
549 for (int i = 0; i < GetSize(wire); i++)
550 {
551 if (sig[i].wire == nullptr) {
552 if (wire->port_output)
553 sig[i] = SigBit(wire, i);
554 else
555 continue;
556 }
557
558 if (wire->port_input) {
559 int a = aig_map.at(sig[i]);
560 log_assert((a & 1) == 0);
561 if (GetSize(wire) != 1)
562 symbols[stringf("i%d", (a >> 1)-1)].push_back(stringf("%s[%d]", log_id(wire), i));
563 else
564 symbols[stringf("i%d", (a >> 1)-1)].push_back(stringf("%s", log_id(wire)));
565 }
566
567 if (wire->port_output) {
568 int o = ordered_outputs.at(SigSpec(wire, i));
569 if (GetSize(wire) != 1)
570 symbols[stringf("%c%d", miter_mode ? 'b' : 'o', o)].push_back(stringf("%s[%d]", log_id(wire), i));
571 else
572 symbols[stringf("%c%d", miter_mode ? 'b' : 'o', o)].push_back(stringf("%s", log_id(wire)));
573 }
574
575 if (init_inputs.count(sig[i])) {
576 int a = init_inputs.at(sig[i]);
577 log_assert((a & 1) == 0);
578 if (GetSize(wire) != 1)
579 symbols[stringf("i%d", (a >> 1)-1)].push_back(stringf("init:%s[%d]", log_id(wire), i));
580 else
581 symbols[stringf("i%d", (a >> 1)-1)].push_back(stringf("init:%s", log_id(wire)));
582 }
583
584 if (ordered_latches.count(sig[i])) {
585 int l = ordered_latches.at(sig[i]);
586 const char *p = (zinit_mode && (aig_latchinit.at(l) == 1)) ? "!" : "";
587 if (GetSize(wire) != 1)
588 symbols[stringf("l%d", l)].push_back(stringf("%s%s[%d]", p, log_id(wire), i));
589 else
590 symbols[stringf("l%d", l)].push_back(stringf("%s%s", p, log_id(wire)));
591 }
592 }
593 }
594
595 symbols.sort();
596
597 for (auto &sym : symbols) {
598 f << sym.first;
599 std::sort(sym.second.begin(), sym.second.end());
600 for (auto &s : sym.second)
601 f << " " << s;
602 f << std::endl;
603 }
604 }
605
606 f << stringf("c\nGenerated by %s\n", yosys_version_str);
607 }
608
609 void write_map(std::ostream &f, bool verbose_map, bool no_startoffset)
610 {
611 dict<int, string> input_lines;
612 dict<int, string> init_lines;
613 dict<int, string> output_lines;
614 dict<int, string> latch_lines;
615 dict<int, string> wire_lines;
616
617 for (auto wire : module->wires())
618 {
619 if (!verbose_map && wire->name[0] == '$')
620 continue;
621
622 SigSpec sig = sigmap(wire);
623
624 for (int i = 0; i < GetSize(wire); i++)
625 {
626 if (aig_map.count(sig[i]) == 0 || sig[i].wire == nullptr)
627 continue;
628
629 int a = aig_map.at(sig[i]);
630 int index = no_startoffset ? i : (wire->start_offset+i);
631
632 if (verbose_map)
633 wire_lines[a] += stringf("wire %d %d %s\n", a, index, log_id(wire));
634
635 if (wire->port_input) {
636 log_assert((a & 1) == 0);
637 input_lines[a] += stringf("input %d %d %s\n", (a >> 1)-1, index, log_id(wire));
638 }
639
640 if (wire->port_output) {
641 int o = ordered_outputs.at(sig[i]);
642 output_lines[o] += stringf("output %d %d %s\n", o, index, log_id(wire));
643 }
644
645 if (init_inputs.count(sig[i])) {
646 int a = init_inputs.at(sig[i]);
647 log_assert((a & 1) == 0);
648 init_lines[a] += stringf("init %d %d %s\n", (a >> 1)-1, index, log_id(wire));
649 }
650
651 if (ordered_latches.count(sig[i])) {
652 int l = ordered_latches.at(sig[i]);
653 if (zinit_mode && (aig_latchinit.at(l) == 1))
654 latch_lines[l] += stringf("invlatch %d %d %s\n", l, index, log_id(wire));
655 else
656 latch_lines[l] += stringf("latch %d %d %s\n", l, index, log_id(wire));
657 }
658 }
659 }
660
661 input_lines.sort();
662 for (auto &it : input_lines)
663 f << it.second;
664
665 init_lines.sort();
666 for (auto &it : init_lines)
667 f << it.second;
668
669 output_lines.sort();
670 for (auto &it : output_lines)
671 f << it.second;
672
673 latch_lines.sort();
674 for (auto &it : latch_lines)
675 f << it.second;
676
677 wire_lines.sort();
678 for (auto &it : wire_lines)
679 f << it.second;
680 }
681 };
682
683 struct AigerBackend : public Backend {
684 AigerBackend() : Backend("aiger", "write design to AIGER file") { }
685 void help() override
686 {
687 // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
688 log("\n");
689 log(" write_aiger [options] [filename]\n");
690 log("\n");
691 log("Write the current design to an AIGER file. The design must be flattened and\n");
692 log("must not contain any cell types except $_AND_, $_NOT_, simple FF types,\n");
693 log("$assert and $assume cells, and $initstate cells.\n");
694 log("\n");
695 log("$assert and $assume cells are converted to AIGER bad state properties and\n");
696 log("invariant constraints.\n");
697 log("\n");
698 log(" -ascii\n");
699 log(" write ASCII version of AIGER format\n");
700 log("\n");
701 log(" -zinit\n");
702 log(" convert FFs to zero-initialized FFs, adding additional inputs for\n");
703 log(" uninitialized FFs.\n");
704 log("\n");
705 log(" -miter\n");
706 log(" design outputs are AIGER bad state properties\n");
707 log("\n");
708 log(" -symbols\n");
709 log(" include a symbol table in the generated AIGER file\n");
710 log("\n");
711 log(" -map <filename>\n");
712 log(" write an extra file with port and latch symbols\n");
713 log("\n");
714 log(" -vmap <filename>\n");
715 log(" like -map, but more verbose\n");
716 log("\n");
717 log(" -no-startoffset\n");
718 log(" make indexes zero based, enable using map files with smt solvers.\n");
719 log("\n");
720 log(" -I, -O, -B, -L\n");
721 log(" If the design contains no input/output/assert/flip-flop then create one\n");
722 log(" dummy input/output/bad_state-pin or latch to make the tools reading the\n");
723 log(" AIGER file happy.\n");
724 log("\n");
725 }
726 void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) override
727 {
728 bool ascii_mode = false;
729 bool zinit_mode = false;
730 bool miter_mode = false;
731 bool symbols_mode = false;
732 bool verbose_map = false;
733 bool imode = false;
734 bool omode = false;
735 bool bmode = false;
736 bool lmode = false;
737 bool no_startoffset = false;
738 std::string map_filename;
739
740 log_header(design, "Executing AIGER backend.\n");
741
742 size_t argidx;
743 for (argidx = 1; argidx < args.size(); argidx++)
744 {
745 if (args[argidx] == "-ascii") {
746 ascii_mode = true;
747 continue;
748 }
749 if (args[argidx] == "-zinit") {
750 zinit_mode = true;
751 continue;
752 }
753 if (args[argidx] == "-miter") {
754 miter_mode = true;
755 continue;
756 }
757 if (args[argidx] == "-symbols") {
758 symbols_mode = true;
759 continue;
760 }
761 if (map_filename.empty() && args[argidx] == "-map" && argidx+1 < args.size()) {
762 map_filename = args[++argidx];
763 continue;
764 }
765 if (map_filename.empty() && args[argidx] == "-vmap" && argidx+1 < args.size()) {
766 map_filename = args[++argidx];
767 verbose_map = true;
768 continue;
769 }
770 if (args[argidx] == "-no-startoffset") {
771 no_startoffset = true;
772 continue;
773 }
774 if (args[argidx] == "-I") {
775 imode = true;
776 continue;
777 }
778 if (args[argidx] == "-O") {
779 omode = true;
780 continue;
781 }
782 if (args[argidx] == "-B") {
783 bmode = true;
784 continue;
785 }
786 if (args[argidx] == "-L") {
787 lmode = true;
788 continue;
789 }
790 break;
791 }
792 extra_args(f, filename, args, argidx, !ascii_mode);
793
794 Module *top_module = design->top_module();
795
796 if (top_module == nullptr)
797 log_error("Can't find top module in current design!\n");
798
799 if (!design->selected_whole_module(top_module))
800 log_cmd_error("Can't handle partially selected module %s!\n", log_id(top_module));
801
802 if (!top_module->processes.empty())
803 log_error("Found unmapped processes in module %s: unmapped processes are not supported in AIGER backend!\n", log_id(top_module));
804 if (!top_module->memories.empty())
805 log_error("Found unmapped memories in module %s: unmapped memories are not supported in AIGER backend!\n", log_id(top_module));
806
807 AigerWriter writer(top_module, zinit_mode, imode, omode, bmode, lmode);
808 writer.write_aiger(*f, ascii_mode, miter_mode, symbols_mode);
809
810 if (!map_filename.empty()) {
811 rewrite_filename(filename);
812 std::ofstream mapf;
813 mapf.open(map_filename.c_str(), std::ofstream::trunc);
814 if (mapf.fail())
815 log_error("Can't open file `%s' for writing: %s\n", map_filename.c_str(), strerror(errno));
816 writer.write_map(mapf, verbose_map, no_startoffset);
817 }
818 }
819 } AigerBackend;
820
821 PRIVATE_NAMESPACE_END