AIGER is a format, library and set of utilities for And-Inverter Graphs (AIGs).
We are working on a new version. The differences are described in the following draft. The old FORMAT report still serves as reference manual and tutorial for all inherited features from older versions.
New BEEM benchmarks.
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.
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.
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
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
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
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.
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.
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.
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.
[ aiger-20060915.zip | aiger-20061005.zip | aiger-20061011.zip | aiger-20061016.zip | aiger-20061115.zip | aiger-20061128.zip | aiger-20061129.zip | aiger-20070308.zip | aiger-20070427.zip ] aiger-1.9.3.tar.gz ]
[ tip-aig.tar.gz ]