Hardware Reference
In-Depth Information
or the assumptions in some indirect way that the automatic pruning algorithms
cannot determine. The verification engineer must thus have detailed knowledge of
the design.
Note that the pruning directives relate to different types of approximation:
Setting an input signal
is underapproximation—we eliminate some model behav-
iors, which can lead to false positives but not to false negatives. Setting input
signals is thus safe but not sound.
Freeing any signal
in the model is an overapproximation—it can only introduce
more behaviors than allowed by the original model. Therefore, it can only
introduce false negatives, but not false positives. Freeing is sound but not safe.
Setting an internal signal
may forbid some behaviors of the original model, but
may also introduce new behaviors (for example, when in the original model a
signal is toggling, and now it is set to a constant value). This kind of pruning may
introduce both false positives and false negatives, and it is neither safe nor sound.
Often there are additional pruning directives provided by the tools, such as black-
boxing parts of the model, but they are beyond the scope of this topic.
20.4
Formal Verification Flows
We now have the necessary background to discuss formal verification flows in RTL
design and verification. There are many possible scenarios; we focus on three of
them:
Exhaustive verification of model specification.
Lightweight verification.
Early RTL verification.
20.4.1
Exhaustive Verification of Model Specification
Figure
20.3
represents a block diagram of the typical FV flow for exhaustively
verifying model compliance to its specification.
The flow starts with writing the specification for the design. The specification
consists of a set of assumptions on the primary inputs and a set of assertions
describing the expected behavior under these assumptions. The specification is
checked first for sanity and debugging in simulation. If there is no simulation
environment available, it is possible to check parts of the specification on manually
created traces. Upon completion of sanity checks and debug, a formal verification
tool is applied. There may be three outcomes of checking a specific assertion:
Search WWH ::
Custom Search