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
    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)
    aigtocnf      translate combinational AIG into a CNF
    aigtoblif     translate AIG into BLIF
    aigtodot      visualizer for AIGs using 'dot' format
    aigtosmv      translate sequential AIG to SMV format
    andtoaig      translate file of AND gates into AIG
    aiguncomment  strip comments from AIG
    aigunroll     time frame expansion for bmc (previously called 'aigbmc')
    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.