Aignet-construction
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" AIGNET stobj or else create a local one using
with-local-stobj.
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 STRASH stobj, which again may either
be the live one or one created locally.
Basic Low-level Construction Functions
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).
Aignet-construction functions
(aignet-add-in aignet) adds a new primary input node to the network and
returns (mv lit aignet), where lit is the non-negated literal of
the new node.
(aignet-add-reg aignet) adds a new register output node to the network and
returns (mv lit aignet), where lit is the non-negated literal of
the new node.
(aignet-add-and lit1 lit2 aignet) adds to the network a new AND node
conjoining 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
aignet-litp (which is true of any literal returned by a node construction
function, or its negation). Note: this function does not do structural
hashing -- for that, see below.
(aignet-add-xor lit1 lit2 aignet) is similar to aignet-add-and,
but makes an XOR node rather than an AND. It also does not to structural
hashing.
(aignet-add-out lit aignet) adds to the network a new primary output with
fanin 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 aignet-litp.
(aignet-set-nxst lit ro aignet) adds to the network a new register input
with fanin lit, and connects it to a register output node whose ID is
ro. It returns aignet. lit must satisfy aignet-litp
and ro must be the ID of a register output node that is not yet
connected to a register input.
Hashing and Simplifying Constructor Functions
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
f1
and
f2 (for and/or/xor) and
c,
tb, and
fb
for mux (signifying condition, true-branch, and false-branch), possibly with
structural hashing and lightweight simplification. All return
(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.
aignet-build macro
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.
Subtopics
- 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-xor
- Add an XOR node to 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-or
- Implement an OR of two literals node in 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.
