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

10 20 30 40 50 60 70 80 90 100

clk

a

Fig. 7.1 Assertion violation

The situation with resets is different. In assertion

a3: assert property (@( posedge clk) disable iff (rst) a);
the value of rst is not sampled. To make it sampled, it should be specified explicitly:
a4: assert property (@( posedge clk)
disable iff ($sampled(rst)) a);
For further discussion about disable iff , see Chap. 13

t

The main use of system function $sampled is in an action block of concurrent
assertions, as illustrated in the following example.

Example 7.9. Assertion

a1: assert property (@( posedge clk) a)
else $error("Error: a = \%b.", a);
is violated at time 40 for the waveform shown in Fig. 7.1 (recall that in the assertion
body the sampled value of a is used, and it is 0 at time 40). But the issued error
message will be Error:a=1. The reason is that the action block is executed
in the Reactive region (Sect. 4.4 ) when the value of a is already 1. To make the
reporting consistent, the function $sampled has to be explicitly invoked in the action
block:

a2: assert property (@( posedge clk) a)
else $error(''Error:a=\%b.'', $sampled(a));
Note that this rule is applicable to action blocks of concurrent assertions only.
Specifying sampled values in action blocks of immediate or deferred assertions will
produce inconsistent error messages because these assertions do not use sampled
values.

t

7.2.1.2 Past Sampled Values

Sampled value function $past(e, n, en, @clk) has the following arguments:
￿ e — an integral expression.
￿ n 1 — a constant expression specifying the number of clock ticks (delay).
￿ en — a gating expression for the clocking event.
￿ clk — a clocking event.