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

property even_odd ( property p, q);

1

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

2

endproperty

3

Fig. 17.6 Recursive encoding of even-odd checks

property even_odd_stall( property p, q);

1

if (stall) nexttime even_odd_stall(p, q)

2

else

3

p and nexttime even_odd_stall(q, p);

4

endproperty

5

Fig. 17.7 Recursive encoding of even-odd checks with stall

property p_fifo_data_check;

1

dataType data;

2

bit [0:$clog2(MAX_OUTSTANDING)] numAhead;

3

(start, data = dataIn, numAhead = outstanding)

4

##1 (numAhead > 0 ##0 complete[->1], numAhead--)[ * ]

5

##1 (numAhead == 0 ##0 complete[->1])

6

|->

7

dataOut == data;

8

endproperty

9

Fig. 17.8 Encoding of FIFO protocol data check using local variables

Suppose now that we want to modify the check so that cycles in which stall is
true are skipped—i.e., no new check of p or q is started in such a cycle and it does
not count for the reckoning of even and odd cycles. Figure 17.7 shows an encoding.
The remaining examples of this section give recursive encodings of several
checks for the FIFO protocol from Sect. 15.3 . Recall that the FIFO protocol
requires dataIn at an occurrence of start to equal dataOut at the corresponding
occurrence of complete . According to FIFO ordering, the nth occurrence of start
corresponds to the nth occurrence of complete . An auxiliary variable outstanding
(see Fig. 15.6 ) keeps track of the number of outstanding transactions, i.e., the
difference between the number of preceding occurrences of start and the number
of preceding occurrences of complete . The encoding of the FIFO protocol data
check property from Fig. 15.9 is repeated here for reference in Fig. 17.8 .
A drawback of this encoding is that the management of the local variable
numAhead in Lines 5 and 6 involves a somewhat tricky pattern. Figure 17.9 shows a
recursive encoding of the same property.
p_fifo_data_check_recur has argument local variables data and numAhead .
The instance of this property in Line 2 initializes data to the value of dataIn and
numAhead to the value of outstanding .Line 8 advances to the nearest strictly
future occurrence of complete . At that point, if numAhead is zero, then dataOut