• 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-chase$-compare
            • Svtv-chase-defsvtv$
          • Svtv-versus-stv
          • Svtv-debug-fsm
          • Structure.lisp
          • Svtv-debug
          • 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
  • Svex-stvs

Svtv-chase$

Diagnose hardware or stimulus bugs by studying an SVTV run in a special-purpose read-eval-print loop.

To enter this read-eval-print loop for the first time, run:

(svtv-chase$ svtv env)

where SVTV is an svtv object (as produced by defsvtv) and env is an assignment to the input/override signals of that SVTV. Depending on the complexity of the SVTV, the initial setup done by this command may take a few minutes.

When setup is complete, you'll be shown an SVTV-CHASE > prompt. Typing ? at this prompt shows the commands that may be used there. Typically you'll start by going to a signal of interest at a certain phase, using the O or G commands. At a given signal/phase, SVTV-CHASE will print the type of signal -- primary input, initial state, previous state, or internal signal. For internal signals, it will also print the list of signals that are this signal's immediate dependencies. To see the expression driving the current signal, you may enter EXPR. The next step is usually to select one of the signal's dependencies and go to it, by typing its number. To go back to the signal you just left, you may type B to pop the stack of signal/phase positions.

At some point you may want to exit the read-eval-print loop, which you can do by typing X at the prompt. To re-enter the loop, you can skip the initial setup by running (svtv-chase$-repl).

See svtv-chase-defsvtv$ for a utility that gives the same behavior but doesn't require the SVTV to be defined already.

Subtopics

Svtv-chase$-compare
Compare two runs of a module using the svtv-chase$ utility.
Svtv-chase-defsvtv$
Enter the svtv-chase$ read-eval-print loop without first defining an SVTV.