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

1.2.3 Using Assertions Beyond RTL

Although assertions are most frequently used at the RT level, other areas of
development later in the design phase can also benefit from their specification. Some
analysis tools have already been developed, while others have been explored to take
advantage of the expressibility of the assertion features. We discuss three important
areas here.

Equivalence Verification

Equivalence [ 45 ] of two models usually means checking that the synthesized gate-
level netlist is equivalent to the golden RTL model (Fig. 1.5 ). Equivalence checking
is also needed when local changes are made in the design to improve its performance
or power consumption.
Equivalence checking is usually done by formal verification because comparing
model behaviors in simulation cannot provide good confidence in the correctness
of design transformations. At first, it seems that there is no need for assertions in
equivalence verification, but it turns out that the role of assertions is quite significant
because two models are equivalent only under some assumptions on their inputs.
For example, the input signal go of an RTL model may correspond to two input
signals of the synthesized model: go and its negation ngo . To prove equivalence the
following assumption about signal inversion should be supplied to the tool:

assume final (go ^ ngo);
In addition, assumptions about internal signals are used as hints for formal
equivalence verification. To maintain correctness of the proof of equivalence,
these assumptions must be proven as assertions in the corresponding blocks (see
Sect. 20.5 ). Assumptions written for formal equivalence verifications are usually
nontemporal; therefore, they are best represented with final assumptions having the
syntax assume final as shown above.

Timing Verification

When an RTL model is synthesized into a gate-level model, a critical step is to
verify its timing to ascertain correct functioning of the circuit [ 27 ]. Even though
timing verification significantly differs from RTL verification, assertions are used
there, although for different purposes. For example, RTL assertions are used to
characterize signal paths, as in the following cases:

False Path Elimination Circuit performance is limited by the delay of the longest
combinatorial path. Given the circuit configuration, if the actual signal trans-
mission along this path is not possible then this path should be ignored for
critical path and performance analysis [ 15 , 28 ].