Aignet
An efficient, stobj-based And-Inverter Graph (AIG)
representation for Boolean functions and finite-state machines.
Background
At its most basic, an AIG is a DAG whose nodes are either AND/XOR gates,
outputs, inputs, or the unique constant node. Outputs have 1
descendant (fanin), ANDs/XORs have 2, and inputs have none. An edge may point
to gate, input, or constant, but not an output; we call gates, inputs, and
constants collectively "fanin nodes". Each edge has a Boolean attribute
signifying whether it is negated or not--thus we need only one constant node instead of one true and one false.
Such an AIG is combinational:
it represents a stateless circuit that produces outputs that are Boolean
functions of its inputs.
A sequential AIG extends this to directly model circuits with
internal state that responds to inputs that are changing over time. Here the
combinational input and outputs to the AIG are divided into two categories:
- Combinational inputs = primary inputs + registers
- Combinational outputs = primary outputs + register next-states
The sequential semantics for an AIG depend on an initial
state and a series of inputs:
- Initially, assign initial values to the register next-states.
- Every cycle:
- copy values from next-states to corresponding registers
- assign values to the primary inputs
- compute values of gates in topological order
- compute values of primary outputs and next states.
The Aignet Library
The Aignet library, found in centaur/aignet, is intended to provide an
efficient implementation of sequential AIGs.
We represent an AIG network as an abstract-stobj. This means that
the Common Lisp implementation and its logical story are substantially
different. This is true of concrete stobjs as well, where access/update
functions are logically defined in terms of nth and update-nth
but implemented as array accesses. But it is especially true for Aignet!
- Logically—for reasoning about the AIG network and proving AIG
algorithms are correct—the AIG network is viewed as just a list of
nodes. Understanding these definitions is a first step toward
successfully using Aignet; see representation.
- For execution, the AIG is actually represented with various stobj
arrays, largely styled after the ABC package. Since the
implementation is kept hidden, most users can feel free to skim or entirely
skip the details in aignet-impl.
The low-level base-api connects these logical and executable
definitions together, and provides the most basic operations for initializing
the network, adding nodes to it, inspecting the contents of the nodes, and so
on. The rest of Aignet is built on top of this API. Generally speaking,
accesses are implemented as constant-time, and updates as amortized
constant-time (since there may be array resizes).
BOZO describe the rest of the library
Comparison with Hons-AIGs
Our focus on efficiency makes Aignet more difficult to work with and reason
about than the simpler Hons-AIG library.
On the other hand, Aignet can sometimes be much faster than Hons-AIGs. For a
good introduction with a more detailed comparison of Hons-AIGs and Aignet,
see:
Subtopics
- Base-api
- Lowest-level functions for working with the aignet stobj.
- Aignet-construction
- How to construct an AIGNET network.
- Representation
- Logical representation of the AIG network.
- Aignet-copy-init
- Set the initial state of an FSM to the all-0 convention.
- Aignet-simplify-with-tracking
- Aignet-simplify-marked-with-tracking
- Aignet-cnf
- Discussion of CNF generation for aignets.
- Aignet-simplify-marked
- Aignet-complete-copy
- Copy an aignet, "normalizing" the order of nodes
- Aignet-transforms
- Various types of transforms preserving different properties of the AIG
- Aignet-eval
- Evaluating AIGNET networks
- Semantics
- The precise combinational and sequential semantics of Aignet
networks, and also definitions of certain kinds of AIG network equivalence.
- Aignet-read-aiger
- Read an aignet from a binary AIGER file.
- Aignet-write-aiger
- Write an aignet into a binary AIGER file.
- Aignet-abc-interface
- Using the open-source synthesis and equivalence/model-checking tool ABC with aignet
- Utilities
- Basic tools for using aignet networks.
