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

1.4.4 Assertion Efficiency

It is often possible to express the same assertions in multiple ways. A specific
style of assertion implementation may have a major effect on simulation or formal
verification performance. Therefore, it is important to know how to write assertions
efficiently. Unfortunately, in many cases formal verification and simulation impose
different requirements on assertions for efficiency considerations, creating situations
where efficiency tradeoff between the two methods becomes necessary. Possibilities
exist to make a small sacrifice in assertion efficiency in formal verification that
can provide a tremendous boost in simulation speed. Many factors are involved
in making tradeoffs: complexity of assertions, number of assertions, and algorithms
employed by a specific tool. When using a specific simulation or formal verification
tool one should follow tool-specific recommendations about assertion efficiency.

1.5 Assertion Reuse

Although SVA is a powerful specification language, writing assertions is not an
easy task. Even experienced people rarely write complex assertions correctly for
the first time. Debugging assertions is more difficult than debugging RTL because
the assertion language is declarative. Fortunately, many assertions are commonly
encountered and may be reused by adapting them to different situations. For
example, such assertions as “two signals are mutually exclusive”, “a request is
granted in N cycles”, and “an FSM is never stuck” are routine. This presents an
opportunity to define them once and then reuse by customizing as a library unit.
SVA provides many features for assertion reuse. Assertion components may be
named and parameterized. Several related assertions, together with modeling code
may be grouped as a unit for future reuse.

Expression Reuse

Expressions may be named and parameterized using a let statement, as shown in
Fig. 1.10 .
In this example, a parameterized expression $onehot(~sig) is named onecold
using a let statement. $onehot is a SVA system function returning true 9
when exactly one bit of its argument is set to 1. This let expression checks for one
cold encoding which means exactly one bit of sig is 0. Notice that an instance of
the let expression is used in assertions a1 , a2 , and a3 . a1 is an immediate assertion

9 Strictly speaking, true is not defined in SystemVerilog, but we will use it where appropriate as an
alias for 1'b1 . Similarly, we will use false for 1'b0 .