Symbolic-test-vector
An object describing a finite run of a hardware model.
Originally, symbolic test vectors (STVs) were conceived as an aid
to concretely and symbolically simulating E/esim modules. Now, a
similar library exists for Svex which is
nearly a drop-in replacement for esim STVs. See ACL2::symbolic-test-vectors for description of the original esim-based
library, and svex-stvs for a description of the differences in the new
svex version.
Subtopics
- Svtv-easy-bindings
- Generating G-bindings from an SVTV in a particular way.
- Svtv-flex-param-bindings
- Generating parametrized g-bindings from an SVTV using gl::flex-bindings.
- Svtv-flex-bindings
- Generating G-bindings from an SVTV using gl::flex-bindings.
