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

property ranged_always( int unsigned low, high, property p);

1

ranged_always_recur(low, high, 0, p);

2

endproperty

3

property ranged_always_recur(

4

local input int unsigned low, high, cnt,

5

property p

6

);

7

if (cnt <= high)

8

(

9

( if (cnt >= low) p)

10

and

11

nexttime ranged_always_recur(low, high, cnt+1, p)

12

);

13

endproperty

14

Fig. 17.2 Recursive encoding of ranged always allowing non-constant range bounds

property my_until( property p, q);

1

( nexttime [0] q)

2

or

3

(( nexttime [0] p) and nexttime my_until(p, q));

4

endproperty

5

Fig. 17.3 Recursive encoding of until

affect the meaning of the range while evaluation of the recursive property was
underway (see Exercise 17.1 ). cnt is an incrementing counter that keeps track of
the number of cycles that have elapsed. Line 8 checks that cnt has not yet exceeded
high . When it does, the recursion ends. When cnt reaches low , checking of p is
caused by Line 10 . The recursive instance in Line 12 increments cnt in the actual
argument expression.
Figure 17.3 shows a recursive encoding of until . Each time evaluation of
my_until begins, either property q must evaluate to true (Line 2 ) or both property
p must evaluate to true and also evaluation of my_until must start again in the
next cycle (Line 4 ). The use of nexttime [0] in Lines 2 and 4 ensures that the
first evaluations of q and p begin after alignment with a tick of the incoming
clock. Satisfaction of q results in satisfaction of my_until without evaluation of the
recursive instance in Line 4 , and so it allows the recursion to stop. Until q is satisfied,
Line 4 must be satisfied, which implies that p must be satisfied. It is possible that q
is never satisfied, in which case p must be satisfied always. Thus, my_until(p,q)
has the same semantics as p until q .
Suppose that we need to check a ranged form of p until q , in which satisfaction
of q must occur within a range [low:high] of cycles from the start of the
evaluation. Let us denote this property p until [low:high] q . Note that this is not
legal SVA code, just a notation. The property p until [low:high] q is satisfied iff
there exists k, low k high , such that q is satisfied in the kth cycle from the
start of evaluation and p is satisfied in every prior cycle from the start of evaluation.
Figure 17.4 shows a recursive encoding of this property.