• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Community
  • Proof-automation
  • ACL2
  • Macro-libraries
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
      • Svex-stvs
        • Svtv-data
        • Defsvtv$
        • Svtv-run
        • Defsvtv-phasewise
        • Svtv
        • Svtv-spec
        • Defsvtv
        • Process.lisp
        • Svtv-doc
        • Svtv-chase$
        • Svtv-versus-stv
        • Svtv-debug-fsm
        • Structure.lisp
        • Svtv-debug
          • Vcd.lisp
          • Debug.lisp
            • Svtv-debug-writephases
            • Svtv-debug-fsm-writephases
            • Svtv-debug-set-ios-logic
            • Svtv-debug-run-fsm
            • Svtv-debug-fsm-core
            • Svtv-debug-run-logic
            • Svtv-debug-init
            • Svtv-debug-eval-aliases-track
            • Svtv-debug-core
            • Svtv-debug-set-svtv
            • Svtv-debug-lhs-eval
            • Svtv-debug-eval-aliases
            • Svtv-debug-set-ios
            • Svtv-debug-run
            • Debugdata-status-p
        • Def-pipeline-thm
        • Expand.lisp
        • Def-cycle-thm
        • Svtv-utilities
        • Svtv-debug$
        • Defsvtv$-phasewise
      • Svex-decomposition-methodology
      • Sv-versus-esim
      • Svex-decomp
      • Svex-compose-dfs
      • Svex-compilation
      • Moddb
      • Svmods
      • Svstmt
      • Sv-tutorial
      • Expressions
      • Symbolic-test-vector
      • Vl-to-svex
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Debug.lisp

Svtv-debug-eval-aliases

Signature

(svtv-debug-eval-aliases n aliases wirevals vcd-vals) 
  → 
vcd-vals1

Arguments

n — Guard (natp n).

wirevals — Guard (svex-env-p wirevals).

Definitions and Theorems

Function: svtv-debug-eval-aliases

(defun svtv-debug-eval-aliases (n aliases wirevals vcd-vals)
 (declare (xargs :stobjs (aliases vcd-vals)))
 (declare (xargs :guard (and (natp n) (svex-env-p wirevals))))
 (declare (xargs :guard (and (<= n (aliass-length aliases))
                             (<= (aliass-length aliases)
                                 (4vecs-length vcd-vals)))))
 (let ((__function__ 'svtv-debug-eval-aliases))
   (declare (ignorable __function__))
   (b* (((when (mbe :logic (zp (- (aliass-length aliases) (nfix n)))
                    :exec (eql (aliass-length aliases) n)))
         vcd-vals)
        (lhs (get-alias n aliases))
        (val (svtv-debug-lhs-eval lhs n wirevals vcd-vals))
        (vcd-vals (set-4vec n val vcd-vals)))
     (svtv-debug-eval-aliases (1+ (lnfix n))
                              aliases wirevals vcd-vals))))

Theorem: len-vcd-vals-of-svtv-debug-eval-aliases

(defthm len-vcd-vals-of-svtv-debug-eval-aliases
  (<= (len vcd-vals)
      (len (svtv-debug-eval-aliases n aliases wirevals vcd-vals)))
  :rule-classes :linear)

Theorem: svtv-debug-eval-aliases-of-nfix-n

(defthm svtv-debug-eval-aliases-of-nfix-n
  (equal (svtv-debug-eval-aliases (nfix n)
                                  aliases wirevals vcd-vals)
         (svtv-debug-eval-aliases n aliases wirevals vcd-vals)))

Theorem: svtv-debug-eval-aliases-nat-equiv-congruence-on-n

(defthm svtv-debug-eval-aliases-nat-equiv-congruence-on-n
 (implies
  (nat-equiv n n-equiv)
  (equal
       (svtv-debug-eval-aliases n aliases wirevals vcd-vals)
       (svtv-debug-eval-aliases n-equiv aliases wirevals vcd-vals)))
 :rule-classes :congruence)

Theorem: svtv-debug-eval-aliases-of-lhslist-fix-aliases

(defthm svtv-debug-eval-aliases-of-lhslist-fix-aliases
  (equal (svtv-debug-eval-aliases n (lhslist-fix aliases)
                                  wirevals vcd-vals)
         (svtv-debug-eval-aliases n aliases wirevals vcd-vals)))

Theorem: svtv-debug-eval-aliases-lhslist-equiv-congruence-on-aliases

(defthm svtv-debug-eval-aliases-lhslist-equiv-congruence-on-aliases
 (implies
  (lhslist-equiv aliases aliases-equiv)
  (equal
       (svtv-debug-eval-aliases n aliases wirevals vcd-vals)
       (svtv-debug-eval-aliases n aliases-equiv wirevals vcd-vals)))
 :rule-classes :congruence)

Theorem: svtv-debug-eval-aliases-of-svex-env-fix-wirevals

(defthm svtv-debug-eval-aliases-of-svex-env-fix-wirevals
  (equal (svtv-debug-eval-aliases n aliases (svex-env-fix wirevals)
                                  vcd-vals)
         (svtv-debug-eval-aliases n aliases wirevals vcd-vals)))

Theorem: svtv-debug-eval-aliases-svex-env-equiv-congruence-on-wirevals

(defthm
      svtv-debug-eval-aliases-svex-env-equiv-congruence-on-wirevals
 (implies
  (svex-env-equiv wirevals wirevals-equiv)
  (equal
       (svtv-debug-eval-aliases n aliases wirevals vcd-vals)
       (svtv-debug-eval-aliases n aliases wirevals-equiv vcd-vals)))
 :rule-classes :congruence)