• 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
          • 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-data

    Defsvtv$-phasewise

    (Deprecated) Create an SVTV using the defsvtv-phasewise syntax, storing and possibly using intermediate results from the svtv-data stobj.

    The formerly different syntax of defsvtv$-phasewise is now allowed in defsvtv$, and so defsvtv$-phasewise is now just an alias for defsvtv$.