Checker Libraries - SVA: The Power of Assertions in SystemVerilog - page 541

input clock, reset, enable;
input req;
input ack;
output ['OVL_FIRE_WIDTH-1:0] fire;
//...
'endmodule // ovl_handshake

t

The macros 'module and 'endmodule resolve to either module and endmodule
or interface and endinterface . This distinction is made so that the checker could
also be instantiated in SV interfaces. In either case, the kinds of ports such checkers
are allowed to have impose severe constraints on the deployment of the checker in a
design:

￿ Clock port clock cannot be an event such as edge clk iff en .
￿ Clock, disabling condition reset , and the enabling condition cannot be inferred
from the instantiation context.
￿ The checker cannot be instantiated inside a procedure.
￿ The ports req and ack must be expressions of type logic , they cannot be of type
sequence or property .
The restrictions make the usage of the checker tedious. In particular, the last
item makes the checker less flexible to use because if either the requests or the
acknowledgments are more complex temporal sequences of signal values, additional
modeling code must be added on the outside of the checker instance to detect such
sequences. This code and the checker instance are usually not to be included in the
synthesized code, hence enclosing them between 'ifndef — 'endif compilation
controls becomes necessary.
Before transforming the assert_handshake checker to its checker -based form,
let us review the kinds of checkers and the main characteristics a library should
possess.

24.2 Kinds of Checkers and Their Characteristics

Checkers can be classified according to four criteria:

1. Temporality: combinational (has no clock) vs. concurrent (requires a clock).
2. Encapsulation: checker (or module or interface )vs. property (or let )
based.
3. Packaging: in a Verilog library vs. in a SystemVerilog package.
4. Configurability: Local per-instance vs. global for all instances.