README

AIGER is a format, library and set of utilities for And-Inverter Graphs (AIGs). For up-to-date version and more information see 'http://fmv.jku.at/aiger'.

To build use './configure.sh && make'. To install use 'make PREFIX=/usr/local install'.

The focus is on conversion utilities and a generic reader and writer API. A simple AIG library 'SimpAIG' is also included. It is currently only used in unrolling sequential models in 'aigunroll'.

documentation:

README                       this file
FORMAT                       detailed description of the format
LICENSE                      license and copyright

libraries:

aiger.h                      API of AIGER library ('aiger.c')
aiger.c                      read and write AIGs in AIGER format

simpaig.h                    API of SimpAIG library ('simpaig.c')
simpaig.c                    A compact and simple AIG library
                             (independent from 'aiger.c')

examples:

examples/*.aig               simple examples discussed in 'FORMAT'
examples/*.aag               (same in ASCII format)

examples/read.c              decoder code for binary integer repr.
examples/write.c             encoder code for binary integer repr.

examples/poormanaigtocnf.c   simple applications reading the binary format
examples/JaigerToCNF.java    without use of the AIGER library
                             (prototypes for competition readers)

utilities:

aigand           conjunction of all outputs
aigbmc           new bounded model checker for format 1.9.x including liveness
aigdd            delta debugger for AIGs in AIGER format
aigdep           determine inputs on which the outputs depend
aigflip          flip/negate all outputs
aigfuzz          fuzzer for AIGS in AIGER format
aiginfo          show comments of AIG
aigjoin          join AIGs over common inputs
aigmiter         generate miter of AIGER models
aigmove          treat non-primary outputs as primary outputs
aignm            show symbol table of AIG
aigor            disjunction of all outputs
aigreset         normalize constant reset either to 0 or 1
aigselect        select outputs from AIG (optionally reduce inputs to cone of influence)
aigsim           simulate AIG from stimulus or randomly
aigsplit         split outputs into separate files
aigstrip         strip symbols and comments from AIG
aigtoaig         converts AIG formats (ascii, binary, stripped, compressed)
aigtoblif        translate AIG into BLIF
aigtocnf         translate combinational AIG into a CNF
aigtobtor        translate AIG into BTOR
aigtodot         visualizer for AIGs using 'dot' format
aigtosmv         translate sequential AIG to SMV format
aiguncomment     strip comments from AIG
aigunconstraint  eliminate constraints by adding a latch
aigunfair        reduce justice properties and merge fairness constraints
aigunor          split a single OR output into multiple outputs
aigunroll        time frame expansion for bmc (previously called 'aigbmc')
andtoaig         translate file of AND gates into AIG
bliftoaig        translate flat BLIF model into AIG
mc.sh            SAT based model checker for AIGER using these tools
smvtoaig         translate flat boolean encoded SMV model into AIG
soltostim        extract input vector from DIMACS solution
wrapstim         sequential stimulus from expanded combinational stimulus

Armin Biere, JKU, Mai 2014.