Def-svtv-ideal
Define a non-executable, fixpoint-based analogue of a symbolic-test-vector.
To use this, first define an SVTV using defsvtv$
and (immediately after) save the contents of the resulting svtv-data
stobj to an object using def-svtv-data-export. Then invoke
def-svtv-ideal as follows:
(def-svtv-ideal ideal-name svtv-name data-name)
For example,
(sv::defsvtv$ my-mod-run ...)
;; must be immediately after the defsvtv$ (or at least ensure that the
;; svtv-data stobj is not modified in between)
(sv::def-svtv-data-export my-mod-data)
;; may occur later, no more reliance on the svtv-data stobj:
(sv::def-svtv-ideal my-mod-ideal my-mod-run my-mod-data)
This produces a 0-ary function (not intended to be executed) named
my-mod-ideal, which returns an svtv-spec object encapsulating the
same pipeline run as in my-mod-run, but based on a fixpoint composition of
the module's assignments rather than the approximate composition that is
computed for the SVTV. See svex-fixpoint-decomposition-methodology for
further explanation. A few important properties relating my-mod-ideal and
my-mod-run are proved:
- my-mod-ideal-refines-my-mod-run -- this allows us to infer facts about
my-mod-ideal from proofs about my-mod-run, where potentially the
my-mod-run proof may be done with override signals that may be removed
from the theorem about my-mod-ideal.
- my-mod-ideal-refines-my-mod-run-on-same-envs -- special case of the
above theorem where the input environments are the same, i.e. no overrides are
removed.
- my-mod-ideal-refines-my-mod-ideal -- this allows us to remove
overrides from theorems about my-mod-ideal.
Additionally, the def-svtv-ideal event produces a function named (in
our example) my-mod-ideal-exec, which (logically) produces some subset of
the output signals of a svtv-spec-run of my-mod-ideal, but
accomplishes this (when successful) executing svtv-run of
my-mod-run. If the outputs from the svtv-run contain no Xes, then
this is the same as the svtv-spec-run of my-mod-ideal.
