		Search-engine friendly clone of the ACL2 documentation.

Aignet

Semantics

The precise combinational and sequential semantics of Aignet networks, and also definitions of certain kinds of AIG network equivalence.

The combinational semantics of aignets is given by the function ID-EVAL. This takes an aignet, a node ID, and assignments to the primary inputs and registers, and produces the value of that ID under those assignments.

The sequential semantics of aignets is given by the function LIT-EVAL-SEQ. This takes an aignet, a time frame number, a literal, a 2D bit array assigning values to the primary inputs on each frame, and an initial assignment to the registers. It produces the value of that literal under those sequential assignments.

The following theorem describes lit-eval-seq in terms of combinational evaluation:

Theorem: lit-eval-seq-in-terms-of-lit-eval

(defthm lit-eval-seq-in-terms-of-lit-eval
  (equal (lit-eval-seq k lit frames initsts aignet)
         (lit-eval lit (nth k (stobjs::2darr->rows frames))
                   (frame-regvals k frames initsts aignet)
                   aignet)))

Here, frame-regvals is a function that creates a register value array from the previous frame's sequential evaluations of the next-state nodes corresponding to each register. That is, to get the value of a literal at a particular timeframe, first evaluate the register next-states at the previous timeframe, then combinationally evaluate the literal with the resulting register values and the current frame's input values.

Subtopics

Comb-equiv: Combinational equivalence of aignets
Seq-equiv: Sequential equivalence of aignets
Seq-equiv-init: Sequential equivalence of aignets on a particular initial state
Invals: Bit array for the primary inputs to an aignet.
Outs-comb-equiv: Combinational equivalence of aignets, considering only primary outputs
Nxsts-comb-equiv: Combinational equivalence of aignets, considering only next-states