Introduction - SVA: The Power of Assertions in SystemVerilog - page 7

Assertions Promote Faster Root Cause Analysis
Because assertions can represent temporal behavior, a failure of an assertion that
stretches out over multiple clock cycles detects a bug and concisely isolates it
to the assertion expression. Now, one only needs to examine and analyze the
temporal expression of the assertion to determine the root cause of the failure.
Several modern debug tools support such an analysis to speed up the bug-fixing
process. For example, by providing a precise window of time in which the failure
occurred along with the cycle-by-cycle values of assertion signals, engineers can
direct the analysis in the immediate design area of the failure. This is highly valuable
and efficient.
A similar case with traditional techniques requires engineers to detect the failure
by examining the output results, perhaps a mismatch of a value many cycles after
the occurrence of the failure. A manual trace of values cycle by cycle through the
design, without having specific clues about the behavior that actually caused the
failure, is what the engineer must typically follow. As such, much of the difficult
debugging is confined to the experts who retain intricate knowledge of the design.
Assertions Can Use Simulation and Formal Checking
The essential SVA features that exhibit temporality and clocking are strictly based
on a mathematical framework, well understood and studied in academia. The
availability of formalism made it possible to adopt proven algorithms for simulation
and formal analysis. This enables taking the same assertion and applying both
methods, one in a simulation environment for a set of tests, and the other in formal
verification to conduct thorough proof analysis. Barring the limitations imposed by
the fundamental differences between the two methods, both methods are applied to
the same assertions for benefits within their individual processes.
The great benefit from this symmetry of use is that engineers need to write asser-
tions only once. In most cases, a failure in simulation can be reproduced in formal
analysis, and vice versa. A good methodology provides sufficient adjustments to
take care of the small practical differences and limitations between the two methods.
Besides being efficient, using the same assertions expels the major impediment
to ensuring that the same behavior is checked by simulation and formal methods.
Formal methods would check the critical blocks, and simulation would concentrate
on system integration and the remaining blocks within it.