Recursive Properties - SVA: The Power of Assertions in SystemVerilog - page 386

property ranged_until( int unsigned low, high, property p, q);

1

if (low > high) 1'b0 // required k does not exist

2

else

3

ranged_until_recur(low, high, 0, p, q);

4

endproperty

5

property ranged_until_recur(

6

local input int unsigned low, high, cnt,

7

property p, q

8

);

9

if (cnt == high) q // last chance to satisfy q

10

else

11

(

12

(q and (cnt >= low))

13

or

14

(p and nexttime ranged_until_recur(low,high,cnt+1,p,q))

15

);

16

endproperty

17

Fig. 17.4 Recursive encoding of ranged until

property even;

1

( nexttime [0] p) and nexttime odd;

2

endproperty

3

property odd;

4

q and nexttime even;

5

endproperty

6

Fig. 17.5 Mutually recursive encoding of even-odd checks

Line 2 requires low to be at most high .If low exceeds high , then the required k
does not exist and ranged_until fails. Otherwise, ranged_until_recur is called
in Line 4 . This recursive property is an adaptation of the ideas of the encoding of
ranged always from Fig. 17.2 to the recursive form of my_until in Fig. 17.3 . cnt is
an incrementing counter of the cycle number, and it is initialized to 0 by the actual
argument in Line 4 . Lines 13 - 15 mimic Lines 2 - 4 of my_until .Line 13 adds the
condition cnt >= low . This ensures that satisfaction of q discharges the evaluation
only if cnt is in the range [low:high] .Line 10 requires q to be satisfied no later
than the last cycle of this range.
For the next example, suppose that we want to check that p holds in every even
tick of the incoming clock and q holds in every odd tick of the incoming clock, both
reckoned from the start of evaluation.
Figure 17.5 shows an encoding with two mutually recursive properties. Property
even checks p , after alignment with the incoming clock, and in the next cycle calls
property odd . Property odd checks q and in the next cycle calls property even .
Figure 17.6 shows a single recursive property that performs the same check as
property even .