• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Community
  • Proof-automation
  • Macro-libraries
  • ACL2
  • 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-track

Signature

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

Arguments

n — Guard (natp n).

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

Returns

changes — Type (nat-listp changes).

Definitions and Theorems

Function: svtv-debug-eval-aliases-track

(defun svtv-debug-eval-aliases-track (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-track))
   (declare (ignorable __function__))
   (b* (((when (mbe :logic (zp (- (aliass-length aliases) (nfix n)))
                    :exec (eql (aliass-length aliases) n)))
         (mv nil vcd-vals))
        (lhs (get-alias n aliases))
        (val (svtv-debug-lhs-eval lhs n wirevals vcd-vals))
        (prev-val (get-4vec n vcd-vals))
        (vcd-vals (set-4vec n val vcd-vals))
        ((when (equal prev-val val))
         (svtv-debug-eval-aliases-track (1+ (lnfix n))
                                        aliases wirevals vcd-vals))
        ((mv rest-changes vcd-vals)
         (svtv-debug-eval-aliases-track (1+ (lnfix n))
                                        aliases wirevals vcd-vals)))
     (mv (cons (lnfix n) rest-changes)
         vcd-vals))))

Theorem: nat-listp-of-svtv-debug-eval-aliases-track.changes

(defthm nat-listp-of-svtv-debug-eval-aliases-track.changes
 (b* (((mv ?changes ?vcd-vals1)
       (svtv-debug-eval-aliases-track n aliases wirevals vcd-vals)))
   (nat-listp changes))
 :rule-classes :rewrite)

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

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

Theorem: nat-list-max-of-svtv-debug-eval-aliases-track

(defthm nat-list-max-of-svtv-debug-eval-aliases-track
 (implies
  (consp
   (mv-nth
       0
       (svtv-debug-eval-aliases-track n aliases wirevals vcd-vals)))
  (<
   (nat-list-max
    (mv-nth
       0
       (svtv-debug-eval-aliases-track n aliases wirevals vcd-vals)))
   (len aliases)))
 :rule-classes :linear)

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

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

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

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

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

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

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

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

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

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

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

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