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

￿ trig and cond do not have default actual arguments, hence the user must supply
valid arguments there.
￿Both clk and rst can be inferred from the context because the inference functions
are used as default actual arguments.
￿ The arguments start_tick and end_tick have the typical default value of 1 .If
used as in the following instantiation example, the property will check that cond
holds true at the next clock tick after trig holds true.

A simple instantiation of property time_interval_p is illustrated in the next
example.

Example 24.7. property -based checker instantiation
module m( input logic clk, reset_n, load,
input logic [3:0] r1,
output logic [3:0] r2);
default disable iff reset_n;
always @( posedge clk) begin
if (!reset_n) r2 <= 'b0;
else if (load) r2 <= r1;
loaded_r2: assert property (time_interval_p(
$past(load), r2 == $past(r1))) else
$error("r2 not loaded correctly by r1");

end
endmodule

t

Except for the arguments that are used in the actual verification, all other ones use
default values. The clock and the disabling condition are inferred from the always
procedure and from the default disable iff declaration, respectively.

24.3.4 A Checker-Based Temporal Checker

The final example illustrates the full power of a checker -based temporal checker
definition. We show a modified form of checker assert_handshake discussed at
the beginning of this chapter (Sect. 24.1 ), but for reasons of brevity we include only
those portions of the code that illustrate the differences.
The interface of the new checker is now as follows 1 :

Example 24.8. assert_handshake checker definition
import std_ovl_defines:: * ;
checker assert_handshake (
sequence req, sequence ack,
event clk = $inferred_clock,
untyped reset = $inferred_disable,
//elaboration-time constants:

1 Port enable is not used in the OVL checker, so it is not included in this description.