• Top
  • Documentation
  • Books
  • Boolean-reasoning
    • Ipasir
    • Aignet
      • Base-api
      • Aignet-construction
      • Representation
      • Aignet-copy-init
      • Aignet-simplify-with-tracking
      • Aignet-simplify-marked-with-tracking
      • Aignet-cnf
      • Aignet-simplify-marked
      • Aignet-complete-copy
      • Aignet-transforms
      • Aignet-eval
        • Vector-simulation
          • Aignet-vecsim
          • Aignet-vecsim1
          • S32v
          • Random-sim
          • Exhaustive-sim
          • S32v-randomize-inputs
          • S32v-randomize-regs
          • Aignet-vecsim-top
      • Semantics
      • Aignet-read-aiger
      • Aignet-write-aiger
      • Aignet-abc-interface
      • Utilities
    • Aig
    • Satlink
    • Truth
    • Ubdds
    • Bdd
    • Faig
    • Bed
    • 4v
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Vector-simulation

Aignet-vecsim

Simulate an AIG on N*32 parallel input vectors.

This takes an s32v that has at least one row (see s32v-nrows) for each fanin node of the AIG and is seeded with combinational input values. This function sweeps over the AIG to compute all other fanin values given those inputs. After this, the Kth bit of the Nth row of the s32v will equal the id-eval of the AIG under the inputs/registers computed by collecting the Kth bit of the rows corresponding to input and register nodes.

If you want to simulate only one 32-bit set of values at a time, it is faster and logically equivalent to use aignet-vecsim1 or aignet-vecsim-top (which logically equals aignet-vecsim but uses aignet-vecsim1 when the input s32v is one column wide).

The combinational inputs of the AIG must have values already set in the s32v before starting. You may initialize them to random values using s32v-randomize-inputs and s32v-randomize-regs.

Exhaustive-sim wraps aignet-vecsim and performs an exhaustive simulation to find whether there is any input setting that results in the 0th output producing 1; i.e. whether the 0th output is satisfiable.

Definitions and Theorems

Function: aignet-vecsim-step$inline

(defun aignet-vecsim-step$inline (n s32v aignet)
  (declare (type (integer 0 *) n)
           (ignorable n s32v aignet))
  (declare (xargs :stobjs (s32v aignet)
                  :guard (<= (num-fanins aignet)
                             (s32v-nrows s32v))))
  (declare (xargs :guard (and (<= 0 n)
                              (< n (num-fanins aignet))
                              t)))
  (b* ((n (lnfix n))
       (nid n)
       (slot0 (id->slot nid 0 aignet))
       (type (snode->type slot0)))
    (aignet-case type :gate
                 (b* ((f0 (snode->fanin slot0))
                      (slot1 (id->slot nid 1 aignet))
                      (f1 (snode->fanin slot1)))
                   (if (eql 1 (snode->regp slot1))
                       (s32v-xor-lits f0 f1 nid s32v)
                     (s32v-and-lits f0 f1 nid s32v)))
                 :const (s32v-zero nid s32v)
                 :in s32v)))

Function: aignet-vecsim-tailrec

(defun aignet-vecsim-tailrec (n s32v aignet)
  (declare (type (integer 0 *) n))
  (declare (xargs :stobjs (s32v aignet)
                  :guard (<= (num-fanins aignet)
                             (s32v-nrows s32v))))
  (declare (xargs :guard (and (<= 0 n)
                              (<= n (num-fanins aignet))
                              t)))
  (b*
    (((when (mbe :logic (zp (- (ifix (num-fanins aignet)) (ifix n)))
                 :exec (int= (num-fanins aignet) n)))
      s32v)
     (n (lifix n))
     (s32v (aignet-vecsim-step n s32v aignet)))
    (aignet-vecsim-tailrec (1+ n)
                           s32v aignet)))

Function: aignet-vecsim-iter

(defun aignet-vecsim-iter (n s32v aignet)
  (declare (type (integer 0 *) n))
  (declare (xargs :stobjs (s32v aignet)
                  :guard (<= (num-fanins aignet)
                             (s32v-nrows s32v))))
  (declare (xargs :guard (and (<= 0 n)
                              (<= n (num-fanins aignet))
                              t)))
  (b* (((when (mbe :logic (zp n) :exec (int= 0 n)))
        s32v)
       (n (1- (lifix n)))
       (s32v (aignet-vecsim-iter n s32v aignet)))
    (aignet-vecsim-step n s32v aignet)))

Theorem: aignet-vecsim-iter-of-ifix-n

(defthm aignet-vecsim-iter-of-ifix-n
  (equal (aignet-vecsim-iter (ifix n)
                             s32v aignet)
         (aignet-vecsim-iter n s32v aignet)))

Theorem: aignet-vecsim-iter-int-equiv-congruence-on-n

(defthm aignet-vecsim-iter-int-equiv-congruence-on-n
  (implies (int-equiv n n-equiv)
           (equal (aignet-vecsim-iter n s32v aignet)
                  (aignet-vecsim-iter n-equiv s32v aignet)))
  :rule-classes :congruence)

Theorem: aignet-vecsim-tailrec-is-aignet-vecsim-iter

(defthm aignet-vecsim-tailrec-is-aignet-vecsim-iter
  (equal (aignet-vecsim-tailrec 0 s32v aignet)
         (aignet-vecsim-iter (num-fanins aignet)
                             s32v aignet)))

