Skip to content
STIMSMITH

AIGER

Concept WIKI v1 · 7/6/2026

AIGER is a formal hardware description language that represents hardware systems at the bit level using and-inverter graphs (AIGs). It is commonly used as a gate-level netlist format in logic synthesis, as a benchmark format for safety specifications in reactive synthesis competitions, and as an output backend of the Yosys synthesis toolchain.

Overview

AIGER is a formal language used to describe hardware systems at the bit level. According to the µArchiFI paper (Tollec et al., 2023), AIGER describes hardware systems using an and-inverter graph [1]. This makes AIGER a foundational format for representing combinational and sequential digital circuits in a compact, canonical form.

Role in Logic Synthesis

AIGER is used as a gate-level netlist format in logic synthesis applications. The paper "An Automated Testing and Debugging Toolkit for Gate-Level Logic Synthesis Applications" (arXiv:2207.13487) highlights AIGER as one of the specialized formats targeted by gate-level netlist tools, with fuzzer and testcase-minimization tooling built around it for logic synthesis applications such as mockturtle, ABC, and LSOracle [arXiv:2207.13487].

Role in Reactive Synthesis Competitions

AIGER serves as the standard benchmark format for safety specifications in the International Competition on Reactive Synthesis (SYNTCOMP). The SYNTCOMP 2016 report (arXiv:1609.00507) describes how the competition uses an AIGER-based format alongside the newer LTL-based temporal logic synthesis format (TLSF). In that edition, 6 tools entered the AIGER-based track [arXiv:1609.00507].

AIGER in the Yosys Toolchain

AIGER is supported as a backend output of the Yosys open-source synthesis framework. The µArchiFI paper notes that "supported formal languages are AIGER, SMV, BTOR2 and SMT-LIB," where:

  • AIGER — describes hardware systems at the bit level using an and-inverter graph.
  • SMV — provided by the symbolic model checker NUXMV; describes finite and infinite transition systems at the word level with data types like bit vectors or memories.
  • BTOR2 — a word-level generalization of AIGER, providing word-level data types, registers, and memories.
  • SMT-LIB — the standard specification for SMT problems, also able to describe hardware transition systems [1].

This positions AIGER as the bit-level baseline in a family of progressively more expressive formats, with BTOR2 lifting AIGER to the word level and SMT-LIB providing a general-purpose alternative.

See Also

  • Yosys — open-source synthesis tool whose backend emits AIGER among other formal languages.
  • BTOR2 — word-level generalization of AIGER.
  • SYNTCOMP — reactive synthesis competition that uses AIGER for its safety-specification track.

LINKED ENTITIES

1 links
Yosys USES

CITATIONS

5 sources
5 citations
[1] AIGER describes hardware systems at the bit level using an and-inverter graph. µArchiFI: Formal Modeling and Verification Strategies for Microarchitectural Fault Injections
[2] AIGER is one of the formal languages supported as a backend output of the Yosys open-source synthesis framework, alongside SMV, BTOR2, and SMT-LIB. µArchiFI: Formal Modeling and Verification Strategies for Microarchitectural Fault Injections
[3] BTOR2 is a word-level generalization of AIGER providing word-level data types, registers, and memories. µArchiFI: Formal Modeling and Verification Strategies for Microarchitectural Fault Injections
[4] AIGER is a gate-level netlist format used in logic synthesis, and is targeted by specialized fuzz testing and delta debugging toolkits. An Automated Testing and Debugging Toolkit for Gate-Level Logic Synthesis Applications
[5] AIGER-based format is used in SYNTCOMP for safety specifications, with the SYNTCOMP 2016 edition having 6 tools in the AIGER-based track. The 3rd Reactive Synthesis Competition (SYNTCOMP 2016): Benchmarks, Participants & Results