		Search-engine friendly clone of the ACL2 documentation.

Svtv

A shorter name for svex-stvs, i.e. SVEX Symbolic Test Vectors.

This is a product type introduced by defprod.

name — symbolp
outexprs — svex-alist
nextstate — svex-alist: NIL if not defined with :state-machine t or :keep-final-state t
states — svex-alistlist: NIL if not defined with :keep-all-states t
inmasks — svar-boolmasks
outmasks — svar-boolmasks
inmap — svtv-inputmap
orig-ins — ACL2::true-list-list
orig-overrides — ACL2::true-list-list
orig-outs — ACL2::true-list-list
orig-internals — ACL2::true-list-list
expanded-ins — svtv-lines
expanded-overrides — svtv-lines
nphases — natp
labels — ACL2::symbol-list
form: Original form defining the defsvtv

Svtv-chase: (Deprecated) Diagnose hardware or stimulus bugs by studying an SVTV run in a special-purpose read-eval-print loop.
Svtv-p: Recognizer for svtv structures.
Svtv-to-fsm: Umbrella topic about proving FSM properties from SVTV properties
Make-svtv: Basic constructor macro for svtv structures.
Svtv-fix: Fixing function for svtv structures.
Change-svtv: Modifying constructor for svtv structures.
Svtv-equiv: Basic equivalence relation for svtv structures.
Svtv->orig-overrides: Get the orig-overrides field from a svtv.
Svtv->orig-internals: Get the orig-internals field from a svtv.
Svtv->expanded-overrides: Get the expanded-overrides field from a svtv.
Svtv->states: Get the states field from a svtv.
Svtv->nextstate: Get the nextstate field from a svtv.
Svtv->expanded-ins: Get the expanded-ins field from a svtv.
Svtv->outmasks: Get the outmasks field from a svtv.
Svtv->outexprs: Get the outexprs field from a svtv.
Svtv->orig-outs: Get the orig-outs field from a svtv.
Svtv->orig-ins: Get the orig-ins field from a svtv.
Svtv->inmasks: Get the inmasks field from a svtv.
Svtv->nphases: Get the nphases field from a svtv.
Svtv->name: Get the name field from a svtv.
Svtv->labels: Get the labels field from a svtv.
Svtv->inmap: Get the inmap field from a svtv.
Svtv->form: Get the form field from a svtv.