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

typedef bit [0:$clog2(MAX_OUTSTANDING)] counterType;

1

property p_fifo_data_check( local input counterType numAhead);

2

dataType data = dataIn;

3

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

4

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

5

|->

6

dataOut == data;

7

endproperty

8

property p_fifo_all_checks;

9

counterType outstanding, nextOutstanding = '0;

10

(

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

endproperty

23

initial

24

a_fifo_all_checks: assert property (

25

p_fifo_all_checks

26

);

27

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

17.2 Retry Protocol

This section presents a write protocol with retry. The protocol involves complex
checks that are handled well with recursive properties. The protocol is a variant
of the retry protocol from Sect. 16.12.17 of the SystemVerilog 2012 LRM. The
LRM version includes transaction tags, which allow multiple write transactions
to be in flight concurrently, distinguished by their tags. Tags have already been
discussed at a high level in the Tag Protocol of Sect. 15.4 . The tags are orthogonal
to the retry, so they have been abstracted away for simplicity. As a result, the
present protocol is sequential, meaning that a new transaction cannot start while
the previous transaction remains in flight. We assume that the protocol is clocked at
posedge clk , as specified by default clocking . Here are the English rules:

1. start , dataValid , complete , and retry are signals of type logic . data is a
signal of the integral type dataType .
2. Start of a write transaction is signaled by occurrence of start .
3. A write transaction has between one and MAX_BEATS data beats, where
MAX_BEATS is a positive integer parameter. Data for a single beat is of type
dataType .