Hardware Reference
In-Depth Information
Chapter 19
Debugging Assertions and Efficiency
Considerations
If everything seems to be going well, you have obviously
overlooked something.
— Steven Wright
Properties and sequences allow us to describe complex behaviors in a very compact
declarative form. That form is quite different from the procedural style used for
writing RTL and other design models as well as test benches. Thus, assertions may
also need a different style for debugging them. Issues related to the run time and
memory overheads for complex temporal assertions also need to be addressed. The
same behavior may be expressed using different assertions. Each may have different
efficiency in formal verification and simulation. We discuss both debugging and
efficiency in this chapter.
There are two kinds of situations to consider (see also [
19
]):
A failure for an assertion from a checker library or a user-written one. Failure
of an assertion from a library usually points to its incorrect usage or a problem
in the design under verification, assuming that the library was validated. User-
written assertion failure may be due to a design error or an incorrect formulation
of the assertion.
A failure for an assertion under development or during regression that needs to
be analyzed. Failure of an assertion under development usually means a failure
during specific simulation tests created to validate the assertion before use in
verifying a design. Failure during regression is more likely to be due to an error
in the design, assuming that the assertion was validated.
Developing assertion-based checkers uses similar techniques as for developing
custom assertions. The main difference is that the testing and documentation must
be quite extensive as demonstrated, for example, in the Accellera OVL checker
library [
10
]. In either situation, effective means must be provided to pinpoint the
source of the problem. Verification tool vendors often provide various mechanisms
Search WWH ::
Custom Search