AIGER

Introduction

AIGER is a format, library and set of utilities for And-Inverter Graphs (AIGs). The FORMAT report serves as reference manual and tutorial.

News

The maintenance release 20071012 fixes many minor glitches.

The translator 'smvtoaig' now accepts 'next' operators in 'DEFINE' sections.

The simulator 'aigsim' can now be used to check correctness of witnesses for structural SAT and model checking problems automatically.

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

We have put a small set of simple and easy to solve structural SAT instances online.

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

Recent versions allow a flow from a sequential AIGER model to CNF and back. This is implemented in a shell script 'mc.sh' and uses the format for witnesses respectively counter examples as defined in the a FORMAT report. The new versions since 20061128 just include minor fixes.

In the previous version we already fixed some minor defects, added a delta debugger, a bounded model checker and last but not least a simple AIG library 'SimpAIG'. See the NEWS file for more details. The README file describes the contents of the archive.

Benchmarks

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.

In the new version of this benchmark set we used the recently fixed 'smvtoaig' utility and kept symbol tables.

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 ]