Hardware Reference
In-Depth Information
Chapter 23
Checkers in Formal Verification
Hope is a great falsifier. Let good judgment keep her in check.
— Baltasar Gracian
This chapter discusses applications of checkers to formal verification. Checkers
were introduced in Chap. 9 , where we described their primary use as an instantiable
container for assertions and associated modeling code. This chapter presents an
additional feature of checkers that is important for formal verification— free vari-
ables . Free variables support the construction of abstract nondeterministic models
and reasoning about them. Recall from Chap. 20 that an abstract model is an over-
approximation of the DUT. If an assertion has been proven for an abstract model,
then it also holds for the DUT. Good abstraction hides irrelevant details and yields
a simpler model on which to conduct formal verification. For example, to reason
about a pipeline latency, the exact data passed through the pipeline and the exact
operations at specific pipeline stages may be immaterial and may be abstracted
away. Checkers provide natural building blocks for these abstract models, and their
usage in FV modeling is similar to the usage of modules in RTL.
Another important application of checkers with free variables is to build abstract
models of the DUT environment. Such models may be supported both in simulation
and in FV, in contrast to traditional software testbenches that are not FV-friendly.
Careful modeling of the environment, avoiding false negatives and false positives
(see Sect. 20.3 ), is a major and effort-consuming problem in FV. Of course, carefully
crafting the environment and writing tests is also important for simulation. Usually
there is no reuse of the environment between simulation and FV. Checkers with free
variables provide an approach to environment modeling that can, in many situations,
be used by both engines and eliminate redundant effort.
Checker free variables, including constant free variables (also called rigid
variables ), can be used in an alternative coding style instead of assertion local
variables. Each style has advantages and disadvantages.
Search WWH ::




Custom Search