An efficient, stobj-based And-Inverter Graph (AIG) representation for Boolean functions and finite-state machines.

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 + registersCombinational 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, found in **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

Our focus on efficiency makes Aignet more difficult to work with and reason
about than the simpler

- Jared Davis and Sol Swords. Verified AIG Algorithms in ACL2. ACL2 Workshop 2013. May, 2013. EPTCS 114. Pages 95-110.

- 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.