		Search-engine friendly clone of the ACL2 documentation.

Svex-stvs

Svtv-spec

A data object representing a run of an FSM, similar to an SVTV but without computing the unrolling of the FSM.

This is a product type introduced by defprod.

Fields

fsm — fsm: The FSM to be run
cycle-phases — svtv-cyclephaselist: The list of svtv-cyclephase objects representing the clock cycle
namemap — svtv-name-lhs-map: Mapping from namemap names to lhs objects in terms of FSM signal names
probes — svtv-probealist: Specification for which outputs/internal signals should be sampled when, in terms of namemap names
in-alists — svex-alistlist: Specification for what (symbolic) inputs are set at what cycles -- a list of binding alists (one for each cycle) of namemap names to constants and user variable names.
override-test-alists — svex-alistlist: Specification for what override tests are set at what cycles -- similar to in-alists
override-val-alists — svex-alistlist: Specification for what override values are set at what cycles -- similar to in-alists
initst-alist — svex-alist: Initial state, mapping from FSM previous-state variables to constants and user variable names

When creating an svtv using defsvtv$, a phase FSM is created for the given design and subsequently that phase FSM is composed further into a clock cycle FSM and then a combinational pipeline, which is an unrolling of the cycle FSM. This pipeline unrolling is the main content of an SVTV object (namely, its outexprs field). An svtv-spec object contains the data necessary to compute the pipeline, but not the unrolled cycle FSM or pipeline itself. It can be shown that an svtv-run of an SVTV is equal to the svtv-spec-run of an analogous svtv-spec object.

Subtopics

Svtv-spec-run: Run an svtv-spec object and return its outputs
Svtv-spec-fix: Fixing function for svtv-spec structures.
Make-svtv-spec: Basic constructor macro for svtv-spec structures.
Svtv-spec-p: Recognizer for svtv-spec structures.
Svtv-spec-equiv: Basic equivalence relation for svtv-spec structures.
Svtv-spec->override-test-alists: Get the override-test-alists field from a svtv-spec.
Svtv-spec->override-val-alists: Get the override-val-alists field from a svtv-spec.
Svtv-spec->cycle-phases: Get the cycle-phases field from a svtv-spec.
Change-svtv-spec: Modifying constructor for svtv-spec structures.
Svtv-spec->namemap: Get the namemap field from a svtv-spec.
Svtv-spec->initst-alist: Get the initst-alist field from a svtv-spec.
Svtv-spec->in-alists: Get the in-alists field from a svtv-spec.
Svtv-spec->probes: Get the probes field from a svtv-spec.
Svtv-spec->fsm: Get the fsm field from a svtv-spec.