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

If a checker has no arguments, the parentheses may be omitted. endchecker may
be qualified with a label of the checker name, similar to other compound constructs
in SystemVerilog. Specifying the checker name with endchecker is a good idea as
it makes the code clearer, and allows the compiler to check that the beginning and
end of the checker match.

Example 9.1. The following checker consists of a single assertion verifying that
request req is granted at the following clock tick.
checker request_granted(req, gnt, clk, rst);
a1: assert property (@clk disable iff (rst) req |=> gnt);
endchecker : request_granted
In this example, all checker formal arguments are untyped. t

9.2.1 Checker Formal Arguments

9.2.1.1 Argument Direction

Checkers may have input and output arguments. The main use of a checker is to
be an observer to follow the DUT behavior and to verify its correctness. Therefore,
usually a checker has only input arguments, and if no direction qualifier is specified
explicitly, all checker arguments are input by default. However, checkers may have
also output arguments. We discuss them in Sects. 9.5 and 23.5 .

Example 9.2. In the checker declaration in Example 9.1 no argument direction has
been specified. Therefore, all its arguments are input. t

The formal rule for the inference of checker argument direction when it has not
been explicitly specified, is as follows:

￿ If the direction of the first checker argument is omitted, it is assumed to be input.
￿ If the direction of another checker argument is omitted, it is inferred from the
direction of the previous argument.

Example 9.3. Consider the following checker argument declaration:

checker check(a, b, output logic c, d,
input event clk, untyped rst);
Here, a is an input argument because it is the first checker argument, and no
direction has been specified. The second argument b is also input, because it has
no explicit direction, and the previous argument a is input. Argument c is output
because its direction has been explicitly specified. The direction of d is output, as
inferred from the direction of c . The direction of arguments clk and rst is input.

t