team
contact
software
publications
teaching
jobs

AIGER

Introduction

AIGER is a format, library and set of utilities for And-Inverter Graphs (AIGs).

The differences of the latest AIGER 1.9 version from 2011 to the earlier AIGER 1 version are described the following technical report.

Armin Biere, Keijo Heljanko, Siert Wieringa. AIGER 1.9 And Beyond, Technical Report 11/2, July 2011, FMV Reports Series, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria.
[ report | bibtex | aiger ]

The old format report from 2007 still serves as reference manual and tutorial for all inherited features from older versions.

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.
[ report | bibtex | aiger ]

News

We are in the process of moving AIGER to github: http://github.com/arminbiere/aiger.

John Komp from the University of Colarado at Boulder provides a Python library:
[ https://github.com/JKomp/AIGER ]

Updated version aiger-1.9.4.tar.gz for HWMCC'14 CAV Edition. The main purpose of this release is to provide a new version of the aigsim tool. Other details are listed in the NEWS file.

New BEEM benchmarks.

The third realease aiger-1.9.4.tar.gz of the 1.9 series is available as well as all the benchmarks used in the HWMCC'11 competition.

A set of benchmarks translated into the new AIGER 1.9 format by Siert Wieringa.

The first official release 1.9.1 of the 1.9 series has been made available. This release was used for the new multi-property track and for the liveness track in HWMCC'11.

Alan Mishchenko kindly provides support for the AIGER format as input and output for his Logic Synthesis and Verification System ABC.

Source

[ aiger-1.9.9.tar.gz | aiger-1.9.4.tar.gz | aiger-1.9.1.tar.gz | aiger-20071012.zip ]

As you might have noticed we switched from a date to a more common version number scheme. Version 1.9.3 implements new features as described in the following draft but otherwise is only an incremental and intermediate release. The old pre 1.9 FORMAT report is still available.

See the NEWS file for more details. The README file describes the contents of the archive.

Geert Janssen generated a nice looking FORMAT-20070427.pdf out of the FORMAT report.

Benchmarks

BEEM AIG Benchmarks

[ beemaigs.7z | beembtors.7z ]

This set of benchmarks is derived from the BEEM explicit state model checking benchmark set. Jori Dubrovin translated them into the sequential BTOR format of our SMT solver Boolector. Here is a README which describes the process in more details. The benchmark set is split into the BTOR files and the synthesized AIG files.

LMCS'06 Aiger 1.9 Benchmarks

[ lmcs2006-aiger-1.9-benchmarks.tar.gz ]

This is a set of benchmarks translated into the new AIGER 1.9 format by Siert Wieringa. The original benchmark set is available from here. You find more information in the README file.

You might also want to check out the HWMCC'11 benchmarks and those of previous competitions.

Bit-Blasted SMT Problems

[ smtqfbv-aigs.7z (260MB) ]

We bit-blasted all the bit-vector problems published on July 2 2009 as training set for the SMT competition 2009 with our SMT solver Boolector except for the rather trivial and huge number of Sage examples.

Sequential Model Checking AIGER Benchmarks

[ tip-aig-20061215.zip ]

The archive contains model checking benchmarks converted from the Tip Suite with the tool 'smvtoaig', which is part of the AIGER distribution. We removed identical files and the examples are all simple safety properties. The sequential circuits represented in AIGER format have exactly one ouput, which is a bad state detector.

Structural SAT AIGER Benchmarks

[ tip-k-ind-aigs-o1234g.zip ]

Strutural SAT benchmarks, all unsatisfiable, encoding k-induction for a subset of the SMV models of the Tip-Suite. The archive contains 5 versions of each benchmark with different optimization levels as described in our paper Local Two-Level And-Inverter Graph Minimization without Blowup.

Other Ways to Obtain AIGER Benchmarks

In the AIGER distribution we include a couple of conversion utilities 'andtoaig', 'smvtoaig', and 'bliftoaig'. The bounded model checker 'aigbmc' can be used for time frame expansion of simple safety model checking problem. The result is a combinational AIG which represents a structural SAT problem.

The seperate tool 'smv2qbf' also produces structural SAT problems in AIGER format. In addition to plain bounded model checking it also supports k-induction. Unfortunately it can not be used to produce structural QBF problems in AIGER format yet.

The hardware model checking competition HWMCC'07 used AIGER as input format. The benchmarks used in the competition are available.

More recently we also published the converter cnf2aig. It extracts AIGs in AIGER format from a CNF in DIMACS format.

Finally our SAT solver 'c32sat' for C expressions can directly produce AIGs in AIGER format.

License

Since version 20061115 we switched to a MIT style LICENSE except for the 'bliftoaig' utility, which still has to use a BSD style license. Please refer to the LICENSE file for more details.

Background

And-Inverter Graphs (AIGs) are a convenient and compact representation for circuits. AIGs can be used to describe combinational and sequential circuits. We also plan to use it to formulate structural SAT and model checking problems. A more detailed description can be found in the report on the FORMAT.

Old Versions

[ tip-aig.tar.gz ]