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

7.2.1.4 Changed and Stable

Sampled value function $changed(e, @clk) returns true iff the past value of e
is different from its current value, and false otherwise. The sampled value function
$stable(e, @clk) returns true if the past value of e is identical to its current value,
and false , otherwise. More precisely,

$changed(e, @clk) $past(e,,,@clk)!== $sampled(e) .
$stable(e, @clk) $past(e,,,@clk)=== $sampled(e) .
$stable(e, @clk) is the same as !$changed(e, @clk) . $changed and $stable
compare the past value with the current sampled value of the expression.
As in other clocked sampled value functions, the clock event argument is optional
and if omitted, its value is inferred from the context (Sect. 7.2.1.5 ).

Example 7.23. For the timing diagram shown in Fig. 7.2 , system function
$changed(a, @( posedge clk)) returns true for time steps 30 < t 60 and
70 < t 80. For all other time steps, it returns false .Thevalueof $stable is the
inverse.

t

Example 7.24. If e remains x , $stable(e) is true. If e changes from 0 or 1 to either
x or z , $stable(e) is false.

t

Example 7.25. Signal sig should be always stable.
Solution: One can attempt to write this assertion as:
a1_wrong: assert property (@( posedge clk) $stable(sig));
but this implementation is wrong . The problem is, as usual, with clock tick 0. At
clock tick 0 $stable returns true only if the new value of sig coincides with its
initial value. Therefore, assertion a1_wrong checks that sig always preserves its
initial value. As an illustration, consider the case when sig is of type logic , and
when it is not explicitly initialized—the most common case in practice. In this case,
assertion a1_wrong succeeds iff sig is always x , apparently not what was intended
to check. As always in such cases, the solution is to delay the assertion execution:
a2: assert property (@( posedge clk) nexttime $stable(sig));

Discussion: Assertion a2 is still problematic: it checks signal stability only on rising
clk . In many cases in practice it is desirable to ensure absolute signal stability, for
example, in verification of clock domain crossing (Sect. 1.2.3 ). We postpone this
discussion until Sect. 7.2.2 . In this section, we consider signal stability only relative
to some specific clock.

t

Example 7.26. We are now ready to implement the assertion from Example 6.11
with the help of a sampled value function: “ sig toggles every cycle: 0101...or
1010...”.

Solution:
a_toggle: assert property (@( posedge clk) ##1 $changed(sig));

t