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

1 checker c_seqprotocol(start, complete,
2 dataIn, dataOut,
3 event clk = $inferred_clock,
4 untyped rst = $inferred_disable);
5 default clocking @clk; endclocking
6 default disable iff rst;
7
8 property match(x, y);
9 x |=> !x until_with y;
10 endproperty : match
11
12 var type (dataIn) last_dataIn;
13
14 always_ff @clk
15

if (start)

last_dataIn <= dataIn;

16

17
18 a_initial_no_complete:
19

assert property ($fell(rst) |-> !complete until_with start);

20
21 a_seq_data_check: assert property (
22 complete |-> dataOut == last_dataIn );
23 a_no_start: assert property (match(start, complete));
24 a_no_complete: assert property (match(complete, start));
25 endchecker : c_seqprotocol

Fig. 9.4 Sequential protocol specification as a checker

9.1.2 Sequential Protocol as Checker

To resolve the problems of assertion packaging and modeling, SystemVerilog
has a special construct called checker . We introduce checkers informally in this
section on the example of the sequential protocol specification, while providing
detailed description in the section that follows. Figure 9.4 shows the checker-based
implementation of the sequential protocol.
The checker syntax is similar to that of the module, but it has several important
differences: instead of module — endmodule the keywords checker — endchecker
are used (Lines 1 - 25 ). By default all checker ports are input, and therefore we
do not explicitly specify their direction (Line 1 ). The checker instantiation follows
the substitution semantics similar to that of sequences and properties, therefore the
explicit type specification of the checker ports is not necessary. For this reason we
omit the type specification of the ports start , complete , dataIn and dataOut ,
and their type is inferred from the checker instantiation. The semantics of checker
input formal arguments is similar to the semantics of property arguments, and
almost all formal argument types allowed in properties are also allowed in checkers,