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

￿ gating_type is omitted for the same reason as
clock_edge —the actual clocking event provided for clk can contain iff
enabling condition.
The formal arguments clk and reset were placed after the arguments that do
not have defaults. This simplifies instantiation of the checker when all arguments
use default values. The type of reset is left unspecified (the keyword untyped )to
provide more flexibility as to the kind of the actual reset expression.
The default value constants for the arguments are no more 'defines , but instead
they are constants picked up from package std_ovl_defines as enum type values.
The type for req and ack is specified as sequence to allow Booleans and
sequences, but prohibit supplying a property expression as the actual argument. This
makes the checker more general, eliminating the need for modeling code to reduce
a complex temporal behavior to a Boolean expression.
The body of the checker has to be modified to comply with restrictions on
modeling code in checker constructs, and to use all the new features that help
implementing and using checkers. The body of the checker -based checker is shown
next. Refer to the OVL library to compare with the original checker body [ 10 ].
Only those portions as in the example of the original checker are shown that
illustrate the differences with the original checker. The following piece of code
shows the transformation needed in the modeling code of the checker.
Example 24.9. Body of assert_handshake checker
'ifdef ASSERT_ON
bit first_req = 1'b0;
function logic setFirstReq();
if (!reset_n) return 1'b0;
if ((first_req ^ first_req) == 1'b0)
return s_req.triggered;
return 1'b0;
endfunction : setFirstReq
always @(clk) first_req <= setFirstReq();
Variable first_req is used in a property in the following code fragment:
property ASSERT_HANDSHAKE_ACK_MIN_CYCLE_P;
req |-> not s_eventually [0:min_ack_cycle] ack;
endproperty
property
ASSERT_HANDSHAKE_ACK_WITHOUT_REQ_FIRST_REQ_P;
(##1 ack) implies
(first_req or req.triggered);
endproperty
// other properties ...
// this remains as before
case (property_type)