How to construct an AIGNET network.

An AIGNET network is constructed by adding nodes in topological order: that is, an AND gate cannot be added until its two fanins are created, and a combinational output cannot be added until its fanin exists. Additionally, a register input cannot be added until its corresponding register output exists.

First, because an AIGNET network is represented in a stobj, you must either
work on the "live"

Usually when constructing an AIG network one wants to structurally hash the
AND nodes, so as to avoid creating duplicate nodes with identical structure.
To do this, you additionally need a

To initialize a new network or clear an existing one, use:

(aignet-clear aignet)or, to allocate a certain amount of space in order to avoid resizing arrays,

(aignet-init output-cap reg-cap input-cap node-cap aignet).

To initialize a strash object or clear an existing one, use:

(strashtab-clear strash)or to allocate a certain amount of space to avoid resizing the hash table,

(strashtab-init node-cap nil nil strash).

`(mv lit aignet)`, where `lit` is the non-negated literal of
the new node.

`(mv lit aignet)`, where `lit` is the non-negated literal of
the new node.

`lit1` and `lit2`, and returns `(mv lit aignet)`,
where `lit` is the non-negated literal of the new node. `lit1`
and `lit2` must be literals of the network, satisfying

`lit`, and returns `aignet`. (It does not return a literal
because a combinational output node is not allowed to be the fanin to another
node.) `lit` must satisfy

`lit`, and connects it to a register output node whose ID is
`ro`. It returns `aignet`. `lit` must satisfy `ro` must be the ID of a register output node that is not yet
connected to a register input.

The following functions:

(aignet-hash-and f1 f2 gatesimp strash aignet) (aignet-hash-or f1 f2 gatesimp strash aignet) (aignet-hash-xor f1 f2 gatesimp strash aignet) (aignet-hash-iff f1 f2 gatesimp strash aignet) (aignet-hash-mux c tb fb gatesimp strash aignet)add nodes implementing the respective functions of input literals

(mv lit strash aignet).Gatesimp is a gatesimp object that specifies whether to structurally hash the nodes, what level of effort to use in Boolean simplification (between 0 and 4), and whether to use XOR nodes at all and if so whether to derive them from AND nodes. The levels of simplification correspond to the paper:

R. Brummayer and A. Biere. Local two-level And-Inverter Graph minimization without blowup. Proc. MEMCIS 6 (2006): 32-38,available here. These simplifications look at most one level deep at the fanins of each AND, that is, examining at most four fanin nodes. Usually at least level 1 is desirable; level 1 deals with ANDs of constants and identical and negated nodes. Practically, we think for most applications building the AIGs is not a performance bottleneck and level 3 or 4 can be used with some potential benefit and no noticeable slowdown.

See also aignet-build, a macro that lays out the calls necessary to build a nest of logic. This uses the structural hashing constructor functions.

- Gatesimp
- Structure encoding AIGNET construction settings for how much to try to simplify and whether to use hashing
- Aignet-hash-mux
- Implement an if-then-else of the given literals in an AIGNET, or find a node already representing the required logical expression.
- Aignet-hash-or
- Implement an OR of two literals node in an AIGNET, or find a node already representing the required logical expression.
- Aignet-hash-and
- Add an AND node to an AIGNET, or find a node already representing the required logical expression.
- Aignet-hash-xor
- Add an XOR node to an AIGNET, or find a node already representing the required logical expression.
- Aignet-hash-iff
- Implement an IFF of two literals node in an AIGNET, or find a node already representing the required logical expression.
- Aignet-build
- Macro that constructs a nested logical expression in an aignet
- Patbind-aignet-build
- B* binder to make a nest of logical functions in an aignet.