• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • 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-writephases

Signature

(svtv-debug-writephases phase nphases offset inalist ins 
                        ovlines prev-state updates next-states 
                        invars aliases vcd-wiremap vcd-vals p) 
 
  → 
(mv vcd-vals1 p1 final-state)

Arguments

phase — Guard (natp phase).

nphases — Guard (natp nphases).

offset — Guard (natp offset).

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

ins — Guard (svtv-lines-p ins).

ovlines — Guard (svtv-overridelines-p ovlines).

prev-state — Guard (svex-env-p prev-state).

updates — Guard (svex-alist-p updates).

next-states — Guard (svex-alist-p next-states).

invars — Guard (svarlist-p invars).

p — Guard (vl-printedlist-p p).

Returns

p1 — Type (vl-printedlist-p p1).

final-state — Type (svex-env-p final-state).

Definitions and Theorems

Function: svtv-debug-writephases

(defun svtv-debug-writephases
       (phase nphases offset inalist ins
              ovlines prev-state updates next-states
              invars aliases vcd-wiremap vcd-vals p)
 (declare (xargs :stobjs (aliases vcd-wiremap vcd-vals)))
 (declare (xargs :guard (and (natp phase)
                             (natp nphases)
                             (natp offset)
                             (svex-env-p inalist)
                             (svtv-lines-p ins)
                             (svtv-overridelines-p ovlines)
                             (svex-env-p prev-state)
                             (svex-alist-p updates)
                             (svex-alist-p next-states)
                             (svarlist-p invars)
                             (vl-printedlist-p p))))
 (declare (xargs :guard (and (<= phase nphases)
                             (<= (aliass-length aliases)
                                 (vcdwires-length vcd-wiremap))
                             (<= (vcdwires-length vcd-wiremap)
                                 (4vecs-length vcd-vals))
                             (<= (aliass-length aliases)
                                 (4vecs-length vcd-vals)))))
 (let ((__function__ 'svtv-debug-writephases))
  (declare (ignorable __function__))
  (b*
   (((when (mbe :logic (zp (- (nfix nphases) (nfix phase)))
                :exec (eql nphases phase)))
     (mv vcd-vals (vl::vl-printedlist-fix p)
         (svex-env-fix prev-state)))
    (in-vals
       (svex-alist-eval (svtv-phase-inputs phase ins ovlines invars)
                        inalist))
    (- (clear-memoize-table 'svex-eval))
    (eval-alist (append in-vals prev-state))
    ((mv wirevals next-state)
     (with-fast-alist
          eval-alist
          (mv (svex-alist-eval updates eval-alist)
              (svex-alist-eval next-states eval-alist))))
    (all-wirevals (append in-vals wirevals))
    (full-phase (+ (lnfix phase) (lnfix offset)))
    ((mv changes vcd-vals)
     (with-fast-alist
        all-wirevals
        (if (zp full-phase)
            (let* ((vcd-vals (svtv-debug-eval-aliases
                                  0 aliases all-wirevals vcd-vals)))
              (mv nil vcd-vals))
          (svtv-debug-eval-aliases-track
               0 aliases all-wirevals vcd-vals))))
    (p (if (zp full-phase)
           (vcd-dump-first-snapshot vcd-vals vcd-wiremap p)
         (vcd-dump-delta (* 10 full-phase)
                         changes vcd-vals vcd-wiremap p))))
   (svtv-debug-writephases (1+ (lnfix phase))
                           nphases offset inalist ins ovlines
                           next-state updates next-states invars
                           aliases vcd-wiremap vcd-vals p))))

Theorem: vl-printedlist-p-of-svtv-debug-writephases.p1

(defthm vl-printedlist-p-of-svtv-debug-writephases.p1
 (b*
  (((mv ?vcd-vals1 ?p1 ?final-state)
    (svtv-debug-writephases phase nphases offset inalist ins
                            ovlines prev-state updates next-states
                            invars aliases vcd-wiremap vcd-vals p)))
  (vl-printedlist-p p1))
 :rule-classes :rewrite)

Theorem: svex-env-p-of-svtv-debug-writephases.final-state

(defthm svex-env-p-of-svtv-debug-writephases.final-state
 (b*
  (((mv ?vcd-vals1 ?p1 ?final-state)
    (svtv-debug-writephases phase nphases offset inalist ins
                            ovlines prev-state updates next-states
                            invars aliases vcd-wiremap vcd-vals p)))
  (svex-env-p final-state))
 :rule-classes :rewrite)

Theorem: len-of-svtv-debug-writephases-vcd-vals

(defthm len-of-svtv-debug-writephases-vcd-vals
 (b*
  (((mv ?vcd-vals1 ?p1 ?final-state)
    (svtv-debug-writephases phase nphases offset inalist ins
                            ovlines prev-state updates next-states
                            invars aliases vcd-wiremap vcd-vals p)))
  (<= (len vcd-vals) (len vcd-vals1)))
 :rule-classes :linear)

Theorem: svtv-debug-writephases-of-nfix-phase

(defthm svtv-debug-writephases-of-nfix-phase
 (equal
    (svtv-debug-writephases (nfix phase)
                            nphases offset inalist ins
                            ovlines prev-state updates next-states
                            invars aliases vcd-wiremap vcd-vals p)
    (svtv-debug-writephases phase nphases offset inalist ins
                            ovlines prev-state updates next-states
                            invars aliases vcd-wiremap vcd-vals p)))

Theorem: svtv-debug-writephases-nat-equiv-congruence-on-phase

(defthm svtv-debug-writephases-nat-equiv-congruence-on-phase
 (implies
  (nat-equiv phase phase-equiv)
  (equal
    (svtv-debug-writephases phase nphases offset inalist ins
                            ovlines prev-state updates next-states
                            invars aliases vcd-wiremap vcd-vals p)
    (svtv-debug-writephases phase-equiv nphases offset inalist ins
                            ovlines prev-state updates next-states
                            invars aliases vcd-wiremap vcd-vals p)))
 :rule-classes :congruence)

Theorem: svtv-debug-writephases-of-nfix-nphases

(defthm svtv-debug-writephases-of-nfix-nphases
 (equal
    (svtv-debug-writephases phase (nfix nphases)
                            offset inalist ins
                            ovlines prev-state updates next-states
                            invars aliases vcd-wiremap vcd-vals p)
    (svtv-debug-writephases phase nphases offset inalist ins
                            ovlines prev-state updates next-states
                            invars aliases vcd-wiremap vcd-vals p)))

Theorem: svtv-debug-writephases-nat-equiv-congruence-on-nphases

(defthm svtv-debug-writephases-nat-equiv-congruence-on-nphases
 (implies
  (nat-equiv nphases nphases-equiv)
  (equal
    (svtv-debug-writephases phase nphases offset inalist ins
                            ovlines prev-state updates next-states
                            invars aliases vcd-wiremap vcd-vals p)
    (svtv-debug-writephases phase nphases-equiv offset inalist ins
                            ovlines prev-state updates next-states
                            invars aliases vcd-wiremap vcd-vals p)))
 :rule-classes :congruence)

Theorem: svtv-debug-writephases-of-nfix-offset

(defthm svtv-debug-writephases-of-nfix-offset
 (equal
    (svtv-debug-writephases phase nphases (nfix offset)
                            inalist ins
                            ovlines prev-state updates next-states
                            invars aliases vcd-wiremap vcd-vals p)
    (svtv-debug-writephases phase nphases offset inalist ins
                            ovlines prev-state updates next-states
                            invars aliases vcd-wiremap vcd-vals p)))

Theorem: svtv-debug-writephases-nat-equiv-congruence-on-offset

(defthm svtv-debug-writephases-nat-equiv-congruence-on-offset
 (implies
  (nat-equiv offset offset-equiv)
  (equal
    (svtv-debug-writephases phase nphases offset inalist ins
                            ovlines prev-state updates next-states
                            invars aliases vcd-wiremap vcd-vals p)
    (svtv-debug-writephases phase nphases offset-equiv inalist ins
                            ovlines prev-state updates next-states
                            invars aliases vcd-wiremap vcd-vals p)))
 :rule-classes :congruence)

Theorem: svtv-debug-writephases-of-svex-env-fix-inalist

(defthm svtv-debug-writephases-of-svex-env-fix-inalist
 (equal
    (svtv-debug-writephases phase
                            nphases offset (svex-env-fix inalist)
                            ins
                            ovlines prev-state updates next-states
                            invars aliases vcd-wiremap vcd-vals p)
    (svtv-debug-writephases phase nphases offset inalist ins
                            ovlines prev-state updates next-states
                            invars aliases vcd-wiremap vcd-vals p)))

Theorem: svtv-debug-writephases-svex-env-equiv-congruence-on-inalist

(defthm svtv-debug-writephases-svex-env-equiv-congruence-on-inalist
 (implies
  (svex-env-equiv inalist inalist-equiv)
  (equal
    (svtv-debug-writephases phase nphases offset inalist ins
                            ovlines prev-state updates next-states
                            invars aliases vcd-wiremap vcd-vals p)
    (svtv-debug-writephases phase nphases offset inalist-equiv ins
                            ovlines prev-state updates next-states
                            invars aliases vcd-wiremap vcd-vals p)))
 :rule-classes :congruence)

Theorem: svtv-debug-writephases-of-svtv-lines-fix-ins

(defthm svtv-debug-writephases-of-svtv-lines-fix-ins
 (equal
    (svtv-debug-writephases phase nphases
                            offset inalist (svtv-lines-fix ins)
                            ovlines prev-state updates next-states
                            invars aliases vcd-wiremap vcd-vals p)
    (svtv-debug-writephases phase nphases offset inalist ins
                            ovlines prev-state updates next-states
                            invars aliases vcd-wiremap vcd-vals p)))

Theorem: svtv-debug-writephases-svtv-lines-equiv-congruence-on-ins

(defthm svtv-debug-writephases-svtv-lines-equiv-congruence-on-ins
 (implies
  (svtv-lines-equiv ins ins-equiv)
  (equal
    (svtv-debug-writephases phase nphases offset inalist ins
                            ovlines prev-state updates next-states
                            invars aliases vcd-wiremap vcd-vals p)
    (svtv-debug-writephases phase nphases offset inalist ins-equiv
                            ovlines prev-state updates next-states
                            invars aliases vcd-wiremap vcd-vals p)))
 :rule-classes :congruence)

Theorem: svtv-debug-writephases-of-svtv-overridelines-fix-ovlines

(defthm svtv-debug-writephases-of-svtv-overridelines-fix-ovlines
 (equal
    (svtv-debug-writephases phase nphases offset inalist
                            ins (svtv-overridelines-fix ovlines)
                            prev-state updates next-states
                            invars aliases vcd-wiremap vcd-vals p)
    (svtv-debug-writephases phase nphases offset inalist ins
                            ovlines prev-state updates next-states
                            invars aliases vcd-wiremap vcd-vals p)))

Theorem: svtv-debug-writephases-svtv-overridelines-equiv-congruence-on-ovlines

(defthm
 svtv-debug-writephases-svtv-overridelines-equiv-congruence-on-ovlines
 (implies
  (svtv-overridelines-equiv ovlines ovlines-equiv)
  (equal
    (svtv-debug-writephases phase nphases offset inalist ins
                            ovlines prev-state updates next-states
                            invars aliases vcd-wiremap vcd-vals p)
    (svtv-debug-writephases phase
                            nphases offset inalist ins ovlines-equiv
                            prev-state updates next-states
                            invars aliases vcd-wiremap vcd-vals p)))
 :rule-classes :congruence)

Theorem: svtv-debug-writephases-of-svex-env-fix-prev-state

(defthm svtv-debug-writephases-of-svex-env-fix-prev-state
 (equal
    (svtv-debug-writephases phase nphases offset inalist
                            ins ovlines (svex-env-fix prev-state)
                            updates next-states
                            invars aliases vcd-wiremap vcd-vals p)
    (svtv-debug-writephases phase nphases offset inalist ins
                            ovlines prev-state updates next-states
                            invars aliases vcd-wiremap vcd-vals p)))

Theorem: svtv-debug-writephases-svex-env-equiv-congruence-on-prev-state

(defthm
     svtv-debug-writephases-svex-env-equiv-congruence-on-prev-state
 (implies
  (svex-env-equiv prev-state prev-state-equiv)
  (equal
    (svtv-debug-writephases phase nphases offset inalist ins
                            ovlines prev-state updates next-states
                            invars aliases vcd-wiremap vcd-vals p)
    (svtv-debug-writephases phase nphases offset inalist ins ovlines
                            prev-state-equiv updates next-states
                            invars aliases vcd-wiremap vcd-vals p)))
 :rule-classes :congruence)

Theorem: svtv-debug-writephases-of-svex-alist-fix-updates

(defthm svtv-debug-writephases-of-svex-alist-fix-updates
 (equal
    (svtv-debug-writephases phase nphases offset inalist ins ovlines
                            prev-state (svex-alist-fix updates)
                            next-states
                            invars aliases vcd-wiremap vcd-vals p)
    (svtv-debug-writephases phase nphases offset inalist ins
                            ovlines prev-state updates next-states
                            invars aliases vcd-wiremap vcd-vals p)))

Theorem: svtv-debug-writephases-svex-alist-equiv-congruence-on-updates

(defthm
      svtv-debug-writephases-svex-alist-equiv-congruence-on-updates
 (implies
  (svex-alist-equiv updates updates-equiv)
  (equal
    (svtv-debug-writephases phase nphases offset inalist ins
                            ovlines prev-state updates next-states
                            invars aliases vcd-wiremap vcd-vals p)
    (svtv-debug-writephases phase nphases offset inalist ins ovlines
                            prev-state updates-equiv next-states
                            invars aliases vcd-wiremap vcd-vals p)))
 :rule-classes :congruence)

Theorem: svtv-debug-writephases-of-svex-alist-fix-next-states

(defthm svtv-debug-writephases-of-svex-alist-fix-next-states
 (equal
    (svtv-debug-writephases phase nphases
                            offset inalist ins ovlines prev-state
                            updates (svex-alist-fix next-states)
                            invars aliases vcd-wiremap vcd-vals p)
    (svtv-debug-writephases phase nphases offset inalist ins
                            ovlines prev-state updates next-states
                            invars aliases vcd-wiremap vcd-vals p)))

Theorem: svtv-debug-writephases-svex-alist-equiv-congruence-on-next-states

(defthm
  svtv-debug-writephases-svex-alist-equiv-congruence-on-next-states
 (implies
  (svex-alist-equiv next-states next-states-equiv)
  (equal
    (svtv-debug-writephases phase nphases offset inalist ins
                            ovlines prev-state updates next-states
                            invars aliases vcd-wiremap vcd-vals p)
    (svtv-debug-writephases phase nphases offset inalist ins ovlines
                            prev-state updates next-states-equiv
                            invars aliases vcd-wiremap vcd-vals p)))
 :rule-classes :congruence)

Theorem: svtv-debug-writephases-of-svarlist-fix-invars

(defthm svtv-debug-writephases-of-svarlist-fix-invars
 (equal
    (svtv-debug-writephases phase nphases offset
                            inalist ins ovlines prev-state updates
                            next-states (svarlist-fix invars)
                            aliases vcd-wiremap vcd-vals p)
    (svtv-debug-writephases phase nphases offset inalist ins
                            ovlines prev-state updates next-states
                            invars aliases vcd-wiremap vcd-vals p)))

Theorem: svtv-debug-writephases-svarlist-equiv-congruence-on-invars

(defthm svtv-debug-writephases-svarlist-equiv-congruence-on-invars
 (implies
  (svarlist-equiv invars invars-equiv)
  (equal
      (svtv-debug-writephases phase nphases offset inalist ins
                              ovlines prev-state updates next-states
                              invars aliases vcd-wiremap vcd-vals p)
      (svtv-debug-writephases phase nphases
                              offset inalist ins ovlines prev-state
                              updates next-states invars-equiv
                              aliases vcd-wiremap vcd-vals p)))
 :rule-classes :congruence)

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

(defthm svtv-debug-writephases-of-lhslist-fix-aliases
 (equal
    (svtv-debug-writephases phase nphases offset
                            inalist ins ovlines prev-state updates
                            next-states invars (lhslist-fix aliases)
                            vcd-wiremap vcd-vals p)
    (svtv-debug-writephases phase nphases offset inalist ins
                            ovlines prev-state updates next-states
                            invars aliases vcd-wiremap vcd-vals p)))

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

(defthm svtv-debug-writephases-lhslist-equiv-congruence-on-aliases
 (implies
  (lhslist-equiv aliases aliases-equiv)
  (equal
    (svtv-debug-writephases phase nphases offset inalist ins
                            ovlines prev-state updates next-states
                            invars aliases vcd-wiremap vcd-vals p)
    (svtv-debug-writephases phase nphases offset inalist ins ovlines
                            prev-state updates next-states invars
                            aliases-equiv vcd-wiremap vcd-vals p)))
 :rule-classes :congruence)