Checkers - SVA: The Power of Assertions in SystemVerilog - page 203

10 20 30 40 50 60 70 80 90 100

clk

rst

sig

Fig. 9.8 Signal stable for two clock ticks

1 checker stable_for_two_ticks(sig,
2

event clk = $inferred_clock, untyped rst = $inferred_disable);

default clocking @clk; endclocking

3

default disable iff rst;

4

5
6 bit toggle = 1'b0;
7 always_ff @clk
8 toggle <= rst ? 1'b0 : !toggle;
9 a1: assert property (!toggle |-> $stable(sig));
10 endchecker : stable_for_two_ticks

This checker works as follows. Variable toggle is initially low, and it becomes
low each time rst is deasserted. Otherwise, at each clock tick the value of toggle
is complemented. Assertion a1 allows sig to change only when toggle value is
high.
For the waveform shown in Fig. 9.8 the value of rst on Line 8 becomes low
at time 30 (recall that the value of rst is sampled in the checker), and in the next
clock tick (time 40) the sampled value of toggle is low. Therefore, at time 40, the
sampled value of sig must be stable: the sampled value of sig at time 30 is the same
as its sampled value at time 40 . At time 50 , the sampled value of toggle becomes 0,
and sig may change in this time step, and so on.

t

Example 9.20. In the checker from Example 9.19 it is illegal to replace

bit toggle = 1'b0;
with

bit toggle;
initial toggle = 1'b0;
Initial procedures in checkers may not contain checker variable assignments (see
Sect. 9.2.2.2 ).

t

There is an additional restriction imposed on checker variable assignments: it is
illegal to reference checker variables in assignments by their hierarchical names.