• 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-vecsim1

Simulate an AIG on 32 parallel input vectors.

Definitions and Theorems

Function: aignet-vecsim1-step$inline

(defun aignet-vecsim1-step$inline (n s32v aignet)
 (declare (type (integer 0 *) n)
          (ignorable n s32v aignet))
 (declare (xargs :stobjs (s32v aignet)
                 :guard (and (<= (num-fanins aignet)
                                 (s32v-nrows s32v))
                             (equal (s32v-ncols s32v) 1))))
 (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)))
    (s32v-set
        n
        (if (eql 1 (snode->regp slot1))
            (logxor (bit-extend (b-xor (lit->neg f0) (lit->neg f1)))
                    (s32v-get (lit->var f0) s32v)
                    (s32v-get (lit->var f1) s32v))
          (logand (logxor (bit-extend (lit->neg f0))
                          (s32v-get (lit->var f0) s32v))
                  (logxor (bit-extend (lit->neg f1))
                          (s32v-get (lit->var f1) s32v))))
        s32v))
   :const (s32v-set n 0 s32v)
   :in s32v)))

Function: aignet-vecsim1-tailrec

(defun aignet-vecsim1-tailrec (n s32v aignet)
  (declare (type (integer 0 *) n))
  (declare (xargs :stobjs (s32v aignet)
                  :guard (and (<= (num-fanins aignet)
                                  (s32v-nrows s32v))
                              (equal (s32v-ncols s32v) 1))))
  (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-vecsim1-step n s32v aignet)))
    (aignet-vecsim1-tailrec (1+ n)
                            s32v aignet)))

Function: aignet-vecsim1-iter

(defun aignet-vecsim1-iter (n s32v aignet)
  (declare (type (integer 0 *) n))
  (declare (xargs :stobjs (s32v aignet)
                  :guard (and (<= (num-fanins aignet)
                                  (s32v-nrows s32v))
                              (equal (s32v-ncols s32v) 1))))
  (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-vecsim1-iter n s32v aignet)))
    (aignet-vecsim1-step n s32v aignet)))

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

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

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

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

Theorem: aignet-vecsim1-tailrec-is-aignet-vecsim1-iter

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

Function: aignet-vecsim1$inline

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

Theorem: aignet-vecsim1-iter-is-aignet-vecsim-iter

(defthm aignet-vecsim1-iter-is-aignet-vecsim-iter
  (implies (equal (s32v-ncols s32v) 1)
           (equal (aignet-vecsim1-iter n s32v aignet)
                  (aignet-vecsim-iter n s32v aignet))))

Theorem: aignet-vecsim1-is-aignet-vecsim

(defthm aignet-vecsim1-is-aignet-vecsim
  (implies (equal (s32v-ncols s32v) 1)
           (equal (aignet-vecsim1 s32v aignet)
                  (aignet-vecsim s32v aignet))))