Def-svtv-data-export
Copy the contents of a svtv-data stobj into a constant.
Usage:
(def-svtv-data-export export-name
:stobj stobj-name) ;; default: sv::svtv-data
This copies the contents of svtv-data (or another stobj congruent to it, if
specified) into a constant and 0-ary function satisfying svtv-data-obj-p,
and proves that the 0-ary function satisfies
(svtv-data$ap (svtv-data-obj-to-stobj-logic (export))), i.e. if converted
back to stobj form it still satisfies the svtv-data$ap invariant. This
has important implications, e.g. see theorems such as
cycle-fsm-validp-of-svtv-data-obj: if the data object has its
cycle-fsm-validp and flatten-validp fields set, then the
cycle-fsm field has a certain relationship to the phase-fsm field.
See also def-svtv-data-import which defines a function to put the
exported object back into a stobj, and def-svtv-data-export/import which
simply combines the two events.
Subtopics
- Svtv-data-obj
- A non-stobj representation of a svtv-data stobj, as produced by def-svtv-data-export.
