Representation
Logical representation of the AIG network.
We now describe the logical view of the aignet stobj. This
representation serves as the foundation for reasoning about AIG algorithms and
provides the logical basis for the base-api.
Note that these definitions are used for reasoning but typically do not get
run. For details about the executable representation, see aignet-impl
instead, but most users should not need to think about those details.
The AIG Network
Logically, aignet is simply a list of nodes, where a node is of one of
five types distinguished by a particular symbol in its CAR, called its sequential-type or stype. Depending on its stype, a node contains 0 or
more fields that encode the and-inverter graph. We will discuss the meanings
of these fields later:
| Node Kind | Representation |
|---|
| Primary input | (:pi) |
| Register | (:reg) |
| AND gate | (:gate fanin0 fanin1) |
| Next state | (:nxst fanin regnum) |
| Primary output | (:po fanin) |
There is one other stype, :const, but generally no node in the list
actually has constant type; instead, the end of the list implicitly contains a
constant node.
Logically, an aignet is constructed by simply consing new nodes onto
it. A newly-created or cleared aignet is just nil, and contains only
the implicit constant node.
Node IDs and Node Lookups
We divide the set of nodes into fanin nodes and (combinational)
outputs. Next-state and primary output nodes are outputs, and all other
kinds are fanin nodes. The function fanin-node-p discriminates between
these two subsets.
Each fanin node has an ID, numbered sequentially with the unique constant
node having ID 0. The function fanin-count counts the number of fanin
nodes in a node list. To look up a node by ID, we use the function
(lookup-id n aignet), which returns the unique suffix of the aignet
whose car is a fanin node and which has fanin-count n. If
n is greater than the fanin count of the network, then it returns
nil:
Function: lookup-id
(defun lookup-id (id aignet)
(declare (xargs :guard (and (natp id) (node-listp aignet))))
(let ((__function__ 'lookup-id))
(declare (ignorable __function__))
(cond ((endp aignet) (node-list-fix aignet))
((and (fanin-node-p (car aignet))
(equal (fanin-count aignet) (lnfix id)))
(node-list-fix aignet))
(t (lookup-id id (cdr aignet))))))
Note that although this looks like a quadratic algorithm, it doesn't matter
because this is never actually executed. Real ID lookups are carried out by
array accesses.
Nodes can also be looked up by stype. The function (stype-count stype
aignet) returns the number of nodes of the given stype, and analogous to
lookup-id, (lookup-stype n stype aignet) returns the unique suffix of
the node list whose car is of the given stype and whose cdr has
stype-count n. (Note: we take the cdr here and not in lookup-id
because fanin-count is off by 1 in that it doesn't count the unique
constant node that is at index 0. That is, (lookup-id 0 aignet) is
supposed to return nil, whereas (lookup-stype 0 :reg aignet) is supposed
to return the suffix containing the 0th :reg node.)
Function: lookup-stype
(defun lookup-stype (n stype aignet)
(declare (xargs :guard (and (natp n)
(stypep stype)
(node-listp aignet))))
(let ((__function__ 'lookup-stype))
(declare (ignorable __function__))
(cond ((endp aignet) (node-list-fix aignet))
((and (equal (stype (car aignet))
(stype-fix stype))
(equal (stype-count stype (cdr aignet))
(lnfix n)))
(node-list-fix aignet))
(t (lookup-stype n stype (cdr aignet))))))
Node Operations, Fanins, Register IDs
Gate, next state, and primary output nodes have some fields:
- A gate has two fanins (representing the inputs to the AND gate),
- A primary output or next-state has one fanin (the function of the output or next-state), and
- A next-state also contains the register number of the corresponding register node.
The fanins are literals, which combine a node ID with a negation flag
as a single natural number: (+ (* 2 id) neg), where neg is 1 or 0.
There are many functions for constructing and accessing the various kinds of
nodes. See node for a reference. Note that these node-related
functions are not meant to be executed; they exist only for reasoning.
Lowest-Level API
The functions described above—fanin-count, lookup-id,
stype-count, lookup-stype and the
other functions for operating on logical nodes, e.g., the functions described
under node, provide the logical basis for reasoning about most kinds of
access to the aignet.
However, note that these functions are typically not used directly,
particularly for execution. Instead, see the wrappers that implement Aignet's
base-api.
Subtopics
- Aignet-impl
- Implementation details of Aignet's representation for execution.
Since these details are hidden, most users can safely skip this section.
- Node
- Type of an AIG node in an aignet object, logically.
- Network
- Reference guide for basic functions for working with the AIG network,
i.e., a list of nodes.
- Combinational-type
- Combinational type of a logical AIG node.
- Typecode
- Numeric encoding of a combinational-type keyword.
- Stypep
- Sequential type of a logical AIG node.
