• 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
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Vcd.lisp

Vcd-print-header

Signature

(vcd-print-header date scope p) → p1

Arguments

date — Guard (stringp date).

scope — Guard (vcd-scope-p scope).

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

Returns

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

Definitions and Theorems

Function: vcd-print-header

(defun vcd-print-header (date scope p)
  (declare (xargs :guard (and (stringp date)
                              (vcd-scope-p scope)
                              (vl-printedlist-p p))))
  (let ((__function__ 'vcd-print-header))
    (declare (ignorable __function__))
    (b* ((p (rlist* p "$date " (str-fix date)
                    "$end" #\Newline
                    "$version SVTV-DEBUG simulation $end"
                    #\Newline "$timescale 1 s $end"
                    #\Newline #\Newline))
         (p (vcd-print-scope scope p)))
      (rlist* p "$enddefinitions $end"
              #\Newline #\Newline))))

Theorem: vl-printedlist-p-of-vcd-print-header

(defthm vl-printedlist-p-of-vcd-print-header
  (b* ((p1 (vcd-print-header date scope p)))
    (vl-printedlist-p p1))
  :rule-classes :rewrite)

Theorem: vcd-print-header-of-str-fix-date

(defthm vcd-print-header-of-str-fix-date
  (equal (vcd-print-header (str-fix date)
                           scope p)
         (vcd-print-header date scope p)))

Theorem: vcd-print-header-streqv-congruence-on-date

(defthm vcd-print-header-streqv-congruence-on-date
  (implies (acl2::streqv date date-equiv)
           (equal (vcd-print-header date scope p)
                  (vcd-print-header date-equiv scope p)))
  :rule-classes :congruence)

Theorem: vcd-print-header-of-vcd-scope-fix-scope

(defthm vcd-print-header-of-vcd-scope-fix-scope
  (equal (vcd-print-header date (vcd-scope-fix scope)
                           p)
         (vcd-print-header date scope p)))

Theorem: vcd-print-header-vcd-scope-equiv-congruence-on-scope

(defthm vcd-print-header-vcd-scope-equiv-congruence-on-scope
  (implies (vcd-scope-equiv scope scope-equiv)
           (equal (vcd-print-header date scope p)
                  (vcd-print-header date scope-equiv p)))
  :rule-classes :congruence)