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
(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)))