README.md

AIGER Format Guide

Author: Hanmo Ou , Byron Hsu, Perry Chen

What are AIGER files?

AIGER files are used to describe logical circuits including only primary inputs, primary outputs, and And-Inverter gates.

Format of AIGER files

AIGER files consist of five parts:

1. Header
2. Input gates (primary inputs) (PIs)
3. Output gates (primary outputs) (POs)
4. AIGs (And-Inverter gates)
5. Symbols of PIs and POs （will not be included in this format guide)
6. Comments

Each gate is assigned a gate ID. Constant 0 gate is assigned gate ID 0 by default. (The "const 0" gate is assigned ID 0 without explicit declaration.)

Take this aag for example

orange: const, brown: input pins, blue: output pins, black: and gate, green: undef gate

aag 8 2 0 2 2
2
4
9
10
8 3 16
10 5 2
c
generated by Byron Hsu

The first line of a AAG file is the header,

which contains information of the circuit, including number of each type of gates and the maximum gate number. The header is written in the below format : aag M I L O A While: M is the maximum gate number (excluding outputs). I is the number of inputs. L is the number of latches (Ignored in our case). O is the number of outputs. A is the number of AND gates.

The following I lines are the primary inputs (PIs) listed by their literals:

Literals are used to declare whether a signal is inverted or not. For gate number N, its non-inverted literal is 2N, while its inverted literal is 2N+1. Since inputs are never inverted, the literals are always even. See the example above, the file lists

2
4

as the input section. So the input gate IDs are 1(2/2), 2(4/2).

After the PIs, the following O lines are the primary outputs (POs). The IDs of output gates are always numbered from M+1 to M+O. The literal in each line tells which signal they receive and whether it is inverted.

See the example above, M = 8,

9
10

Output gate 9(M+1) has inverted 4(9/2) as its input, and output gate 10(M+2) has 5(10/2) as its input.

Next, the following A lines are the AIG section. Each line consists of a gate literal, followed by its fanins' literals. (Fanins are the inputs of gates)

See the example above, M=8,

8 3 16
10 5 2

The first line indicates that AIG gate 4(8/2) has inverted 1(3/2) and 8(16/2) as its inputs. The second line indicates that AIG gate 5(10/2) has inverted 2(5/2) and 1(2/2) as its inputs.

Last of all, the character 'c' marks the end of the file. The rest after this line are comments and could be ignored.