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

1 bit [0:$clog2(MAX_OUTSTANDING)] outstanding;
2 initial
3 outstanding <= '0;
4 always @( posedge clk)
5

outstanding <= outstanding + $sampled(start - complete);

Fig. 15.6 Encoding of the number of outstanding transactions

nth occurrence of start pairs with the nth occurrence of complete .Herearethe
English rules:

1. start and complete are signals of type logic . dataIn and dataOut are signals
of type dataType .
2. Whenever start is high, dataIn is valid. Whenever complete is high, dataOut
is valid.
3. MAX_OUTSTANDING is a positive integer parameter.
4. start may be high if and only if complete is not high and the number of
preceding occurrences of start minus the number of preceding occurrences of
complete is less than MAX_OUTSTANDING .
5. complete may be high if and only if start is not high and the number of
preceding occurrences of start minus the number of preceding occurrences of
complete is positive.
6. For all n 1,atthenth occurrence of complete ,thevalueof dataOut must
equal the value of dataIn at the nth occurrence of start .

As with the sequential protocol, this specification decomposes into a control part,
governing the signals start and complete , and a data part. The control part of the
specification must keep track of the difference between the number of preceding
occurrences of start and the number of preceding occurrences of complete .
Let us call this difference the number of outstanding transactions . One way to keep
track of this number is to encode an auxiliary variable to store it. Figure 15.6 shows
how this can be done.
Line 1 references the $clog2 system function, which returns the ceiling of the
base-2 logarithm of its argument. This declaration ensures that outstanding has
enough bits to store the number MAX_OUTSTANDING (see Exercise 15.3 ). (Question:
Why is it important that outstanding be able to store MAX_OUTSTANDING ?) The
always procedure updates outstanding , incrementing it whenever start occurs
and decrementing it whenever complete occurs. Of course, if start or complete
does not obey the control part of the specification, then outstanding may overflow
or underflow.
Using outstanding , the control part of the FIFO protocol specification can be
encoded as shown in Fig. 15.7 . Without using local variables, the various values of
dataIn for the outstanding transactions need to be stored in some data structure. A
bounded queue of maximum size MAX_OUTSTANDING is a good choice because of the
in-order pairing of corresponding occurrences of start and complete . Figure 15.8