An Apology for Local Variables - SVA: The Power of Assertions in SystemVerilog - page 344

a tag and whose activeTag field is equal to the function's argument tag .Ifthe
tag protocol control checks are satisfied, then there will be at most one such index.
If there is no such index, then the function returns MAX_ACTIVE . These functions
have been declared with automatic lifetime to guard against undesired contention
on their internal loop counter variables in the event of multiple calls in the same
time step.
A similar array can be encoded to store the data values for the active transactions
and used to encode the tag protocol data check in a way that is suitable for formal
verification. See Exercise 15.9 . The complexity of the data management in such
arrays is striking in comparison with the simplicity of the data check using local
variables.

15.5 FIFO Protocol Revisited

This section shows an alternative encoding of the FIFO protocol control and data
checks that uses only local variables.
The encoding with local variables from Sect. 15.3 makes use of only one nonlocal
variable, namely, outstanding as defined in Fig. 15.6 . Thus, the present encoding

1 typedef bit [0:$clog2(MAX_OUTSTANDING)] counterType;
2 property p_fifo_data_check( local input counterType numAhead);
3 dataType data = dataIn;
4 ##1 (numAhead > 0 ##0 complete[->1], numAhead--)[ * ]
5 ##1 (numAhead == 0 ##0 complete[->1])
6 |->
7 dataOut == data;
8 endproperty
9 property p_fifo_all_checks;
10

counterType outstanding, nextOutstanding = '0;

(

11

(start || complete)[->1],

12

outstanding = nextOutstanding,

13

nextOutstanding += start - complete

14

)[+]

15

|->

16

if (start) (

17

(!complete && outstanding < MAX_OUTSTANDING)

18

and p_fifo_data_check(.numAhead(outstanding))

19

) else ( // complete

20

!start && outstanding > 0

21

22 );
23 endproperty
24 initial
25

a_fifo_all_checks: assert property (p_fifo_all_checks);

Fig. 15.15 Encoding of all FIFO protocol checks using only local variables