• 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$
            • Defcycle
            • Def-pipeline-thm
            • Def-svtv-data-export
            • Def-svtv-data-import
            • Svtv-name-lhs-map
            • Def-cycle-thm
            • Def-svtv-data-export/import
            • Defsvtv$-phasewise
            • 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$.