|
|
|---|
|
|
|
|---|
Summary of the relative advantages of the ideal-based vs syntactic-check-based methods for SVTV decomposition.
See svex-decomposition-methodology for background on these choices. This topic pertains to the choice in SVTV decomposition proofs of whether, in proofs using def-svtv-generalized-thm, to target the SVTV itself (showing the override transparency property using a syntactic check), the SVTV-spec analogous to that SVTV (also using the syntactic check), or the idealized SVTV-spec based on a fixpoint composition (without needing the syntactic check).
The main advantage of the ideal-based method is that the syntactic check of the other method might not pass on your design, and the FGL equivalence check-based fallback method might be too expensive. If these checks pass, you can do your decomposition proofs using the syntax check method, and subsequently if needed you can always define an ideal later; any theorems already proved about the SVTV are true of it as well. However, it's also possible that the syntactic check will work on some set of overrides but fail if more override signals are added because some new signal to be overridden is involved in an apparent combinational loop. This is mainly of concern if there is latch-based logic in the design, but can come up in other situations.
The disadvantage of the ideal-based method is that what you've proved about the ideal isn't always provable about the computed SVTV. Generally we only know that the computed SVTV's results are conservative approximations of those of the ideal SVTV. If we can show that the computed SVTV's results are non-X for some case, then we know it's equivalent to the ideal SVTV for that case. But this has to be proved without overrides, which can be prohibitively expensive. In most cases it's good enough to know these facts about the ideal. However, if (e.g.) we want to prove via equivalence checking that some new design produces the same result as an original design, which we've proven correct via decomposition, then the equivalence check has to be done between the computed SVTVs, but we really want to show that the ideal SVTV for the new design is equivalent to the ideal SVTV of the original design. Assuming the equivalence check passes, it's still possible that the new design's SVTV and ideal SVTV along with the original design's SVTV all produce X in some case where the correct result (and the result computed by the original design's ideal SVTV) is non-X.
If the syntactic check works on your design for all the override signals
needed, you can choose to phrase your generalized theorems on the SVTV itself
or an analogous SVTV-spec object. This decision isn't as important because the
two types of generalized theorems can be reproved about the other object. If
the generalized theorems are proved about SVTV-spec objects, they can be
reproved about the SVTV itself by using the equivalence between the SVTV and
SVTV-spec (a theorem named according to the scheme