• 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
            • Elab-mod->vcd-wires
            • Vcd-scope
            • Vcd-wire
            • Vcd-print-4vec-aux
            • Vcd-dump-delta
            • Vcd-wirelist-add-to-wiremap
            • Vcd-print-header
            • Vcd-dump-first-snapshot-aux
            • Vcd-dump-delta-aux
            • Vcd-wiremap
            • 4vecarr
            • Vcd-print-wiredecls
            • Vcd-4vec-bitstr
            • Vcd-index->codechars
            • Vcd-wire->width
            • Vcd-index->codestr
            • Vcd-dump-first-snapshot
            • Vcd-wirelist
          • Debug.lisp
        • 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
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Vcd.lisp

Vcd-dump-delta

Signature

(vcd-dump-delta time changes vcd-vals vcd-wiremap p) → p1

Arguments

time — Guard (natp time).

changes — Guard (nat-listp changes).

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

Returns

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

Definitions and Theorems

Function: vcd-dump-delta

(defun vcd-dump-delta (time changes vcd-vals vcd-wiremap p)
  (declare (xargs :stobjs (vcd-vals vcd-wiremap)))
  (declare (xargs :guard (and (natp time)
                              (nat-listp changes)
                              (vl-printedlist-p p))))
  (declare
       (xargs :guard (and (<= (vcdwires-length vcd-wiremap)
                              (4vecs-length vcd-vals))
                          (or (atom changes)
                              (< (nat-list-max changes)
                                 (vcdwires-length vcd-wiremap))))))
  (let ((__function__ 'vcd-dump-delta))
    (declare (ignorable __function__))
    (b* ((p (rlist* p #\# (natstr time) #\Newline))
         (p (vcd-dump-delta-aux changes vcd-vals vcd-wiremap p)))
      (rlist* p #\Newline))))

Theorem: vl-printedlist-p-of-vcd-dump-delta

(defthm vl-printedlist-p-of-vcd-dump-delta
  (b* ((p1 (vcd-dump-delta time changes vcd-vals vcd-wiremap p)))
    (vl-printedlist-p p1))
  :rule-classes :rewrite)

Theorem: vcd-dump-delta-of-nfix-time

(defthm vcd-dump-delta-of-nfix-time
  (equal (vcd-dump-delta (nfix time)
                         changes vcd-vals vcd-wiremap p)
         (vcd-dump-delta time changes vcd-vals vcd-wiremap p)))

Theorem: vcd-dump-delta-nat-equiv-congruence-on-time

(defthm vcd-dump-delta-nat-equiv-congruence-on-time
  (implies
       (nat-equiv time time-equiv)
       (equal (vcd-dump-delta time changes vcd-vals vcd-wiremap p)
              (vcd-dump-delta time-equiv
                              changes vcd-vals vcd-wiremap p)))
  :rule-classes :congruence)

Theorem: vcd-dump-delta-of-nat-list-fix-changes

(defthm vcd-dump-delta-of-nat-list-fix-changes
  (equal (vcd-dump-delta time (acl2::nat-list-fix changes)
                         vcd-vals vcd-wiremap p)
         (vcd-dump-delta time changes vcd-vals vcd-wiremap p)))

Theorem: vcd-dump-delta-nat-list-equiv-congruence-on-changes

(defthm vcd-dump-delta-nat-list-equiv-congruence-on-changes
 (implies
      (acl2::nat-list-equiv changes changes-equiv)
      (equal (vcd-dump-delta time changes vcd-vals vcd-wiremap p)
             (vcd-dump-delta time
                             changes-equiv vcd-vals vcd-wiremap p)))
 :rule-classes :congruence)