Checkers - SVA: The Power of Assertions in SystemVerilog - page 191

Example 9.9. What happens if we pass the value of -1 to n in checker
request_granted (Example 9.5 )? Apparently, we should get an error message
about assertion a1 saying that ##-1 is wrong syntax. Since the user is not necessarily
familiar with the checker internals, it may be confusing. It would be much clearer if
we report the error message relative to the checker interface. We can do that using
a generate if statement as follows:
checker request_granted(
sequence req, property gnt, untyped n = 1, ...);
if (!$isunbounded(n) &&n<0)
$error("Delay value n cannot be negative", n);
...
a1: assert property (req |-> nexttime [n] gnt) else $error(msg);
endchecker : request_granted
$isunbounded(n) is a system function returning true if its argument is $. We
need this function to isolate the situation when the unbounded value is provided for
n because we cannot compare $ with 0. When the checker is instantiated with the
negative value for n the error message is issued at elaboration time. t

Use generate statements and elaboration system tasks to perform custom
elaboration-time checks and to issue custom elaboration error messages.

The ability to use generate statements is an important advantage of checkers over
bare assertions: checkers are more flexible and tunable. Therefore, it often makes
sense to use checkers even when they consist of a single assertion.

Example 9.10. We explain in Sect. 11.1.4 that simulation performance may degrade
when the antecedents have distant matches, or remain unfinished. If in the checker
request_granted , req is a long sequence or if there are incomplete pend-
ing requests, the simulation time may be negatively affected. It is possible to
truncate the antecedent to k clock ticks by intersecting it with 1[ * 1:k] ,as
explained in Example 11.16 . This truncation is very inefficient in FV, and it should
be avoided there. We can add an optional argument truncate to the checker
request_granted : when a nonzero value, say, 10, is passed to it, the antecedent
req will be truncated after 10 clock ticks, and when $ is passed, no truncation is
performed. The resulting checker is shown in Fig. 9.6 .
If truncate has a value $, the conditional generate if in Line 7 will yield
the sequence ante (antecedent) from Lines 8 to 10 in the elaboration model. If
truncate is positive, it will yield the sequence ante from Lines 14 to 16 .If
truncate has a nonpositive value, an error message is issued.
The reader may wonder why we suggested this solution instead of always
defining the antecedent of assertion a1 as req intersect 1[ * 1:truncate] .
This is, of course, correct, but both formal and simulation tools may implement
req intersect 1[ * 1:$] less efficiently than just req .

t