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
25 // https://stackoverflow.com/a/46137633
28 #define __builtin_bswap32 _byteswap_ulong
29 #elif defined(__APPLE__)
30 #include <libkern/OSByteOrder.h>
31 #define __builtin_bswap32 OSSwapInt32
33 #ifndef __STDC_FORMAT_MACROS
34 #define __STDC_FORMAT_MACROS
38 #include "kernel/yosys.h"
39 #include "kernel/sigtools.h"
40 #include "kernel/celltypes.h"
41 #include "aigerparse.h"
45 inline int32_t from_big_endian(int32_t i32
) {
46 #if __BYTE_ORDER__ == __ORDER_LITTLE_ENDIAN__
47 return __builtin_bswap32(i32
);
48 #elif __BYTE_ORDER__ == __ORDER_BIG_ENDIAN__
51 #error "Unknown endianness"
55 #define log_debug2(...) ;
56 //#define log_debug2(...) log_debug(__VA_ARGS__)
60 RTLIL::Module
*module
;
61 dict
<RTLIL::SigBit
, RTLIL::State
> values_map
;
62 dict
<RTLIL::SigBit
, RTLIL::Cell
*> sig2driver
;
63 dict
<SigBit
, pool
<RTLIL::SigBit
>> sig2deps
;
65 ConstEvalAig(RTLIL::Module
*module
) : module(module
)
67 for (auto &it
: module
->cells_
) {
68 if (!yosys_celltypes
.cell_known(it
.second
->type
))
70 for (auto &it2
: it
.second
->connections())
71 if (yosys_celltypes
.cell_output(it
.second
->type
, it2
.first
)) {
72 auto r
YS_ATTRIBUTE(unused
) = sig2driver
.insert(std::make_pair(it2
.second
, it
.second
));
84 void set(RTLIL::SigBit sig
, RTLIL::State value
)
86 auto it
= values_map
.find(sig
);
88 if (it
!= values_map
.end()) {
89 RTLIL::State current_val
= it
->second
;
90 log_assert(current_val
== value
);
93 if (it
!= values_map
.end())
96 values_map
[sig
] = value
;
99 void set_incremental(RTLIL::SigSpec sig
, RTLIL::Const value
)
101 log_assert(GetSize(sig
) == GetSize(value
));
103 for (int i
= 0; i
< GetSize(sig
); i
++) {
104 auto it
= values_map
.find(sig
[i
]);
105 if (it
!= values_map
.end()) {
106 RTLIL::State current_val
= it
->second
;
107 if (current_val
!= value
[i
])
108 for (auto dep
: sig2deps
[sig
[i
]])
109 values_map
.erase(dep
);
110 it
->second
= value
[i
];
113 values_map
[sig
[i
]] = value
[i
];
117 void compute_deps(RTLIL::SigBit output
, const pool
<RTLIL::SigBit
> &inputs
)
119 sig2deps
[output
].insert(output
);
121 RTLIL::Cell
*cell
= sig2driver
.at(output
);
122 RTLIL::SigBit sig_a
= cell
->getPort(ID::A
);
123 sig2deps
[sig_a
].reserve(sig2deps
[sig_a
].size() + sig2deps
[output
].size()); // Reserve so that any invalidation
124 // that may occur does so here, and
125 // not mid insertion (below)
126 sig2deps
[sig_a
].insert(sig2deps
[output
].begin(), sig2deps
[output
].end());
127 if (!inputs
.count(sig_a
))
128 compute_deps(sig_a
, inputs
);
130 if (cell
->type
== ID($_AND_
)) {
131 RTLIL::SigSpec sig_b
= cell
->getPort(ID::B
);
132 sig2deps
[sig_b
].reserve(sig2deps
[sig_b
].size() + sig2deps
[output
].size()); // Reserve so that any invalidation
133 // that may occur does so here, and
134 // not mid insertion (below)
135 sig2deps
[sig_b
].insert(sig2deps
[output
].begin(), sig2deps
[output
].end());
137 if (!inputs
.count(sig_b
))
138 compute_deps(sig_b
, inputs
);
140 else if (cell
->type
== ID($_NOT_
)) {
145 bool eval(RTLIL::Cell
*cell
)
147 RTLIL::SigBit sig_y
= cell
->getPort(ID::Y
);
148 if (values_map
.count(sig_y
))
151 RTLIL::SigBit sig_a
= cell
->getPort(ID::A
);
155 RTLIL::State eval_ret
= RTLIL::Sx
;
156 if (cell
->type
== ID($_NOT_
)) {
157 if (sig_a
== State::S0
) eval_ret
= State::S1
;
158 else if (sig_a
== State::S1
) eval_ret
= State::S0
;
160 else if (cell
->type
== ID($_AND_
)) {
161 if (sig_a
== State::S0
) {
162 eval_ret
= State::S0
;
167 RTLIL::SigBit sig_b
= cell
->getPort(ID::B
);
170 if (sig_b
== State::S0
) {
171 eval_ret
= State::S0
;
175 if (sig_a
!= State::S1
|| sig_b
!= State::S1
)
178 eval_ret
= State::S1
;
184 set(sig_y
, eval_ret
);
188 bool eval(RTLIL::SigBit
&sig
)
190 auto it
= values_map
.find(sig
);
191 if (it
!= values_map
.end()) {
196 RTLIL::Cell
*cell
= sig2driver
.at(sig
);
200 it
= values_map
.find(sig
);
201 if (it
!= values_map
.end()) {
210 AigerReader::AigerReader(RTLIL::Design
*design
, std::istream
&f
, RTLIL::IdString module_name
, RTLIL::IdString clk_name
, std::string map_filename
, bool wideports
)
211 : design(design
), f(f
), clk_name(clk_name
), map_filename(map_filename
), wideports(wideports
), aiger_autoidx(autoidx
++)
213 module
= new RTLIL::Module
;
214 module
->name
= module_name
;
215 if (design
->module(module
->name
))
216 log_error("Duplicate definition of module %s!\n", log_id(module
->name
));
219 void AigerReader::parse_aiger()
223 if (header
!= "aag" && header
!= "aig")
224 log_error("Unsupported AIGER file!\n");
226 // Parse rest of header
227 if (!(f
>> M
>> I
>> L
>> O
>> A
))
228 log_error("Invalid AIGER header\n");
232 if (f
.peek() != ' ') goto end_of_header
;
233 if (!(f
>> B
)) log_error("Invalid AIGER header\n");
234 if (f
.peek() != ' ') goto end_of_header
;
235 if (!(f
>> C
)) log_error("Invalid AIGER header\n");
236 if (f
.peek() != ' ') goto end_of_header
;
237 if (!(f
>> J
)) log_error("Invalid AIGER header\n");
238 if (f
.peek() != ' ') goto end_of_header
;
239 if (!(f
>> F
)) log_error("Invalid AIGER header\n");
243 std::getline(f
, line
); // Ignore up to start of next line, as standard
244 // says anything that follows could be used for
247 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
);
255 else if (header
== "aig")
256 parse_aiger_binary();
260 RTLIL::Wire
* n0
= module
->wire(stringf("$aiger%d$0", aiger_autoidx
));
262 module
->connect(n0
, State::S0
);
264 // Parse footer (symbol table, comments, etc.)
267 for (int c
= f
.peek(); c
!= EOF
; c
= f
.peek(), ++line_count
) {
268 if (c
== 'i' || c
== 'l' || c
== 'o' || c
== 'b') {
271 log_error("Line %u cannot be interpreted as a symbol entry!\n", line_count
);
273 if ((c
== 'i' && l1
> inputs
.size()) || (c
== 'l' && l1
> latches
.size()) || (c
== 'o' && l1
> outputs
.size()))
274 log_error("Line %u has invalid symbol position!\n", line_count
);
276 RTLIL::IdString escaped_s
= stringf("\\%s", s
.c_str());
278 if (c
== 'i') wire
= inputs
[l1
];
279 else if (c
== 'l') wire
= latches
[l1
];
281 wire
= module
->wire(escaped_s
);
283 // Could have been renamed by a latch
284 module
->swap_names(wire
, outputs
[l1
]);
285 module
->connect(outputs
[l1
], wire
);
290 else if (c
== 'b') wire
= bad_properties
[l1
];
293 module
->rename(wire
, escaped_s
);
295 else if (c
== 'j' || c
== 'f') {
300 if (f
.peek() == '\r')
302 if (f
.peek() == '\n')
304 // Else constraint (TODO)
307 log_error("Line %u: cannot interpret first character '%c'!\n", line_count
, c
);
309 std::getline(f
, line
); // Ignore up to start of next line
315 static uint32_t parse_xaiger_literal(std::istream
&f
)
318 f
.read(reinterpret_cast<char*>(&l
), sizeof(l
));
319 if (f
.gcount() != sizeof(l
))
320 #if defined(_WIN32) && defined(__MINGW32__)
321 log_error("Offset %I64d: unable to read literal!\n", static_cast<int64_t>(f
.tellg()));
323 log_error("Offset %" PRId64
": unable to read literal!\n", static_cast<int64_t>(f
.tellg()));
325 return from_big_endian(l
);
328 RTLIL::Wire
* AigerReader::createWireIfNotExists(RTLIL::Module
*module
, unsigned literal
)
330 const unsigned variable
= literal
>> 1;
331 const bool invert
= literal
& 1;
332 RTLIL::IdString
wire_name(stringf("$aiger%d$%d%s", aiger_autoidx
, variable
, invert
? "b" : ""));
333 RTLIL::Wire
*wire
= module
->wire(wire_name
);
334 if (wire
) return wire
;
335 log_debug2("Creating %s\n", wire_name
.c_str());
336 wire
= module
->addWire(wire_name
);
337 wire
->port_input
= wire
->port_output
= false;
338 if (!invert
) return wire
;
339 RTLIL::IdString
wire_inv_name(stringf("$aiger%d$%d", aiger_autoidx
, variable
));
340 RTLIL::Wire
*wire_inv
= module
->wire(wire_inv_name
);
342 if (module
->cell(wire_inv_name
)) return wire
;
345 log_debug2("Creating %s\n", wire_inv_name
.c_str());
346 wire_inv
= module
->addWire(wire_inv_name
);
347 wire_inv
->port_input
= wire_inv
->port_output
= false;
350 log_debug2("Creating %s = ~%s\n", wire_name
.c_str(), wire_inv_name
.c_str());
351 module
->addNotGate(stringf("$not$aiger%d$%d", aiger_autoidx
, variable
), wire_inv
, wire
);
356 void AigerReader::parse_xaiger()
360 if (header
!= "aag" && header
!= "aig")
361 log_error("Unsupported AIGER file!\n");
363 // Parse rest of header
364 if (!(f
>> M
>> I
>> L
>> O
>> A
))
365 log_error("Invalid AIGER header\n");
371 std::getline(f
, line
); // Ignore up to start of next line, as standard
372 // says anything that follows could be used for
375 log_debug("M=%u I=%u L=%u O=%u A=%u\n", M
, I
, L
, O
, A
);
383 else if (header
== "aig")
384 parse_aiger_binary();
388 RTLIL::Wire
* n0
= module
->wire(stringf("$aiger%d$0", aiger_autoidx
));
390 module
->connect(n0
, State::S0
);
394 log_error("Line %u: cannot interpret first character '%c'!\n", line_count
, c
);
395 if (f
.peek() == '\n')
398 // Parse footer (symbol table, comments, etc.)
400 for (int c
= f
.get(); c
!= EOF
; c
= f
.get()) {
403 uint32_t dataSize
YS_ATTRIBUTE(unused
) = parse_xaiger_literal(f
);
404 uint32_t lutNum
= parse_xaiger_literal(f
);
405 uint32_t lutSize
YS_ATTRIBUTE(unused
) = parse_xaiger_literal(f
);
406 log_debug("m: dataSize=%u lutNum=%u lutSize=%u\n", dataSize
, lutNum
, lutSize
);
407 ConstEvalAig
ce(module
);
408 for (unsigned i
= 0; i
< lutNum
; ++i
) {
409 uint32_t rootNodeID
= parse_xaiger_literal(f
);
410 uint32_t cutLeavesM
= parse_xaiger_literal(f
);
411 log_debug2("rootNodeID=%d cutLeavesM=%d\n", rootNodeID
, cutLeavesM
);
412 RTLIL::Wire
*output_sig
= module
->wire(stringf("$aiger%d$%d", aiger_autoidx
, rootNodeID
));
413 log_assert(output_sig
);
415 RTLIL::SigSpec input_sig
;
416 for (unsigned j
= 0; j
< cutLeavesM
; ++j
) {
417 nodeID
= parse_xaiger_literal(f
);
418 log_debug2("\t%u\n", nodeID
);
420 log_debug("\tLUT '$lut$aiger%d$%d' input %d is constant!\n", aiger_autoidx
, rootNodeID
, cutLeavesM
);
423 RTLIL::Wire
*wire
= module
->wire(stringf("$aiger%d$%d", aiger_autoidx
, nodeID
));
425 input_sig
.append(wire
);
427 // Reverse input order as fastest input is returned first
429 // TODO: Compute LUT mask from AIG in less than O(2 ** input_sig.size())
431 ce
.compute_deps(output_sig
, input_sig
.to_sigbit_pool());
432 RTLIL::Const
lut_mask(RTLIL::State::Sx
, 1 << GetSize(input_sig
));
433 for (int j
= 0; j
< GetSize(lut_mask
); ++j
) {
434 int gray
= j
^ (j
>> 1);
435 ce
.set_incremental(input_sig
, RTLIL::Const
{gray
, GetSize(input_sig
)});
436 RTLIL::SigBit
o(output_sig
);
437 bool success
YS_ATTRIBUTE(unused
) = ce
.eval(o
);
439 log_assert(o
.wire
== nullptr);
440 lut_mask
[gray
] = o
.data
;
442 RTLIL::Cell
*output_cell
= module
->cell(stringf("$and$aiger%d$%d", aiger_autoidx
, rootNodeID
));
443 log_assert(output_cell
);
444 module
->remove(output_cell
);
445 module
->addLut(stringf("$lut$aiger%d$%d", aiger_autoidx
, rootNodeID
), input_sig
, output_sig
, std::move(lut_mask
));
449 uint32_t dataSize
YS_ATTRIBUTE(unused
) = parse_xaiger_literal(f
);
450 flopNum
= parse_xaiger_literal(f
);
451 log_debug("flopNum = %u\n", flopNum
);
452 log_assert(dataSize
== (flopNum
+1) * sizeof(uint32_t));
453 mergeability
.reserve(flopNum
);
454 for (unsigned i
= 0; i
< flopNum
; i
++)
455 mergeability
.emplace_back(parse_xaiger_literal(f
));
458 uint32_t dataSize
YS_ATTRIBUTE(unused
) = parse_xaiger_literal(f
);
459 flopNum
= parse_xaiger_literal(f
);
460 log_assert(dataSize
== (flopNum
+1) * sizeof(uint32_t));
461 initial_state
.reserve(flopNum
);
462 for (unsigned i
= 0; i
< flopNum
; i
++)
463 initial_state
.emplace_back(parse_xaiger_literal(f
));
466 parse_xaiger_literal(f
);
468 log_debug("n: '%s'\n", s
.c_str());
471 f
.ignore(sizeof(uint32_t));
472 uint32_t version
YS_ATTRIBUTE(unused
) = parse_xaiger_literal(f
);
473 log_assert(version
== 1);
474 uint32_t ciNum
YS_ATTRIBUTE(unused
) = parse_xaiger_literal(f
);
475 log_debug("ciNum = %u\n", ciNum
);
476 uint32_t coNum
YS_ATTRIBUTE(unused
) = parse_xaiger_literal(f
);
477 log_debug("coNum = %u\n", coNum
);
478 piNum
= parse_xaiger_literal(f
);
479 log_debug("piNum = %u\n", piNum
);
480 uint32_t poNum
YS_ATTRIBUTE(unused
) = parse_xaiger_literal(f
);
481 log_debug("poNum = %u\n", poNum
);
482 uint32_t boxNum
= parse_xaiger_literal(f
);
483 log_debug("boxNum = %u\n", boxNum
);
484 for (unsigned i
= 0; i
< boxNum
; i
++) {
485 uint32_t boxInputs
= parse_xaiger_literal(f
);
486 uint32_t boxOutputs
= parse_xaiger_literal(f
);
487 uint32_t boxUniqueId
= parse_xaiger_literal(f
);
488 log_assert(boxUniqueId
> 0);
489 uint32_t oldBoxNum
= parse_xaiger_literal(f
);
490 RTLIL::Cell
* cell
= module
->addCell(stringf("$box%u", oldBoxNum
), stringf("$__boxid%u", boxUniqueId
));
491 cell
->setPort(ID(i
), SigSpec(State::S0
, boxInputs
));
492 cell
->setPort(ID(o
), SigSpec(State::S0
, boxOutputs
));
493 cell
->attributes
[ID::abc9_box_seq
] = oldBoxNum
;
494 boxes
.emplace_back(cell
);
497 else if (c
== 'a' || c
== 'i' || c
== 'o' || c
== 's') {
498 uint32_t dataSize
= parse_xaiger_literal(f
);
500 log_debug("ignoring '%c'\n", c
);
510 void AigerReader::parse_aiger_ascii()
513 std::stringstream ss
;
518 int digits
= ceil(log10(I
));
519 for (unsigned i
= 1; i
<= I
; ++i
, ++line_count
) {
521 log_error("Line %u cannot be interpreted as an input!\n", line_count
);
522 log_debug2("%d is an input\n", l1
);
523 log_assert(!(l1
& 1)); // Inputs can't be inverted
524 RTLIL::Wire
*wire
= module
->addWire(stringf("$i%0*d", digits
, l1
>> 1));
525 wire
->port_input
= true;
526 module
->connect(createWireIfNotExists(module
, l1
), wire
);
527 inputs
.push_back(wire
);
531 RTLIL::Wire
*clk_wire
= nullptr;
532 if (L
> 0 && !clk_name
.empty()) {
533 clk_wire
= module
->wire(clk_name
);
534 log_assert(!clk_wire
);
535 log_debug2("Creating %s\n", clk_name
.c_str());
536 clk_wire
= module
->addWire(clk_name
);
537 clk_wire
->port_input
= true;
538 clk_wire
->port_output
= false;
540 digits
= ceil(log10(L
));
541 for (unsigned i
= 0; i
< L
; ++i
, ++line_count
) {
542 if (!(f
>> l1
>> l2
))
543 log_error("Line %u cannot be interpreted as a latch!\n", line_count
);
544 log_debug2("%d %d is a latch\n", l1
, l2
);
545 log_assert(!(l1
& 1));
546 RTLIL::Wire
*q_wire
= module
->addWire(stringf("$l%0*d", digits
, l1
>> 1));
547 module
->connect(createWireIfNotExists(module
, l1
), q_wire
);
548 RTLIL::Wire
*d_wire
= createWireIfNotExists(module
, l2
);
551 module
->addDffGate(NEW_ID
, clk_wire
, d_wire
, q_wire
);
553 module
->addFfGate(NEW_ID
, d_wire
, q_wire
);
555 // Reset logic is optional in AIGER 1.9
556 if (f
.peek() == ' ') {
558 log_error("Line %u cannot be interpreted as a latch!\n", line_count
);
561 q_wire
->attributes
[ID::init
] = State::S0
;
563 q_wire
->attributes
[ID::init
] = State::S1
;
565 //q_wire->attributes[ID::init] = RTLIL::Sx;
568 log_error("Line %u has invalid reset literal for latch!\n", line_count
);
571 // AIGER latches are assumed to be initialized to zero
572 q_wire
->attributes
[ID::init
] = State::S0
;
574 latches
.push_back(q_wire
);
578 digits
= ceil(log10(O
));
579 for (unsigned i
= 0; i
< O
; ++i
, ++line_count
) {
581 log_error("Line %u cannot be interpreted as an output!\n", line_count
);
583 log_debug2("%d is an output\n", l1
);
584 RTLIL::Wire
*wire
= module
->addWire(stringf("$o%0*d", digits
, i
));
585 wire
->port_output
= true;
586 module
->connect(wire
, createWireIfNotExists(module
, l1
));
587 outputs
.push_back(wire
);
589 //std::getline(f, line); // Ignore up to start of next line
591 // Parse bad properties
592 for (unsigned i
= 0; i
< B
; ++i
, ++line_count
) {
594 log_error("Line %u cannot be interpreted as a bad state property!\n", line_count
);
596 log_debug2("%d is a bad state property\n", l1
);
597 RTLIL::Wire
*wire
= createWireIfNotExists(module
, l1
);
598 wire
->port_output
= true;
599 bad_properties
.push_back(wire
);
602 // std::getline(f, line); // Ignore up to start of next line
604 // TODO: Parse invariant constraints
605 for (unsigned i
= 0; i
< C
; ++i
, ++line_count
)
606 std::getline(f
, line
); // Ignore up to start of next line
608 // TODO: Parse justice properties
609 for (unsigned i
= 0; i
< J
; ++i
, ++line_count
)
610 std::getline(f
, line
); // Ignore up to start of next line
612 // TODO: Parse fairness constraints
613 for (unsigned i
= 0; i
< F
; ++i
, ++line_count
)
614 std::getline(f
, line
); // Ignore up to start of next line
617 for (unsigned i
= 0; i
< A
; ++i
) {
618 if (!(f
>> l1
>> l2
>> l3
))
619 log_error("Line %u cannot be interpreted as an AND!\n", line_count
);
621 log_debug2("%d %d %d is an AND\n", l1
, l2
, l3
);
622 log_assert(!(l1
& 1));
623 RTLIL::Wire
*o_wire
= createWireIfNotExists(module
, l1
);
624 RTLIL::Wire
*i1_wire
= createWireIfNotExists(module
, l2
);
625 RTLIL::Wire
*i2_wire
= createWireIfNotExists(module
, l3
);
626 module
->addAndGate("$and" + o_wire
->name
.str(), i1_wire
, i2_wire
, o_wire
);
628 std::getline(f
, line
); // Ignore up to start of next line
631 static unsigned parse_next_delta_literal(std::istream
&f
, unsigned ref
)
633 unsigned x
= 0, i
= 0;
635 while ((ch
= f
.get()) & 0x80)
636 x
|= (ch
& 0x7f) << (7 * i
++);
637 return ref
- (x
| (ch
<< (7 * i
)));
640 void AigerReader::parse_aiger_binary()
646 int digits
= ceil(log10(I
));
647 for (unsigned i
= 1; i
<= I
; ++i
) {
648 log_debug2("%d is an input\n", i
);
649 RTLIL::Wire
*wire
= module
->addWire(stringf("$i%0*d", digits
, i
));
650 wire
->port_input
= true;
651 module
->connect(createWireIfNotExists(module
, i
<< 1), wire
);
652 inputs
.push_back(wire
);
656 RTLIL::Wire
*clk_wire
= nullptr;
657 if (L
> 0 && !clk_name
.empty()) {
658 clk_wire
= module
->wire(clk_name
);
659 log_assert(!clk_wire
);
660 log_debug2("Creating %s\n", clk_name
.c_str());
661 clk_wire
= module
->addWire(clk_name
);
662 clk_wire
->port_input
= true;
663 clk_wire
->port_output
= false;
665 digits
= ceil(log10(L
));
667 for (unsigned i
= 0; i
< L
; ++i
, ++line_count
, l1
+= 2) {
669 log_error("Line %u cannot be interpreted as a latch!\n", line_count
);
670 log_debug("%d %d is a latch\n", l1
, l2
);
671 RTLIL::Wire
*q_wire
= module
->addWire(stringf("$l%0*d", digits
, l1
>> 1));
672 module
->connect(createWireIfNotExists(module
, l1
), q_wire
);
673 RTLIL::Wire
*d_wire
= createWireIfNotExists(module
, l2
);
676 module
->addDff(NEW_ID
, clk_wire
, d_wire
, q_wire
);
678 module
->addFf(NEW_ID
, d_wire
, q_wire
);
680 // Reset logic is optional in AIGER 1.9
681 if (f
.peek() == ' ') {
683 log_error("Line %u cannot be interpreted as a latch!\n", line_count
);
686 q_wire
->attributes
[ID::init
] = State::S0
;
688 q_wire
->attributes
[ID::init
] = State::S1
;
690 //q_wire->attributes[ID::init] = RTLIL::Sx;
693 log_error("Line %u has invalid reset literal for latch!\n", line_count
);
696 // AIGER latches are assumed to be initialized to zero
697 q_wire
->attributes
[ID::init
] = State::S0
;
699 latches
.push_back(q_wire
);
703 digits
= ceil(log10(O
));
704 for (unsigned i
= 0; i
< O
; ++i
, ++line_count
) {
706 log_error("Line %u cannot be interpreted as an output!\n", line_count
);
708 log_debug2("%d is an output\n", l1
);
709 RTLIL::Wire
*wire
= module
->addWire(stringf("$o%0*d", digits
, i
));
710 wire
->port_output
= true;
711 module
->connect(wire
, createWireIfNotExists(module
, l1
));
712 outputs
.push_back(wire
);
714 std::getline(f
, line
); // Ignore up to start of next line
716 // Parse bad properties
717 for (unsigned i
= 0; i
< B
; ++i
, ++line_count
) {
719 log_error("Line %u cannot be interpreted as a bad state property!\n", line_count
);
721 log_debug2("%d is a bad state property\n", l1
);
722 RTLIL::Wire
*wire
= createWireIfNotExists(module
, l1
);
723 wire
->port_output
= true;
724 bad_properties
.push_back(wire
);
727 std::getline(f
, line
); // Ignore up to start of next line
729 // TODO: Parse invariant constraints
730 for (unsigned i
= 0; i
< C
; ++i
, ++line_count
)
731 std::getline(f
, line
); // Ignore up to start of next line
733 // TODO: Parse justice properties
734 for (unsigned i
= 0; i
< J
; ++i
, ++line_count
)
735 std::getline(f
, line
); // Ignore up to start of next line
737 // TODO: Parse fairness constraints
738 for (unsigned i
= 0; i
< F
; ++i
, ++line_count
)
739 std::getline(f
, line
); // Ignore up to start of next line
743 for (unsigned i
= 0; i
< A
; ++i
, ++line_count
, l1
+= 2) {
744 l2
= parse_next_delta_literal(f
, l1
);
745 l3
= parse_next_delta_literal(f
, l2
);
747 log_debug2("%d %d %d is an AND\n", l1
, l2
, l3
);
748 log_assert(!(l1
& 1));
749 RTLIL::Wire
*o_wire
= createWireIfNotExists(module
, l1
);
750 RTLIL::Wire
*i1_wire
= createWireIfNotExists(module
, l2
);
751 RTLIL::Wire
*i2_wire
= createWireIfNotExists(module
, l3
);
752 module
->addAndGate("$and" + o_wire
->name
.str(), i1_wire
, i2_wire
, o_wire
);
756 void AigerReader::post_process()
758 unsigned ci_count
= 0, co_count
= 0;
759 for (auto cell
: boxes
) {
760 for (auto &bit
: cell
->connections_
.at(ID(i
))) {
761 log_assert(bit
== State::S0
);
762 log_assert(co_count
< outputs
.size());
763 bit
= outputs
[co_count
++];
764 log_assert(bit
.wire
&& GetSize(bit
.wire
) == 1);
765 log_assert(bit
.wire
->port_output
);
766 bit
.wire
->port_output
= false;
768 for (auto &bit
: cell
->connections_
.at(ID(o
))) {
769 log_assert(bit
== State::S0
);
770 log_assert((piNum
+ ci_count
) < inputs
.size());
771 bit
= inputs
[piNum
+ ci_count
++];
772 log_assert(bit
.wire
&& GetSize(bit
.wire
) == 1);
773 log_assert(bit
.wire
->port_input
);
774 bit
.wire
->port_input
= false;
778 dict
<int, Wire
*> mergeability_to_clock
;
779 for (uint32_t i
= 0; i
< flopNum
; i
++) {
780 RTLIL::Wire
*d
= outputs
[outputs
.size() - flopNum
+ i
];
782 log_assert(d
->port_output
);
783 d
->port_output
= false;
785 RTLIL::Wire
*q
= inputs
[piNum
- flopNum
+ i
];
787 log_assert(q
->port_input
);
788 q
->port_input
= false;
790 Cell
* ff
= module
->addFfGate(NEW_ID
, d
, q
);
791 ff
->attributes
[ID::abc9_mergeability
] = mergeability
[i
];
792 q
->attributes
[ID::init
] = initial_state
[i
];
795 dict
<RTLIL::IdString
, std::pair
<int,int>> wideports_cache
;
797 if (!map_filename
.empty()) {
798 std::ifstream
mf(map_filename
);
799 std::string type
, symbol
;
801 while (mf
>> type
>> variable
>> index
>> symbol
) {
802 RTLIL::IdString escaped_s
= RTLIL::escape_id(symbol
);
803 if (type
== "input") {
804 log_assert(static_cast<unsigned>(variable
) < inputs
.size());
805 RTLIL::Wire
* wire
= inputs
[variable
];
807 log_assert(wire
->port_input
);
808 log_debug("Renaming input %s", log_id(wire
));
810 RTLIL::Wire
*existing
= nullptr;
812 // Cope with the fact that a CI might be identical
813 // to a PI (necessary due to ABC); in those cases
814 // simply connect the latter to the former
815 existing
= module
->wire(escaped_s
);
817 module
->rename(wire
, escaped_s
);
819 wire
->port_input
= false;
820 module
->connect(wire
, existing
);
822 log_debug(" -> %s\n", log_id(escaped_s
));
825 RTLIL::IdString indexed_name
= stringf("%s[%d]", escaped_s
.c_str(), index
);
826 existing
= module
->wire(indexed_name
);
828 module
->rename(wire
, indexed_name
);
830 module
->connect(wire
, existing
);
831 wire
->port_input
= false;
833 log_debug(" -> %s\n", log_id(indexed_name
));
836 if (wideports
&& !existing
) {
837 auto r
= wideports_cache
.insert(escaped_s
);
839 r
.first
->second
.first
= index
;
840 r
.first
->second
.second
= index
;
843 r
.first
->second
.first
= std::min(r
.first
->second
.first
, index
);
844 r
.first
->second
.second
= std::max(r
.first
->second
.second
, index
);
848 else if (type
== "output") {
849 log_assert(static_cast<unsigned>(variable
+ co_count
) < outputs
.size());
850 RTLIL::Wire
* wire
= outputs
[variable
+ co_count
];
852 log_assert(wire
->port_output
);
853 log_debug("Renaming output %s", log_id(wire
));
855 RTLIL::Wire
*existing
;
857 // Cope with the fact that a CO might be identical
858 // to a PO (necessary due to ABC); in those cases
859 // simply connect the latter to the former
860 existing
= module
->wire(escaped_s
);
862 module
->rename(wire
, escaped_s
);
864 wire
->port_output
= false;
865 existing
->port_output
= true;
866 module
->connect(wire
, existing
);
869 log_debug(" -> %s\n", log_id(escaped_s
));
872 RTLIL::IdString indexed_name
= stringf("%s[%d]", escaped_s
.c_str(), index
);
873 existing
= module
->wire(indexed_name
);
875 module
->rename(wire
, indexed_name
);
877 wire
->port_output
= false;
878 existing
->port_output
= true;
879 module
->connect(wire
, existing
);
881 log_debug(" -> %s\n", log_id(indexed_name
));
884 if (wideports
&& !existing
) {
885 auto r
= wideports_cache
.insert(escaped_s
);
887 r
.first
->second
.first
= index
;
888 r
.first
->second
.second
= index
;
891 r
.first
->second
.first
= std::min(r
.first
->second
.first
, index
);
892 r
.first
->second
.second
= std::max(r
.first
->second
.second
, index
);
896 else if (type
== "box") {
897 RTLIL::Cell
* cell
= module
->cell(stringf("$box%d", variable
));
898 if (cell
) // ABC could have optimised this box away
899 module
->rename(cell
, escaped_s
);
902 log_error("Symbol type '%s' not recognised.\n", type
.c_str());
906 for (auto &wp
: wideports_cache
) {
907 auto name
= wp
.first
;
908 int min
= wp
.second
.first
;
909 int max
= wp
.second
.second
;
911 RTLIL::Wire
*wire
= module
->wire(name
);
913 module
->rename(wire
, RTLIL::escape_id(stringf("%s[%d]", name
.c_str(), 0)));
915 // Do not make ports with a mix of input/output into
917 bool port_input
= false, port_output
= false;
918 for (int i
= min
; i
<= max
; i
++) {
919 RTLIL::IdString other_name
= name
.str() + stringf("[%d]", i
);
920 RTLIL::Wire
*other_wire
= module
->wire(other_name
);
922 port_input
= port_input
|| other_wire
->port_input
;
923 port_output
= port_output
|| other_wire
->port_output
;
927 wire
= module
->addWire(name
, max
-min
+1);
928 wire
->start_offset
= min
;
929 wire
->port_input
= port_input
;
930 wire
->port_output
= port_output
;
932 for (int i
= min
; i
<= max
; i
++) {
933 RTLIL::IdString other_name
= stringf("%s[%d]", name
.c_str(), i
);
934 RTLIL::Wire
*other_wire
= module
->wire(other_name
);
936 other_wire
->port_input
= false;
937 other_wire
->port_output
= false;
938 if (wire
->port_input
)
939 module
->connect(other_wire
, SigSpec(wire
, i
-min
));
941 module
->connect(SigSpec(wire
, i
-min
), other_wire
);
946 module
->fixup_ports();
948 // Insert into a new (temporary) design so that "clean" will only
949 // operate (and run checks on) this one module
950 RTLIL::Design
*mapped_design
= new RTLIL::Design
;
951 mapped_design
->add(module
);
952 Pass::call(mapped_design
, "clean");
953 mapped_design
->modules_
.erase(module
->name
);
954 delete mapped_design
;
958 for (auto cell
: module
->cells().to_vector()) {
959 if (cell
->type
!= ID($lut
)) continue;
960 auto y_port
= cell
->getPort(ID::Y
).as_bit();
961 if (y_port
.wire
->width
== 1)
962 module
->rename(cell
, stringf("$lut%s", y_port
.wire
->name
.c_str()));
964 module
->rename(cell
, stringf("$lut%s[%d]", y_port
.wire
->name
.c_str(), y_port
.offset
));
968 struct AigerFrontend
: public Frontend
{
969 AigerFrontend() : Frontend("aiger", "read AIGER file") { }
970 void help() YS_OVERRIDE
972 // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
974 log(" read_aiger [options] [filename]\n");
976 log("Load module from an AIGER file into the current design.\n");
978 log(" -module_name <module_name>\n");
979 log(" name of module to be created (default: <filename>)\n");
981 log(" -clk_name <wire_name>\n");
982 log(" if specified, AIGER latches to be transformed into $_DFF_P_ cells\n");
983 log(" clocked by wire of this name. otherwise, $_FF_ cells will be used\n");
985 log(" -map <filename>\n");
986 log(" read file with port and latch symbols\n");
988 log(" -wideports\n");
989 log(" merge ports that match the pattern 'name[int]' into a single\n");
990 log(" multi-bit port 'name'\n");
993 log(" read XAIGER extensions\n");
996 void execute(std::istream
*&f
, std::string filename
, std::vector
<std::string
> args
, RTLIL::Design
*design
) YS_OVERRIDE
998 log_header(design
, "Executing AIGER frontend.\n");
1000 RTLIL::IdString clk_name
;
1001 RTLIL::IdString module_name
;
1002 std::string map_filename
;
1003 bool wideports
= false, xaiger
= false;
1006 for (argidx
= 1; argidx
< args
.size(); argidx
++) {
1007 std::string arg
= args
[argidx
];
1008 if (arg
== "-module_name" && argidx
+1 < args
.size()) {
1009 module_name
= RTLIL::escape_id(args
[++argidx
]);
1012 if (arg
== "-clk_name" && argidx
+1 < args
.size()) {
1013 clk_name
= RTLIL::escape_id(args
[++argidx
]);
1016 if (map_filename
.empty() && arg
== "-map" && argidx
+1 < args
.size()) {
1017 map_filename
= args
[++argidx
];
1020 if (arg
== "-wideports") {
1024 if (arg
== "-xaiger") {
1030 extra_args(f
, filename
, args
, argidx
, true);
1032 if (module_name
.empty()) {
1034 char fname
[_MAX_FNAME
];
1035 _splitpath(filename
.c_str(), NULL
/* drive */, NULL
/* dir */, fname
, NULL
/* ext */);
1036 char* bn
= strdup(fname
);
1037 module_name
= RTLIL::escape_id(bn
);
1040 char* bn
= strdup(filename
.c_str());
1041 module_name
= RTLIL::escape_id(bn
);
1046 AigerReader
reader(design
, *f
, module_name
, clk_name
, map_filename
, wideports
);
1048 reader
.parse_xaiger();
1050 reader
.parse_aiger();