Assertion System Functions and Tasks - SVA: The Power of Assertions in SystemVerilog - page 141

Example 7.16. Verify the following implementation of a flip-flop:

always @( posedge clk)
if (en)q<=d;

Solution:

a_ff: assert property (@( posedge clk)
nexttime q == $past(d,, en));

t

Efficiency Tip. $past(..., n, ...) is not efficient for big delays n .Itis
recommended to minimize the number of calls of $past , and to avoid calling it
whenever it is not essential. The width of the expression e in $past(e, ...) is not
critical in simulation, but may significantly affect FV performance: every additional
bit in e introduces performance penalty.
Example 7.17. Given the definition:

logic check;
logic [31:0] a, b, c;
assertion

a1: assert property (@( posedge clk) ##1 check |-> $past(c) ==
$past(a) + $past(b));
is better to rewrite as:

a2: assert property (@( posedge clk) ##1 check |-> $past(c == a +
b));
In fact, assertion a1 has three invocations of $past , while a2 has only one.
Assertion a1 has 32 * 3 D 96 application of $past to individual bits, while a2 is
applied to a single bit—the result of comparison. This is essential for FV and helps
in simulation. t

Sampled Value Functions Outside Concurrent Assertions. $past and other
sampled value functions, except for the global clocking future value functions
described in Sect. 7.2.2 , are not limited to concurrent assertions. However, it should
be understood that the values returned are based on the sampled values of the
argument, as discussed in the following example.

Example 7.18. The following code

logic a, b;
always @( posedge clk)
a <= $past(b);