Def-svtv-refinement
For a given SVTV, prove the theorems necessary to use that SVTV
in (de)composition proofs using def-svtv-generalized-thm, as in the
svex-decomposition-methodology.
Prerequisite: An SVTV defined with defsvtv$, and an svtv-data-obj created using def-svtv-data-export immediately after
defining that SVTV.
Usage:
(def-svtv-refinement svtv-name data-name
;; optional:
:fgl-semantic-check t
:omit-default-aignet-transforms t
:ideal idealname
:svtv-spec specname
:fsm my-fsm-name
:define-fsm t
:inclusive-overridekeys t
:pkg-sym pkg-sym)
A particular type of invocation has an alias, def-svtv-ideal -- in
particular, these two forms are equivalent:
(def-svtv-ideal ideal-name svtv-name data-name)
(def-svtv-refinement svtv-name data-name :ideal ideal-name)
This form either proves the override transparency property (discussed in
svex-decomposition-methodology) of the given SVTV, or defines an
idealized SVTV and proves the override transparency property about it.
If the :ideal is provided, this is like an invocation of def-svtv-ideal: it produces an idealized svtv-spec object that is a refinement
of the given SVTV and proves that it satisfies the override-transparency
property. The top-level theorems are then called
idealname-refines-idealname (the ideal SVTV-spec satisfies the
override-transparency property on its own) and
idealname-refines-svtvname (relating the ideal SVTV-spec with the original
SVTV).
If not, then the syntactic check method is used to prove the
override-transparency property of the given SVTV itself. If the
:fgl-semantic-check keyword argument is set, then if any overrides fail
the syntactic check for the override transparency property, an FGL proof will
be attempted to show the same property using equivalence checking -- see below.
The main theorem, showing that it satisfies the override-transparency
property, is svtvname-refines-svtvname. If the :svtv-spec argument
is given, this also defines a function (with the given name) with the same
behavior as the original SVTV and adds another refinement theorem,
specname-refines-svtvname.
The FGL proof of override transparency, attempted only when
:fgl-semantic-check is set and some overrides fail the syntactic check,
requires the "centaur/fgl/top" book to be included. Additionally, by default
a special AIGNET simplification
routine is used in the equivalence check. This can be overridden with
:omit-default-aignet-transforms, but if not, the
"centaur/aignet/transforms" and "centaur/ipasir/ipasir-backend" books must
also be loaded. The latter requires an IPASIR shared library to be available and the
IPASIR_SHARED_LIBRARY environment variable set accordingly; see ipasir::building-an-ipasir-solver-library for how to get one. In summary, the
following include-books are usually needed when using the FGL semantic
check:
(include-book "centaur/fgl/top" :dir :system)
(include-book "centaur/aignet/transforms" :dir :system)
(include-book "centaur/ipasir/ipasir-backend" :dir :system)
Subtopics
- Def-override-transparent
- For a given FSM and set of keys (internal signal names), prove that the FSM is override-transparent with respect to those keys.
