		Search-engine friendly clone of the ACL2 documentation.

Aignet

Aignet-eval

Evaluating AIGNET networks

The (combinational) semantics of an AIGNET network is given by the function

(lit-eval lit invals regvals aignet).

Invals and regvals are bit arrays containing a value for each (respectively) primary input and register node in the network. But because this function is a simple recursive specification for the semantics of a node and not written for performance, it is likely to perform badly (worst-case exponential time in the size of the network).

To actually execute evaluations of nodes, instead do the following:

(b* ((vals ;; Resize vals to have one bit for each aignet node.
      (resize-bits (num-fanins aignet) vals))
     (vals ;; Copy primary input values from invals into vals.
      (aignet-invals->vals invals vals aignet))
     (vals ;; Copy register values from regvals into vals.
      (aignet-regvals->vals regvals vals aignet))
     (vals ;; Record the evaluations of all other nodes in vals.
      (aignet-eval vals aignet))
     (lit-value1 ;; Look up the value of a particular literal of interest.
      (aignet-eval-lit lit1 vals))
     (lit-value2 ;; Look up another literal.
      (aignet-eval-lit lit2 vals)))
 ...)

(Note: invals and regvals have a different layout than vals; they include only one entry per (respectively) primary input or register instead of one entry per node, so they are indexed by I/O number whereas vals is indexed by node ID.)

The following theorem shows the correspondence between a literal looked up in vals after running aignet-eval and the lit-eval of that literal:

Theorem: aignet-eval-lit-of-aignet-eval

(defthm aignet-eval-lit-of-aignet-eval
  (implies (aignet-idp (lit-id lit) aignet)
           (equal (aignet-eval-lit lit (aignet-eval vals aignet))
                  (lit-eval lit
                            (aignet-vals->invals nil vals aignet)
                            (aignet-vals->regvals nil vals aignet)
                            aignet))))

These theorems resolve the copying between invals/regvals and vals:

Theorem: aignet-vals->invals-of-aignet-invals->vals

(defthm aignet-vals->invals-of-aignet-invals->vals
  (bits-equiv
       (aignet-vals->invals invals1
                            (aignet-invals->vals invals vals aignet)
                            aignet)
       (set-prefix (num-ins aignet)
                   invals invals1)))

Theorem: aignet-vals->invals-of-aignet-regvals->vals

(defthm aignet-vals->invals-of-aignet-regvals->vals
 (bits-equiv
     (aignet-vals->invals invals1
                          (aignet-regvals->vals regvals vals aignet)
                          aignet)
     (aignet-vals->invals invals1 vals aignet)))

Theorem: aignet-vals->regvals-of-aignet-regvals->vals

(defthm aignet-vals->regvals-of-aignet-regvals->vals
 (bits-equiv
    (aignet-vals->regvals regvals1
                          (aignet-regvals->vals regvals vals aignet)
                          aignet)
    (set-prefix (num-regs aignet)
                regvals regvals1)))

Theorem: aignet-vals->regvals-of-aignet-invals->vals

(defthm aignet-vals->regvals-of-aignet-invals->vals
 (bits-equiv
      (aignet-vals->regvals regvals1
                            (aignet-invals->vals invals vals aignet)
                            aignet)
      (aignet-vals->regvals regvals1 vals aignet)))

For higher-level functions for simulation, see the book "aig-sim.lisp".

Subtopics

Vector-simulation: Simulating the network by running many tests in parallel using vector logic operations