• 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

S32v-randomize-regs

Assign random values to the register nodes of an AIG in an s32v

Signature

(s32v-randomize-regs n s32v aignet state) 
  → 
(mv new-s32v new-state)

Arguments

n — start at 0.
    Guard (natp n).

Definitions and Theorems

Function: s32v-randomize-regs

(defun s32v-randomize-regs (n s32v aignet state)
  (declare (xargs :stobjs (s32v aignet state)))
  (declare (xargs :guard (natp n)))
  (declare (xargs :guard (and (<= n (num-regs aignet))
                              (<= (num-fanins aignet)
                                  (s32v-nrows s32v)))))
  (let ((__function__ 's32v-randomize-regs))
    (declare (ignorable __function__))
    (if (mbe :logic (zp (- (num-regs aignet) (nfix n)))
             :exec (eql n (num-regs aignet)))
        (mv s32v state)
      (b* (((mv s32v state)
            (s32v-randomize (regnum->id n aignet)
                            s32v state)))
        (s32v-randomize-regs (1+ (lnfix n))
                             s32v aignet state)))))

Theorem: ncols-of-s32v-randomize-regs

(defthm ncols-of-s32v-randomize-regs
  (b* (((mv ?new-s32v ?new-state)
        (s32v-randomize-regs n s32v aignet state)))
    (equal (stobjs::2darr->ncols new-s32v)
           (stobjs::2darr->ncols s32v))))

Theorem: nrows-of-s32v-randomize-regs

(defthm nrows-of-s32v-randomize-regs
  (b* (((mv ?new-s32v ?new-state)
        (s32v-randomize-regs n s32v aignet state)))
    (implies (< (fanin-count aignet)
                (len (stobjs::2darr->rows s32v)))
             (equal (len (stobjs::2darr->rows new-s32v))
                    (len (stobjs::2darr->rows s32v))))))

Theorem: w-state-of-s32v-randomize-regs

(defthm w-state-of-s32v-randomize-regs
  (equal (w (mv-nth 1
                    (s32v-randomize-regs n s32v aignet state)))
         (w state)))

Theorem: s32v-randomize-regs-of-nfix-n

(defthm s32v-randomize-regs-of-nfix-n
  (equal (s32v-randomize-regs (nfix n)
                              s32v aignet state)
         (s32v-randomize-regs n s32v aignet state)))

Theorem: s32v-randomize-regs-nat-equiv-congruence-on-n

(defthm s32v-randomize-regs-nat-equiv-congruence-on-n
  (implies (nat-equiv n n-equiv)
           (equal (s32v-randomize-regs n s32v aignet state)
                  (s32v-randomize-regs n-equiv s32v aignet state)))
  :rule-classes :congruence)