Mechanics of Local Variables - SVA: The Power of Assertions in SystemVerilog - page 376

sequence s_skip(

1

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

2

);

3

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

4

##1 (numToSkip == 0 ##0 complete[->1]);

5

endsequence

6

property p_fifo_data_check;

7

dataType data;

8

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

9

(start, data = dataIn, numAhead = outstanding)

10

##1 s_skip(.numToSkip(numAhead))

11

|->

12

dataOut == data;

13

endproperty

14

a_fifo_data_check: assert property (p_fifo_data_check);

15

Fig. 16.17 FIFO protocol data check using a subsequence

The usual rules of passing actual arguments to untyped formal arguments apply
in this case: the bit width of numToSkip for a given instance is determined
by the corresponding actual argument, and there is no type checking to ensure
compatibility between the formal and actual argument.

Exception for Sequence Methods

There is an exception to all of the preceding discussion of this section: it does
not apply to a local variable passed to an instance of a named sequence to which
a sequence method ( triggered or ) is applied. SystemVerilog does not allow
the value of a local variable passed into such an instance to be observed by the
instance. 9 This means that the declaration of the sequence must not reference the
corresponding formal argument unless the formal argument has been assigned as
a local variable within the sequence body. This restriction is important for the
preservation of forward progress of time and causality because, in general, it is not
known how the time of assignment to a local variable in the instantiating context
relates to the start time of a match of the sequence to which a sequence method is
applied. For example, the following contrived code is not legal:

9 In addition, a local variable passed to a sequence instance to which a sequence method is applied
must be the entire actual argument passed to the corresponding formal argument and must not be
passed to an argument local variable of direction input or inout .