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

The formal argument req of checker request_granted is of type sequence, whereas the actual
argument nexttime go is an expression of type property.

Consider the message we might get if the req argument were untyped, as in
Example 9.5 :
Type mismatch in
a1: assert property(req |-> nexttime[n] gnt) else $error(msg);
req is of property type, whereas sequence type is expected.

The user understands the first error message, since it explains the problem
in terms of the interface of the checker. However, the second error message is
confusing because it mentions the checker internals , which are normally hidden
from the user.
Unfortunately, it is not always possible or desirable to provide a specific type
for a checker argument. Although it seems natural to declare n as int , doing so
would exclude the possibility of passing the checker an infinite upper bound $ ,
since only untyped formal arguments may receive $ . In our example, we have to
explicitly declare n as untyped , otherwise its type would be taken from the previous
argument gnt that is of type property .Wealsohavetoleave rst untyped because
providing a specific type, say, logic , would require type conversion when the actual
argument is of a different type. This may affect checker correctness or slow down
the simulation.

t

Always specify an explicit type for checker formal arguments that are used
as sequences, properties, events, or strings. Specifying a type for formal
arguments used as Booleans or integral expressions usually limits checker
generality.

9.2.2 Checker Contents

Checker contents are similar, but more restricted than those of a module. For
example, checkers cannot contain declarations of modules, interfaces, programs,
and packages. Modules, interfaces, and programs cannot be instantiated inside
checkers. 4 Also general purpose always procedures are deprecated in checkers and
should not be used. 5 Consult the LRM for the exhaustive definition of the constructs
allowed in checkers.

4 The LRM is not clear about placing immediate assertions in checkers. In any case it should be
safe to place immediate assertions in action blocks of concurrent assertions.
5 In the SystemVerilog 2009 standard only general purpose always procedures have been allowed
in checkers. But the SystemVerilog 2012 standard introduced specialized always procedures in
checkers and the general purpose always procedure has been deprecated.