Function: aignet-vecsim$inline

(defun aignet-vecsim$inline (s32v aignet)
  (declare (xargs :stobjs (s32v aignet)
                  :guard (<= (num-fanins aignet)
                             (s32v-nrows s32v))))
  (declare (xargs :guard t))
  (b* nil
    (mbe :logic (aignet-vecsim-iter (num-fanins aignet)
                                    s32v aignet)
         :exec (aignet-vecsim-tailrec 0 s32v aignet))))

Theorem: car-nonnil-forward-to-consp

(defthm car-nonnil-forward-to-consp
  (implies (car x) (consp x))
  :rule-classes :forward-chaining)

Theorem: memo-tablep-aignet-vecsim-iter

(defthm memo-tablep-aignet-vecsim-iter
 (implies
  (< (fanin-count aignet)
     (len (stobjs::2darr->rows s32v)))
  (<
    (fanin-count aignet)
    (len (stobjs::2darr->rows (aignet-vecsim-iter n s32v aignet)))))
 :rule-classes :linear)

Theorem: aignet-vecsim-iter-lookup-prev

(defthm aignet-vecsim-iter-lookup-prev
 (implies
  (<= (nfix n) (nfix m))
  (equal
   (nth
     slot
     (nth m
          (stobjs::2darr->rows (aignet-vecsim-iter n s32v aignet))))
   (nth slot
        (nth m (stobjs::2darr->rows s32v))))))

Theorem: ncols-of-aignet-vecsim-iter

(defthm ncols-of-aignet-vecsim-iter
  (equal (stobjs::2darr->ncols (aignet-vecsim-iter n s32v aignet))
         (stobjs::2darr->ncols s32v)))

Theorem: nrows-of-aignet-vecsim-iter

(defthm nrows-of-aignet-vecsim-iter
 (implies
  (<= n (len (stobjs::2darr->rows s32v)))
  (equal
      (len (stobjs::2darr->rows (aignet-vecsim-iter n s32v aignet)))
      (len (stobjs::2darr->rows s32v)))))

Theorem: nth-in-aignet-vecsim-iter-preserved

(defthm nth-in-aignet-vecsim-iter-preserved
 (implies
  (and (< (nfix m) (nfix n))
       (equal nm (1+ (nfix m)))
       (syntaxp (not (equal n nm))))
  (equal
   (nth
     slot
     (nth m
          (stobjs::2darr->rows (aignet-vecsim-iter n vals aignet))))
   (nth
    slot
    (nth
      m
      (stobjs::2darr->rows (aignet-vecsim-iter nm vals aignet)))))))

Theorem: aignet-vecsim-iter-correct

(defthm aignet-vecsim-iter-correct
 (implies
  (and (aignet-idp m aignet)
       (< (nfix m) (nfix n))
       (< (nfix slot) (s32v-ncols s32v)))
  (equal
   (logbit
    bit
    (s32-fix
     (nth
      slot
      (nth
        m
        (stobjs::2darr->rows (aignet-vecsim-iter n s32v aignet))))))
   (let* ((vals (vecsim-to-eval slot bit s32v vals aignet))
          (in-vals (aignet-vals->invals nil vals aignet))
          (reg-vals (aignet-vals->regvals nil vals aignet)))
     (id-eval m in-vals reg-vals aignet)))))

Theorem: aignet-vecsim-correct

(defthm aignet-vecsim-correct
 (implies
  (and (aignet-idp m aignet)
       (< (nfix slot) (s32v-ncols s32v)))
  (equal
   (logbit
    bit
    (s32-fix
     (nth slot
          (nth m
               (stobjs::2darr->rows (aignet-vecsim s32v aignet))))))
   (let* ((vals (vecsim-to-eval slot bit s32v vals aignet))
          (in-vals (aignet-vals->invals nil vals aignet))
          (reg-vals (aignet-vals->regvals nil vals aignet)))
     (id-eval m in-vals reg-vals aignet)))))

Theorem: aignet-eval-iter-out-of-bounds

(defthm aignet-eval-iter-out-of-bounds
  (implies (<= (nfix n) (nfix m))
           (equal (nth m (aignet-eval-iter n vals aignet))
                  (nth m vals))))

Theorem: aignet-eval-out-of-bounds

(defthm aignet-eval-out-of-bounds
  (implies (< (fanin-count aignet) (nfix m))
           (equal (nth m (aignet-eval vals aignet))
                  (nth m vals))))

Theorem: aignet-vecsim-to-eval-lemma

(defthm aignet-vecsim-to-eval-lemma
 (implies
   (< (nfix slot) (s32v-ncols s32v))
   (bit-equiv
        (nth id
             (vecsim-to-eval slot bit (aignet-vecsim s32v aignet)
                             vals aignet))
        (nth id
             (aignet-eval (vecsim-to-eval slot bit s32v vals aignet)
                          aignet)))))

Theorem: aignet-vecsim-to-eval

(defthm aignet-vecsim-to-eval
  (implies
       (< (nfix slot) (s32v-ncols s32v))
       (bits-equiv
            (vecsim-to-eval slot bit (aignet-vecsim s32v aignet)
                            vals aignet)
            (aignet-eval (vecsim-to-eval slot bit s32v vals aignet)
                         aignet))))