• 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
          • Def-pipeline-thm
          • Expand.lisp
          • Def-cycle-thm
          • Svtv-utilities
          • Svtv-debug$
            • Svtv-debug-defsvtv$
            • 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
    • Svtv-debug$

    Svtv-debug-defsvtv$

    Dump a VCD waveform for an SVTV, without first having defined the SVTV.

    Usage:

    (svtv-debug-defsvtv$
      ;; entire form used to define an SVTV.  May also be DEFSVTV$.
      (defsvtv$-phasewise ...)
      :env env
      :filename "my-file.vcd") ;; default "svtv-debug.vcd"

    See svtv-debug$. This version is useful in cases where a user is debugging the signal settings of an SVTV. It skips the composition of the cycle FSM and pipeline stages, which on large designs can greatly shorten the debug loop.