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

and

$past(c, 2,,@( posedge clk)) = 1'bx
etc. As mentioned in the note preceding this example, some FV tools will assume
the past value of all these expressions to be 1'b0 .

t

Example 7.12. Consider the following code fragment.

logic a;
a1: assert property (@( posedge clk) $past(a));
Assertion a1 fails at clock tick 0, since $past(a) returns x —the initial value of a .
This example shows that one should be careful when using $past in assertions
because it may lead to nonintuitive assertion behavior in the initial clock ticks. t

Example 7.13. Each grant gnt should be immediately preceded by a request req .

Solution:

a1: assert property (@( posedge clk) gnt |-> $past(req));

Discussion: What happens if gnt is active at the initial clock tick? If req has not
been explicitly initialized, $past(req) is x or 0 depending on req type, and the
assertion fails. In this case, this is a desired behavior. t

Example 7.14. Gray Encoding: Check that signal sig has a Gray encoding, i.e., its
two consecutive values differ in only one bit.

Solution: Here is the first solution:

a1_wrong: assert property (@( posedge clk)
$onehot(sig ^ $past(sig)));
The result of the exclusive OR ^ operator between the current and the past values
of sig contains ones in the bits that changed. We want to make sure that exactly
one bit of the result is 1. But what happens at the initial clock tick? $past(sig)
will return x , the result of the exclusive OR will also be x , and assertion a1_wrong
will fail in the initial clock tick! To handle the initial situation correctly, we need to
delay the first check of the assertion:

a2: assert property (@( posedge clk)
nexttime $onehot(sig ^ $past(sig)));
Here sig may have any value at the initial clock tick.
Discussion: One can argue that a real-life implementation should take into account
the reset sequence during which no check is performed and therefore no initial delay
is necessary:

a3_problematic: assert property (
@( posedge clk) disable iff (rst) $onehot(sig ^ $past(sig)));
but this is also problematic. For example, if during reset and immediately after it
sig was equal to 0, assertion a3_problematic will fail immediately after reset.