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

property p_retry_check;

1

dataType l_dataModel [MAX_BEATS];

2

(start, l_dataModel = dataModel)

3

|=>

4

sync_reject_on (start) p_retry_check_recur(dataModel, 0);

5

endproperty

6

property p_retry_check_recur(

7

local input dataType l_dataModel [MAX_BEATS],

8

local input int unsigned i

9

);

10

(dataValid || retry)[->1]

11

|->

12

(dataValid |-> data == l_dataModel[i]) and

13

if (retry)

14

nexttime p_retry_check_recur(l_dataModel, 0)

15

else if (complete)

16

nexttime (

17

!dataValid and

18

if (retry)

19

nexttime p_retry_check_recur(l_dataModel, 0)

20

)

21

else (

22

(i < MAX_BEATS-1) and

23

nexttime p_retry_check_recur(l_dataModel, i+1)

24

);

25

endproperty

26

a_retry_check: assert property (p_retry_check);

27

Fig. 17.14 Recursive encoding of retry protocol checks

then the flow is done. Otherwise, the flow advances a cycle and resets i to zero to
begin the data transfer again.
Figure 17.14 shows a recursive encoding of the retry protocol checks. The
encoding follows closely the flow diagram of Fig. 17.13 . The outer property
p_retry_check corresponds to the whole diagram, beginning from the start
figure. The recursive property p_retry_check_recur corresponds to the subflow
that is downstream from the node “goto dataValid or retry ”. There are three
cycles in the flow diagram, and these correspond to the three recursive instances of
p_retry_check_recur . The cycle on the left of the flow diagram corresponds
to the recursive instance on Line 24 . The smaller cycle on the right of the flow
diagram corresponds to the recursive instance on Line 15 . And the larger cycle on
the right of the flow diagram corresponds to the recursive instance on Line 20 .Note
that management of the counter i is accomplished in the actual arguments to the
instances of p_retry_check_recur . With careful study of these correspondences,
the reader should gain an appreciation for the simplicity of encoding flow diagrams
into sets of properties, where cycles correspond to recursion.