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

property p_fifo_data_check;

1

start |-> p_fifo_data_check_recur(dataIn, outstanding);

2

endproperty

3

property p_fifo_data_check_recur(

4

local input dataType data,

5

local input bit [0:$clog2(MAX_OUTSTANDING)] numAhead

6

);

7

##1 complete[->1]

8

|->

9

if (numAhead == 0)

10

dataOut == data;

11

else

12

p_fifo_data_check_recur(data, numAhead--);

13

endproperty

14

Fig. 17.9 Recursive encoding of FIFO protocol data check

is compared to data (Line 11 ). Otherwise, the evaluation recurs, decrementing
numAhead in the actual argument in Line 13 . The overall encoding of Fig. 17.9
occupies more lines than the nonrecursive encoding, but the pattern in the body of
the recursive property (Lines 8 - 13 ) may be more accessible than the trickier pattern
in Lines 5 and 6 of the nonrecursive encoding.
Figure 17.10 is a copy of Fig. 15.15 for reference. It shows the encoding
from Sect. 15.5 of all of the FIFO protocol checks using only local variables.
This encoding is subtle in the use of two local variables of type counterType
in p_fifo_all_checks . Because outstanding is managed as a local variable
and updated in the repetition of Lines 11 - 15 , it is necessary to have it shadow
nextOutstanding so that the appropriate value will still be available for use in
the consequent (Lines 17 - 22 ).
With recursion, there is more flexibility in where local variables are updated.
As a result, the shadow variable can be eliminated. A recursive encoding is given in
Fig. 17.11 . Property p_fifo_data_check_recur is the same as in Fig. 17.9 , except
that the user-defined type counterType is used for numAhead . The main recursive
property is p_fifo_all_checks_recur . It has a single argument local variable,
outstanding , which is initialized to '0 in the instance in Line 32 .Line 16 advances
to the next occurrence of start or complete . Lines 18 - 21 of the consequent update
outstanding and, in the next cycle, recur with the new value of outstanding .
This part of the code keeps the ongoing check running. Rules of local variable flow
(see Sect. 16.4 ) ensure that the new value of outstanding from Line 19 is not
visible in Lines 23 - 28 . This is how the shadow variable is eliminated. Lines 23 - 28
perform the same checks as Lines 17 - 22 of the nonrecursive encoding. Again, the
overall number of lines is a bit greater in the recursive case, but the code patterns
are easier to understand.