		Search-engine friendly clone of the ACL2 documentation.

Aignet

Base-api

Lowest-level functions for working with the aignet stobj.

Quick Guide

Initialization

aignet-clear clears the network without resizing.
aignet-init clears the network and resize arrays.

Network construction

aignet-add-in adds a primary input
aignet-add-out adds a primary output
aignet-add-and adds an and gate
aignet-add-xor adds an xor gate
aignet-add-reg adds a register
aignet-set-nxst sets the next-state formula for a register.

Network size

num-fanins returns the number of nodes in the network
num-ins returns the number of primary inputs
num-outs returns the number of primary outputs
num-gates returns the number of gates
num-regs returns the number of register nodes
num-nxsts returns the number of times any register's next-state as been set

To see whether a node ID is in bounds use (id-existsp id aignet); this is the same as (< (nfix id) (num-fanins aignet)).

General node queries

id->type looks up the type of some node -- constant (0), gate (1), input (2), or output (3)
id->regp gets the register/xor bit for a node id, which distinguishes between types of gate (1 for XORs, 0 for ANDs), combinational input (1 for registers, 0 for primary inputs), and combinational output (1 for next-state, 0 for primary output).
id->phase gets the value of this node in the all-0 evaluation.
gate-id->fanin0 gets the 0th fanin literal from an AND or XOR gate
gate-id->fanin1 gets the 1st fanin literal from an AND or XOR gate.
ci-id->ionum gets the PI or register number given a PI or register node ID.

All of the above fields are in fact stored in two 32-bit array entries. Instead of repeatedly querying these, it may be more efficient to grab one or both entries and use field accessors to get these values. The array slot accessors are id->slot0 and id->slot1, and the accessors are as follows:

(snode->type (id->slot0 id aignet)) is the same as (id->type id aignet)
(snode->regp (id->slot1 id aignet)) is the same as (id->regp id aignet)
(snode->phase (id->slot1 id aignet)) is the same as (id->phase id aignet)
(snode->fanin (id->slot0 id aignet)) is the same as (gate-id->fanin0 id aignet)
(snode->fanin (id->slot1 id aignet)) is the same as (gate-id->fanin1 id aignet)
(snode->ionum (id->slot1 id aignet)) is the same as (ci-id->ionum id aignet)
(snode->fanin (id->slot0 id aignet)) is the same as (regnum->nxst n aignet) if id is (regnum->id id aignet).

Name mappings

innum->id looks up the node id for the nth primary input
regnum->id looks up the node id for the nth register
regnum->nxst gets the next-state literal associated with a register
outnum->fanin gets the output literal for a given PO number.

Misc

Subtopics

Aignet-case: Macro for node type case splits.
Aignet-init: (aignet-init max-outs max-regs max-ins max-nodes aignet) clears the aignet, setting the arrays to the given sizes.
Aignet-add-xor: (aignet-add-xor f0 f1 aignet) adds an new XOR gate node to the aignet with the given fanin literals.
Aignet-add-and: (aignet-add-and f0 f1 aignet) adds an new AND gate node to the aignet with the given fanin literals.
Ci-id->ionum: (ci-id->ionum id aignet) gets the input or register number of the node whose ID is id.
Literal: See litp.
Gate-id->fanin1: (gate-id->fanin1 id aignet) gets the 1st fanin literal of the AND gate node whose ID is id.
Gate-id->fanin0: (gate-id->fanin0 id aignet) gets the 0th fanin literal of the AND gate node whose ID is id.
Aignet-set-nxst: (aignet-set-nxst f reg aignet) adds a next-state node to the aignet.
Aignet-clear: (aignet-clear aignet) clears the aignet, essentially without resizing its arrays.
Aignet-add-out: (aignet-add-out f aignet) adds a primary output node to the aignet.
Regnum->nxst: (regnum->nxst reg aignet) gets the next-state literal for register number reg.
Id->slot1: (id->slot1 id aignet) fetches the slot0 data for the given node from the fanin node array.
Id->phase: (id->phase id aignet) computes the value of the node under the all-0 simulation.
Num-regs: (num-regs aignet) returns the number of register nodes in an aignet.
Num-ins: (num-ins aignet) returns the number of primary input nodes in an aignet.
Num-fanins: (num-fanins aignet) returns the total number of nodes in an aignet.
Id->slot0: (id->slot0 id aignet) fetches the slot0 data for the given node from the fanin node array.
Regnum->id: (regnum->id n aignet) gets the ID of the node with register number n.
Id->type: (id->type id aignet) gets the type code of the node with ID id.
Id->regp: (id->regp id aignet) gets the register bit from the node with ID id.
Outnum->fanin: (outnum->fanin n aignet) gets the fanin literal of primary output number n.
Innum->id: (innum->id n aignet) gets the ID of the node with primary input number n.
Id-existsp: (id-existsp id aignet) checks whether an ID is in bounds for an aignet.
Aignet-add-reg: (aignet-add-reg aignet) adds a new register node to the aignet.
Aignet-add-in: (aignet-add-in aignet) adds a new primary input node to the aignet.
Aignet-rollback: (aignet-rollback n aignet) rewinds the aignet so that node n is the last node.
Num-outs: (num-outs aignet) returns the number of primary output nodes in an aignet.
Num-nxsts: (num-nxsts aignet) returns the number of next-state nodes in an aignet.
Num-gates: (num-gates aignet) returns the number of AND gate nodes in an aignet.
Fanin-litp: (fanin-litp x aignet) checks whether a literal is appropriate as a fanin to another node.