2 * yosys -- Yosys Open SYnthesis Suite
4 * Copyright (C) 2012 Clifford Wolf <clifford@clifford.at>
5 * 2019 Eddie Hung <eddie@fpgeh.com>
7 * Permission to use, copy, modify, and/or distribute this software for any
8 * purpose with or without fee is hereby granted, provided that the above
9 * copyright notice and this permission notice appear in all copies.
11 * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
12 * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
13 * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
14 * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
15 * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
16 * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
17 * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
21 // [[CITE]] The AIGER And-Inverter Graph (AIG) Format Version 20071012
22 // Armin Biere. The AIGER And-Inverter Graph (AIG) Format Version 20071012. Technical Report 07/1, October 2011, FMV Reports Series, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria.
23 // http://fmv.jku.at/papers/Biere-FMV-TR-07-1.pdf
31 #include "kernel/yosys.h"
32 #include "kernel/sigtools.h"
33 #include "kernel/consteval.h"
34 #include "aigerparse.h"
40 RTLIL::Module
*module
;
41 dict
<RTLIL::SigBit
, RTLIL::Const
> values_map
;
42 SigSet
<RTLIL::Cell
*> sig2driver
;
43 dict
<SigBit
, pool
<RTLIL::SigBit
>> sig2deps
;
45 ConstEvalAig(RTLIL::Module
*module
) : module(module
)
51 for (auto &it
: module
->cells_
) {
52 if (!ct
.cell_known(it
.second
->type
))
54 for (auto &it2
: it
.second
->connections())
55 if (ct
.cell_output(it
.second
->type
, it2
.first
))
56 sig2driver
.insert(it2
.second
, it
.second
);
66 void set(RTLIL::SigSpec sig
, RTLIL::Const value
)
69 auto it
= values_map
.find(sig
);
70 RTLIL::SigSpec current_val
;
71 if (it
!= values_map
.end())
72 current_val
= it
->second
;
73 for (int i
= 0; i
< GetSize(current_val
); i
++)
74 log_assert(current_val
[i
].wire
!= NULL
|| current_val
[i
] == value
.bits
[i
]);
76 for (int i
= 0; i
< GetSize(sig
); i
++)
77 values_map
[sig
[i
]] = value
[i
];
80 void set_incremental(RTLIL::SigSpec sig
, RTLIL::Const value
)
82 log_assert(GetSize(sig
) == GetSize(value
));
84 for (int i
= 0; i
< GetSize(sig
); i
++) {
85 auto it
= values_map
.find(sig
[i
]);
86 if (it
!= values_map
.end()) {
87 RTLIL::SigSpec current_val
= it
->second
;
88 if (current_val
!= value
[i
])
89 for (auto dep
: sig2deps
[sig
[i
]])
90 values_map
.erase(dep
);
91 it
->second
= value
[i
];
94 values_map
[sig
[i
]] = value
[i
];
98 void compute_deps(RTLIL::SigBit output
, const pool
<RTLIL::SigBit
> &inputs
)
100 sig2deps
[output
].insert(output
);
102 std::set
<RTLIL::Cell
*> driver_cells
;
103 sig2driver
.find(output
, driver_cells
);
104 for (auto cell
: driver_cells
) {
105 RTLIL::SigBit sig_a
= cell
->getPort("\\A");
106 sig2deps
[sig_a
].insert(sig2deps
[output
].begin(), sig2deps
[output
].end());
107 if (!inputs
.count(sig_a
))
108 compute_deps(sig_a
, inputs
);
110 if (cell
->type
== "$_AND_") {
111 RTLIL::SigSpec sig_b
= cell
->getPort("\\B");
112 sig2deps
[sig_b
].insert(sig2deps
[output
].begin(), sig2deps
[output
].end());
113 if (!inputs
.count(sig_b
))
114 compute_deps(sig_b
, inputs
);
116 else if (cell
->type
== "$_NOT_") {
122 bool eval(RTLIL::Cell
*cell
)
124 RTLIL::SigSpec sig_y
= cell
->getPort("\\Y");
125 auto it
= values_map
.find(sig_y
);
126 if (it
!= values_map
.end())
128 if (sig_y
.is_fully_const())
131 RTLIL::SigSpec sig_a
= cell
->getPort("\\A");
132 if (sig_a
.size() > 0 && !eval(sig_a
))
135 RTLIL::Const eval_ret
;
136 if (cell
->type
== "$_NOT_") {
137 if (sig_a
== RTLIL::S0
) eval_ret
= RTLIL::S1
;
138 else if (sig_a
== RTLIL::S1
) eval_ret
= RTLIL::S0
;
140 else if (cell
->type
== "$_AND_") {
141 if (sig_a
== RTLIL::S0
) {
142 eval_ret
= RTLIL::S0
;
147 RTLIL::SigSpec sig_b
= cell
->getPort("\\B");
148 if (sig_b
.size() > 0 && !eval(sig_b
))
150 if (sig_b
== RTLIL::S0
) {
151 eval_ret
= RTLIL::S0
;
155 if (sig_a
!= RTLIL::State::S1
|| sig_b
!= RTLIL::State::S1
) {
156 eval_ret
= RTLIL::State::Sx
;
160 eval_ret
= RTLIL::State::S1
;
166 set(sig_y
, eval_ret
);
170 bool eval(RTLIL::SigSpec
&sig
)
172 auto it
= values_map
.find(sig
);
173 if (it
!= values_map
.end())
175 if (sig
.is_fully_const())
178 std::set
<RTLIL::Cell
*> driver_cells
;
179 sig2driver
.find(sig
, driver_cells
);
180 for (auto cell
: driver_cells
)
184 it
= values_map
.find(sig
);
185 if (it
!= values_map
.end())
187 if (sig
.is_fully_const())
194 AigerReader::AigerReader(RTLIL::Design
*design
, std::istream
&f
, RTLIL::IdString module_name
, RTLIL::IdString clk_name
, std::string map_filename
, bool wideports
)
195 : design(design
), f(f
), clk_name(clk_name
), map_filename(map_filename
), wideports(wideports
)
197 module
= new RTLIL::Module
;
198 module
->name
= module_name
;
199 if (design
->module(module
->name
))
200 log_error("Duplicate definition of module %s!\n", log_id(module
->name
));
203 void AigerReader::parse_aiger()
207 if (header
!= "aag" && header
!= "aig")
208 log_error("Unsupported AIGER file!\n");
210 // Parse rest of header
211 if (!(f
>> M
>> I
>> L
>> O
>> A
))
212 log_error("Invalid AIGER header\n");
216 if (f
.peek() != ' ') goto end_of_header
;
217 if (!(f
>> B
)) log_error("Invalid AIGER header\n");
218 if (f
.peek() != ' ') goto end_of_header
;
219 if (!(f
>> C
)) log_error("Invalid AIGER header\n");
220 if (f
.peek() != ' ') goto end_of_header
;
221 if (!(f
>> J
)) log_error("Invalid AIGER header\n");
222 if (f
.peek() != ' ') goto end_of_header
;
223 if (!(f
>> F
)) log_error("Invalid AIGER header\n");
227 std::getline(f
, line
); // Ignore up to start of next line, as standard
228 // says anything that follows could be used for
231 log_debug("M=%u I=%u L=%u O=%u A=%u B=%u C=%u J=%u F=%u\n", M
, I
, L
, O
, A
, B
, C
, J
, F
);
239 else if (header
== "aig")
240 parse_aiger_binary();
244 RTLIL::Wire
* n0
= module
->wire("\\__0__");
246 module
->connect(n0
, RTLIL::S0
);
248 // Parse footer (symbol table, comments, etc.)
251 for (int c
= f
.peek(); c
!= EOF
; c
= f
.peek(), ++line_count
) {
252 if (c
== 'i' || c
== 'l' || c
== 'o' || c
== 'b') {
255 log_error("Line %u cannot be interpreted as a symbol entry!\n", line_count
);
257 if ((c
== 'i' && l1
> inputs
.size()) || (c
== 'l' && l1
> latches
.size()) || (c
== 'o' && l1
> outputs
.size()))
258 log_error("Line %u has invalid symbol position!\n", line_count
);
261 if (c
== 'i') wire
= inputs
[l1
];
262 else if (c
== 'l') wire
= latches
[l1
];
263 else if (c
== 'o') wire
= outputs
[l1
];
264 else if (c
== 'b') wire
= bad_properties
[l1
];
267 module
->rename(wire
, stringf("\\%s", s
.c_str()));
269 else if (c
== 'j' || c
== 'f') {
274 if (f
.peek() == '\n')
276 // Else constraint (TODO)
279 log_error("Line %u: cannot interpret first character '%c'!\n", line_count
, c
);
280 std::getline(f
, line
); // Ignore up to start of next line
286 static uint32_t parse_xaiger_literal(std::istream
&f
)
289 f
.read(reinterpret_cast<char*>(&l
), sizeof(l
));
290 if (f
.gcount() != sizeof(l
))
291 log_error("Offset %ld: unable to read literal!\n", static_cast<int64_t>(f
.tellg()));
292 // TODO: Don't assume we're on little endian
294 return _byteswap_ulong(l
);
296 return __builtin_bswap32(l
);
300 static RTLIL::Wire
* createWireIfNotExists(RTLIL::Module
*module
, unsigned literal
)
302 const unsigned variable
= literal
>> 1;
303 const bool invert
= literal
& 1;
304 RTLIL::IdString
wire_name(stringf("\\__%d%s__", variable
, invert
? "b" : "")); // FIXME: is "b" the right suffix?
305 RTLIL::Wire
*wire
= module
->wire(wire_name
);
306 if (wire
) return wire
;
307 log_debug("Creating %s\n", wire_name
.c_str());
308 wire
= module
->addWire(wire_name
);
309 wire
->port_input
= wire
->port_output
= false;
310 if (!invert
) return wire
;
311 RTLIL::IdString
wire_inv_name(stringf("\\__%d__", variable
));
312 RTLIL::Wire
*wire_inv
= module
->wire(wire_inv_name
);
314 if (module
->cell(wire_inv_name
)) return wire
;
317 log_debug("Creating %s\n", wire_inv_name
.c_str());
318 wire_inv
= module
->addWire(wire_inv_name
);
319 wire_inv
->port_input
= wire_inv
->port_output
= false;
322 log_debug("Creating %s = ~%s\n", wire_name
.c_str(), wire_inv_name
.c_str());
323 module
->addNotGate(stringf("\\__%d__$not", variable
), wire_inv
, wire
); // FIXME: is "$not" the right suffix?
328 void AigerReader::parse_xaiger()
332 if (header
!= "aag" && header
!= "aig")
333 log_error("Unsupported AIGER file!\n");
335 // Parse rest of header
336 if (!(f
>> M
>> I
>> L
>> O
>> A
))
337 log_error("Invalid AIGER header\n");
343 std::getline(f
, line
); // Ignore up to start of next line, as standard
344 // says anything that follows could be used for
347 log_debug("M=%u I=%u L=%u O=%u A=%u\n", M
, I
, L
, O
, A
);
355 else if (header
== "aig")
356 parse_aiger_binary();
360 RTLIL::Wire
* n0
= module
->wire("\\__0__");
362 module
->connect(n0
, RTLIL::S0
);
364 dict
<int,IdString
> box_lookup
;
365 for (auto m
: design
->modules()) {
366 auto it
= m
->attributes
.find("\\abc_box_id");
367 if (it
== m
->attributes
.end())
369 if (m
->name
[0] == '$') continue;
370 auto r
= box_lookup
.insert(std::make_pair(it
->second
.as_int(), m
->name
));
371 log_assert(r
.second
);
374 // Parse footer (symbol table, comments, etc.)
376 bool comment_seen
= false;
377 for (int c
= f
.peek(); c
!= EOF
; c
= f
.peek()) {
378 if (comment_seen
|| c
== 'c') {
389 uint32_t dataSize
= parse_xaiger_literal(f
);
390 uint32_t lutNum
= parse_xaiger_literal(f
);
391 uint32_t lutSize
= parse_xaiger_literal(f
);
392 log_debug("m: dataSize=%u lutNum=%u lutSize=%u\n", dataSize
, lutNum
, lutSize
);
393 ConstEvalAig
ce(module
);
394 for (unsigned i
= 0; i
< lutNum
; ++i
) {
395 uint32_t rootNodeID
= parse_xaiger_literal(f
);
396 uint32_t cutLeavesM
= parse_xaiger_literal(f
);
397 log_debug("rootNodeID=%d cutLeavesM=%d\n", rootNodeID
, cutLeavesM
);
398 RTLIL::Wire
*output_sig
= module
->wire(stringf("\\__%d__", rootNodeID
));
400 RTLIL::SigSpec input_sig
;
401 for (unsigned j
= 0; j
< cutLeavesM
; ++j
) {
402 nodeID
= parse_xaiger_literal(f
);
403 log_debug("\t%u\n", nodeID
);
404 RTLIL::Wire
*wire
= module
->wire(stringf("\\__%d__", nodeID
));
406 input_sig
.append(wire
);
409 ce
.compute_deps(output_sig
, input_sig
.to_sigbit_pool());
410 RTLIL::Const
lut_mask(RTLIL::State::Sx
, 1 << input_sig
.size());
411 for (int j
= 0; j
< (1 << cutLeavesM
); ++j
) {
412 int gray
= j
^ (j
>> 1);
413 ce
.set_incremental(input_sig
, RTLIL::Const
{gray
, static_cast<int>(cutLeavesM
)});
414 RTLIL::SigSpec
o(output_sig
);
416 lut_mask
[gray
] = o
.as_const()[0];
418 RTLIL::Cell
*output_cell
= module
->cell(stringf("\\__%d__$and", rootNodeID
));
419 log_assert(output_cell
);
420 module
->remove(output_cell
);
421 module
->addLut(stringf("\\__%d__$lut", rootNodeID
), input_sig
, output_sig
, std::move(lut_mask
));
425 uint32_t dataSize
= parse_xaiger_literal(f
);
426 flopNum
= parse_xaiger_literal(f
);
427 log_assert(dataSize
== (flopNum
+1) * sizeof(uint32_t));
428 f
.ignore(flopNum
* sizeof(uint32_t));
431 parse_xaiger_literal(f
);
433 log_debug("n: '%s'\n", s
.c_str());
436 f
.ignore(sizeof(uint32_t));
437 uint32_t version
= parse_xaiger_literal(f
);
438 log_assert(version
== 1);
439 uint32_t ciNum
= parse_xaiger_literal(f
);
440 log_debug("ciNum = %u\n", ciNum
);
441 uint32_t coNum
= parse_xaiger_literal(f
);
442 log_debug("coNum = %u\n", coNum
);
443 piNum
= parse_xaiger_literal(f
);
444 log_debug("piNum = %u\n", piNum
);
445 uint32_t poNum
= parse_xaiger_literal(f
);
446 log_debug("poNum = %u\n", poNum
);
447 uint32_t boxNum
= parse_xaiger_literal(f
);
448 log_debug("boxNum = %u\n", poNum
);
449 for (unsigned i
= 0; i
< boxNum
; i
++) {
450 f
.ignore(2*sizeof(uint32_t));
451 uint32_t boxUniqueId
= parse_xaiger_literal(f
);
452 log_assert(boxUniqueId
> 0);
453 uint32_t oldBoxNum
= parse_xaiger_literal(f
);
454 RTLIL::Cell
* cell
= module
->addCell(stringf("$__box%u__", oldBoxNum
), box_lookup
.at(boxUniqueId
));
455 boxes
.emplace_back(cell
);
458 else if (c
== 'a' || c
== 'i' || c
== 'o') {
459 uint32_t dataSize
= parse_xaiger_literal(f
);
467 log_error("Line %u: cannot interpret first character '%c'!\n", line_count
, c
);
473 void AigerReader::parse_aiger_ascii()
476 std::stringstream ss
;
481 for (unsigned i
= 1; i
<= I
; ++i
, ++line_count
) {
483 log_error("Line %u cannot be interpreted as an input!\n", line_count
);
484 log_debug("%d is an input\n", l1
);
485 log_assert(!(l1
& 1)); // Inputs can't be inverted
486 RTLIL::Wire
*wire
= createWireIfNotExists(module
, l1
);
487 wire
->port_input
= true;
488 inputs
.push_back(wire
);
492 RTLIL::Wire
*clk_wire
= nullptr;
494 log_assert(clk_name
!= "");
495 clk_wire
= module
->wire(clk_name
);
496 log_assert(!clk_wire
);
497 log_debug("Creating %s\n", clk_name
.c_str());
498 clk_wire
= module
->addWire(clk_name
);
499 clk_wire
->port_input
= true;
500 clk_wire
->port_output
= false;
502 for (unsigned i
= 0; i
< L
; ++i
, ++line_count
) {
503 if (!(f
>> l1
>> l2
))
504 log_error("Line %u cannot be interpreted as a latch!\n", line_count
);
505 log_debug("%d %d is a latch\n", l1
, l2
);
506 log_assert(!(l1
& 1)); // TODO: Latch outputs can't be inverted?
507 RTLIL::Wire
*q_wire
= createWireIfNotExists(module
, l1
);
508 RTLIL::Wire
*d_wire
= createWireIfNotExists(module
, l2
);
510 module
->addDffGate(NEW_ID
, clk_wire
, d_wire
, q_wire
);
512 // Reset logic is optional in AIGER 1.9
513 if (f
.peek() == ' ') {
515 log_error("Line %u cannot be interpreted as a latch!\n", line_count
);
518 q_wire
->attributes
["\\init"] = RTLIL::S0
;
520 q_wire
->attributes
["\\init"] = RTLIL::S1
;
522 //q_wire->attributes["\\init"] = RTLIL::Sx;
525 log_error("Line %u has invalid reset literal for latch!\n", line_count
);
528 // AIGER latches are assumed to be initialized to zero
529 q_wire
->attributes
["\\init"] = RTLIL::S0
;
531 latches
.push_back(q_wire
);
535 for (unsigned i
= 0; i
< O
; ++i
, ++line_count
) {
537 log_error("Line %u cannot be interpreted as an output!\n", line_count
);
539 log_debug("%d is an output\n", l1
);
540 const unsigned variable
= l1
>> 1;
541 const bool invert
= l1
& 1;
542 RTLIL::IdString
wire_name(stringf("\\__%d%s__", variable
, invert
? "b" : "")); // FIXME: is "b" the right suffix?
543 RTLIL::Wire
*wire
= module
->wire(wire_name
);
545 wire
= createWireIfNotExists(module
, l1
);
546 else if (wire
->port_input
|| wire
->port_output
) {
547 RTLIL::Wire
*new_wire
= module
->addWire(NEW_ID
);
548 module
->connect(new_wire
, wire
);
551 wire
->port_output
= true;
552 outputs
.push_back(wire
);
555 // Parse bad properties
556 for (unsigned i
= 0; i
< B
; ++i
, ++line_count
) {
558 log_error("Line %u cannot be interpreted as a bad state property!\n", line_count
);
560 log_debug("%d is a bad state property\n", l1
);
561 RTLIL::Wire
*wire
= createWireIfNotExists(module
, l1
);
562 wire
->port_output
= true;
563 bad_properties
.push_back(wire
);
566 // TODO: Parse invariant constraints
567 for (unsigned i
= 0; i
< C
; ++i
, ++line_count
)
568 std::getline(f
, line
); // Ignore up to start of next line
570 // TODO: Parse justice properties
571 for (unsigned i
= 0; i
< J
; ++i
, ++line_count
)
572 std::getline(f
, line
); // Ignore up to start of next line
574 // TODO: Parse fairness constraints
575 for (unsigned i
= 0; i
< F
; ++i
, ++line_count
)
576 std::getline(f
, line
); // Ignore up to start of next line
579 for (unsigned i
= 0; i
< A
; ++i
) {
580 if (!(f
>> l1
>> l2
>> l3
))
581 log_error("Line %u cannot be interpreted as an AND!\n", line_count
);
583 log_debug("%d %d %d is an AND\n", l1
, l2
, l3
);
584 log_assert(!(l1
& 1));
585 RTLIL::Wire
*o_wire
= createWireIfNotExists(module
, l1
);
586 RTLIL::Wire
*i1_wire
= createWireIfNotExists(module
, l2
);
587 RTLIL::Wire
*i2_wire
= createWireIfNotExists(module
, l3
);
588 module
->addAndGate(o_wire
->name
.str() + "$and", i1_wire
, i2_wire
, o_wire
);
590 std::getline(f
, line
); // Ignore up to start of next line
593 static unsigned parse_next_delta_literal(std::istream
&f
, unsigned ref
)
595 unsigned x
= 0, i
= 0;
597 while ((ch
= f
.get()) & 0x80)
598 x
|= (ch
& 0x7f) << (7 * i
++);
599 return ref
- (x
| (ch
<< (7 * i
)));
602 void AigerReader::parse_aiger_binary()
608 for (unsigned i
= 1; i
<= I
; ++i
) {
609 log_debug("%d is an input\n", i
);
610 RTLIL::Wire
*wire
= createWireIfNotExists(module
, i
<< 1);
611 wire
->port_input
= true;
612 log_assert(!wire
->port_output
);
613 inputs
.push_back(wire
);
617 RTLIL::Wire
*clk_wire
= nullptr;
619 log_assert(clk_name
!= "");
620 clk_wire
= module
->wire(clk_name
);
621 log_assert(!clk_wire
);
622 log_debug("Creating %s\n", clk_name
.c_str());
623 clk_wire
= module
->addWire(clk_name
);
624 clk_wire
->port_input
= true;
625 clk_wire
->port_output
= false;
628 for (unsigned i
= 0; i
< L
; ++i
, ++line_count
, l1
+= 2) {
630 log_error("Line %u cannot be interpreted as a latch!\n", line_count
);
631 log_debug("%d %d is a latch\n", l1
, l2
);
632 RTLIL::Wire
*q_wire
= createWireIfNotExists(module
, l1
);
633 RTLIL::Wire
*d_wire
= createWireIfNotExists(module
, l2
);
635 module
->addDff(NEW_ID
, clk_wire
, d_wire
, q_wire
);
637 // Reset logic is optional in AIGER 1.9
638 if (f
.peek() == ' ') {
640 log_error("Line %u cannot be interpreted as a latch!\n", line_count
);
643 q_wire
->attributes
["\\init"] = RTLIL::S0
;
645 q_wire
->attributes
["\\init"] = RTLIL::S1
;
647 //q_wire->attributes["\\init"] = RTLIL::Sx;
650 log_error("Line %u has invalid reset literal for latch!\n", line_count
);
653 // AIGER latches are assumed to be initialized to zero
654 q_wire
->attributes
["\\init"] = RTLIL::S0
;
656 latches
.push_back(q_wire
);
660 for (unsigned i
= 0; i
< O
; ++i
, ++line_count
) {
662 log_error("Line %u cannot be interpreted as an output!\n", line_count
);
664 log_debug("%d is an output\n", l1
);
665 const unsigned variable
= l1
>> 1;
666 const bool invert
= l1
& 1;
667 RTLIL::IdString
wire_name(stringf("\\__%d%s__", variable
, invert
? "b" : "")); // FIXME: is "_b" the right suffix?
668 RTLIL::Wire
*wire
= module
->wire(wire_name
);
670 wire
= createWireIfNotExists(module
, l1
);
671 else if (wire
->port_input
|| wire
->port_output
) {
672 RTLIL::Wire
*new_wire
= module
->addWire(NEW_ID
);
673 module
->connect(new_wire
, wire
);
676 wire
->port_output
= true;
677 outputs
.push_back(wire
);
679 std::getline(f
, line
); // Ignore up to start of next line
681 // Parse bad properties
682 for (unsigned i
= 0; i
< B
; ++i
, ++line_count
) {
684 log_error("Line %u cannot be interpreted as a bad state property!\n", line_count
);
686 log_debug("%d is a bad state property\n", l1
);
687 RTLIL::Wire
*wire
= createWireIfNotExists(module
, l1
);
688 wire
->port_output
= true;
689 bad_properties
.push_back(wire
);
692 std::getline(f
, line
); // Ignore up to start of next line
694 // TODO: Parse invariant constraints
695 for (unsigned i
= 0; i
< C
; ++i
, ++line_count
)
696 std::getline(f
, line
); // Ignore up to start of next line
698 // TODO: Parse justice properties
699 for (unsigned i
= 0; i
< J
; ++i
, ++line_count
)
700 std::getline(f
, line
); // Ignore up to start of next line
702 // TODO: Parse fairness constraints
703 for (unsigned i
= 0; i
< F
; ++i
, ++line_count
)
704 std::getline(f
, line
); // Ignore up to start of next line
708 for (unsigned i
= 0; i
< A
; ++i
, ++line_count
, l1
+= 2) {
709 l2
= parse_next_delta_literal(f
, l1
);
710 l3
= parse_next_delta_literal(f
, l2
);
712 log_debug("%d %d %d is an AND\n", l1
, l2
, l3
);
713 log_assert(!(l1
& 1));
714 RTLIL::Wire
*o_wire
= createWireIfNotExists(module
, l1
);
715 RTLIL::Wire
*i1_wire
= createWireIfNotExists(module
, l2
);
716 RTLIL::Wire
*i2_wire
= createWireIfNotExists(module
, l3
);
717 module
->addAndGate(o_wire
->name
.str() + "$and", i1_wire
, i2_wire
, o_wire
);
721 void AigerReader::post_process()
723 pool
<RTLIL::Module
*> abc_carry_modules
;
724 unsigned ci_count
= 0, co_count
= 0, flop_count
= 0;
725 for (auto cell
: boxes
) {
726 RTLIL::Module
* box_module
= design
->module(cell
->type
);
727 log_assert(box_module
);
729 if (box_module
->attributes
.count("\\abc_carry") && !abc_carry_modules
.count(box_module
)) {
730 RTLIL::Wire
* carry_in
= nullptr, *carry_out
= nullptr;
731 RTLIL::Wire
* last_in
= nullptr, *last_out
= nullptr;
732 for (const auto &port_name
: box_module
->ports
) {
733 RTLIL::Wire
* w
= box_module
->wire(port_name
);
736 if (w
->attributes
.count("\\abc_carry_in")) {
737 log_assert(!carry_in
);
740 log_assert(!last_in
|| last_in
->port_id
< w
->port_id
);
743 if (w
->port_output
) {
744 if (w
->attributes
.count("\\abc_carry_out")) {
745 log_assert(!carry_out
);
748 log_assert(!last_out
|| last_out
->port_id
< w
->port_id
);
753 if (carry_in
!= last_in
) {
754 std::swap(box_module
->ports
[carry_in
->port_id
], box_module
->ports
[last_in
->port_id
]);
755 std::swap(carry_in
->port_id
, last_in
->port_id
);
757 if (carry_out
!= last_out
) {
758 log_assert(last_out
);
759 std::swap(box_module
->ports
[carry_out
->port_id
], box_module
->ports
[last_out
->port_id
]);
760 std::swap(carry_out
->port_id
, last_out
->port_id
);
764 bool flop
= box_module
->attributes
.count("\\abc_flop");
765 log_assert(!flop
|| flop_count
< flopNum
);
767 // NB: Assume box_module->ports are sorted alphabetically
768 // (as RTLIL::Module::fixup_ports() would do)
769 for (auto port_name
: box_module
->ports
) {
770 RTLIL::Wire
* w
= box_module
->wire(port_name
);
773 RTLIL::Wire
* wire
= nullptr;
774 for (int i
= 0; i
< GetSize(w
); i
++) {
776 log_assert(co_count
< outputs
.size());
777 wire
= outputs
[co_count
++];
779 log_assert(wire
->port_output
);
780 wire
->port_output
= false;
782 if (flop
&& w
->attributes
.count("\\abc_flop_d")) {
783 RTLIL::Wire
* d
= outputs
[outputs
.size() - flopNum
+ flop_count
];
785 log_assert(d
->port_output
);
786 d
->port_output
= false;
789 if (w
->port_output
) {
790 log_assert((piNum
+ ci_count
) < inputs
.size());
791 wire
= inputs
[piNum
+ ci_count
++];
793 log_assert(wire
->port_input
);
794 wire
->port_input
= false;
796 if (flop
&& w
->attributes
.count("\\abc_flop_q")) {
797 wire
= inputs
[piNum
- flopNum
+ flop_count
];
799 log_assert(wire
->port_input
);
800 wire
->port_input
= false;
805 cell
->setPort(port_name
, rhs
);
808 if (flop
) flop_count
++;
811 dict
<RTLIL::IdString
, int> wideports_cache
;
813 if (!map_filename
.empty()) {
814 std::ifstream
mf(map_filename
);
815 std::string type
, symbol
;
817 while (mf
>> type
>> variable
>> index
>> symbol
) {
818 RTLIL::IdString escaped_s
= RTLIL::escape_id(symbol
);
819 if (type
== "input") {
820 log_assert(static_cast<unsigned>(variable
) < inputs
.size());
821 RTLIL::Wire
* wire
= inputs
[variable
];
823 log_assert(wire
->port_input
);
826 // Cope with the fact that a CI might be identical
827 // to a PI (necessary due to ABC); in those cases
828 // simply connect the latter to the former
829 RTLIL::Wire
* existing
= module
->wire(escaped_s
);
831 module
->rename(wire
, escaped_s
);
833 wire
->port_input
= false;
834 module
->connect(wire
, existing
);
837 else if (index
> 0) {
838 std::string indexed_name
= stringf("%s[%d]", escaped_s
.c_str(), index
);
839 RTLIL::Wire
* existing
= module
->wire(indexed_name
);
841 module
->rename(wire
, indexed_name
);
843 wideports_cache
[escaped_s
] = std::max(wideports_cache
[escaped_s
], index
);
846 module
->connect(wire
, existing
);
847 wire
->port_input
= false;
851 else if (type
== "output") {
852 log_assert(static_cast<unsigned>(variable
+ co_count
) < outputs
.size());
853 RTLIL::Wire
* wire
= outputs
[variable
+ co_count
];
855 log_assert(wire
->port_output
);
858 // Cope with the fact that a CO might be identical
859 // to a PO (necessary due to ABC); in those cases
860 // simply connect the latter to the former
861 RTLIL::Wire
* existing
= module
->wire(escaped_s
);
863 if (escaped_s
.ends_with("$inout.out")) {
864 wire
->port_output
= false;
865 RTLIL::Wire
*in_wire
= module
->wire(escaped_s
.substr(0, escaped_s
.size()-10));
867 log_assert(in_wire
->port_input
&& !in_wire
->port_output
);
868 in_wire
->port_output
= true;
869 module
->connect(in_wire
, wire
);
872 module
->rename(wire
, escaped_s
);
875 wire
->port_output
= false;
876 module
->connect(wire
, existing
);
879 else if (index
> 0) {
880 std::string indexed_name
= stringf("%s[%d]", escaped_s
.c_str(), index
);
881 RTLIL::Wire
* existing
= module
->wire(indexed_name
);
883 if (escaped_s
.ends_with("$inout.out")) {
884 wire
->port_output
= false;
885 RTLIL::Wire
*in_wire
= module
->wire(stringf("%s[%d]", escaped_s
.substr(0, escaped_s
.size()-10).c_str(), index
));
887 log_assert(in_wire
->port_input
&& !in_wire
->port_output
);
888 in_wire
->port_output
= true;
889 module
->connect(in_wire
, wire
);
892 module
->rename(wire
, indexed_name
);
894 wideports_cache
[escaped_s
] = std::max(wideports_cache
[escaped_s
], index
);
898 module
->connect(wire
, existing
);
899 wire
->port_output
= false;
903 else if (type
== "box") {
904 RTLIL::Cell
* cell
= module
->cell(stringf("$__box%d__", variable
));
905 if (cell
) { // ABC could have optimised this box away
906 module
->rename(cell
, escaped_s
);
907 RTLIL::Module
* box_module
= design
->module(cell
->type
);
908 log_assert(box_module
);
910 for (const auto &i
: cell
->connections()) {
911 RTLIL::IdString port_name
= i
.first
;
912 RTLIL::SigSpec rhs
= i
.second
;
914 for (auto bit
: rhs
.bits()) {
915 RTLIL::Wire
* wire
= bit
.wire
;
916 RTLIL::IdString escaped_s
= RTLIL::escape_id(stringf("%s.%s", log_id(cell
), log_id(port_name
)));
918 module
->rename(wire
, escaped_s
);
919 else if (index
> 0) {
920 module
->rename(wire
, stringf("%s[%d]", escaped_s
.c_str(), index
));
922 wideports_cache
[escaped_s
] = std::max(wideports_cache
[escaped_s
], index
);
930 log_error("Symbol type '%s' not recognised.\n", type
.c_str());
934 for (auto &wp
: wideports_cache
) {
935 auto name
= wp
.first
;
936 int width
= wp
.second
+ 1;
938 RTLIL::Wire
*wire
= module
->wire(name
);
940 module
->rename(wire
, RTLIL::escape_id(stringf("%s[%d]", name
.c_str(), 0)));
942 // Do not make ports with a mix of input/output into
944 bool port_input
= false, port_output
= false;
945 for (int i
= 0; i
< width
; i
++) {
946 RTLIL::IdString other_name
= name
.str() + stringf("[%d]", i
);
947 RTLIL::Wire
*other_wire
= module
->wire(other_name
);
949 port_input
= port_input
|| other_wire
->port_input
;
950 port_output
= port_output
|| other_wire
->port_output
;
954 wire
= module
->addWire(name
, width
);
955 wire
->port_input
= port_input
;
956 wire
->port_output
= port_output
;
958 for (int i
= 0; i
< width
; i
++) {
959 RTLIL::IdString other_name
= name
.str() + stringf("[%d]", i
);
960 RTLIL::Wire
*other_wire
= module
->wire(other_name
);
962 other_wire
->port_input
= false;
963 other_wire
->port_output
= false;
964 if (wire
->port_input
)
965 module
->connect(other_wire
, SigSpec(wire
, i
));
967 module
->connect(SigSpec(wire
, i
), other_wire
);
972 module
->fixup_ports();
975 design
->selection_stack
.emplace_back(false);
976 RTLIL::Selection
& sel
= design
->selection_stack
.back();
979 Pass::call(design
, "clean");
981 design
->selection_stack
.pop_back();
983 for (auto cell
: module
->cells().to_vector()) {
984 if (cell
->type
!= "$lut") continue;
985 auto y_port
= cell
->getPort("\\Y").as_bit();
986 if (y_port
.wire
->width
== 1)
987 module
->rename(cell
, stringf("%s$lut", y_port
.wire
->name
.c_str()));
989 module
->rename(cell
, stringf("%s[%d]$lut", y_port
.wire
->name
.c_str(), y_port
.offset
));
993 struct AigerFrontend
: public Frontend
{
994 AigerFrontend() : Frontend("aiger", "read AIGER file") { }
995 void help() YS_OVERRIDE
997 // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
999 log(" read_aiger [options] [filename]\n");
1001 log("Load module from an AIGER file into the current design.\n");
1003 log(" -module_name <module_name>\n");
1004 log(" Name of module to be created (default: <filename>)\n");
1006 log(" -clk_name <wire_name>\n");
1007 log(" AIGER latches to be transformed into posedge DFFs clocked by wire of");
1008 log(" this name (default: clk)\n");
1010 log(" -map <filename>\n");
1011 log(" read file with port and latch symbols\n");
1013 log(" -wideports\n");
1014 log(" Merge ports that match the pattern 'name[int]' into a single\n");
1015 log(" multi-bit port 'name'.\n");
1018 void execute(std::istream
*&f
, std::string filename
, std::vector
<std::string
> args
, RTLIL::Design
*design
) YS_OVERRIDE
1020 log_header(design
, "Executing AIGER frontend.\n");
1022 RTLIL::IdString clk_name
= "\\clk";
1023 RTLIL::IdString module_name
;
1024 std::string map_filename
;
1025 bool wideports
= false;
1028 for (argidx
= 1; argidx
< args
.size(); argidx
++) {
1029 std::string arg
= args
[argidx
];
1030 if (arg
== "-module_name" && argidx
+1 < args
.size()) {
1031 module_name
= RTLIL::escape_id(args
[++argidx
]);
1034 if (arg
== "-clk_name" && argidx
+1 < args
.size()) {
1035 clk_name
= RTLIL::escape_id(args
[++argidx
]);
1038 if (map_filename
.empty() && arg
== "-map" && argidx
+1 < args
.size()) {
1039 map_filename
= args
[++argidx
];
1042 if (arg
== "-wideports") {
1048 extra_args(f
, filename
, args
, argidx
);
1050 if (module_name
.empty()) {
1052 char fname
[_MAX_FNAME
];
1053 _splitpath(filename
.c_str(), NULL
/* drive */, NULL
/* dir */, fname
, NULL
/* ext */)
1054 module_name
= fname
;
1056 char* bn
= strdup(filename
.c_str());
1057 module_name
= RTLIL::escape_id(bn
);
1062 AigerReader
reader(design
, *f
, module_name
, clk_name
, map_filename
, wideports
);
1063 reader
.parse_aiger();