• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Community
    • 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
    • Svtv-data

    Def-svtv-data-export/import

    Combines def-svtv-data-export and def-svtv-data-import.

    Usage:

    (def-svtv-data-export/import
      export-name
      :stobj stobj-name)  ;; default: sv::svtv-data

    This just does def-svtv-data-export followed by def-svtv-data-import, i.e. defines a constant and 0-ary function export-name containing the current contents of the given svtv-data stobj, and subsequently defines a function that copies those contents back into such a stobj.