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

sequence s_3_in_a_row( bit signal, goal);

1

(signal == goal)[ * 3];

2

endsequence

3

property p_illegal_causality;

4

bit l_v;

5

(start, l_v = a)

6

|-> s_3_in_a_row(.signal(b), .goal(l_v)).triggered;

7

endproperty

8

In Line 7 , this code attempts to pass the value of local variable l_v into an instance
of sequence s_3_in_a_row to which sequence method triggered is applied. The
intended meaning of the code is that if start occurs, then b must equal a now
and b must now have held this value for at least three cycles, including the current
one. This encoding is forbidden by SystemVerilog because it requires evaluation of
s_3_in_a_row to be aware of the future value of a when looking for a match to
satisfy the instance to which triggered is applied (cf. Exercise 16.8 ).

16.5.2 Output with Local Variables

Values of local variables can be output only from instances of named sequences.
There is no notion of passing values of local variables out of instances of named
properties because:
￿ The evaluation of a property or subproperty is terminal in the sense that there is
no ensuing thread of assertion evaluation.
￿ In general, property evaluation has no well-defined finite endpoint.
There are two mechanisms for passing the value of a local variable out of an
instance of a named sequence. The first is to pass the value out through an argument
local variable of direction output or inout . The following rules apply to named
sequences with argument local variables of direction output or inout and their
instances:
1. The entire actual argument bound to an argument local variable of direction
output or inout must itself be a local variable to whose type the type of the
formal argument can be cast. The actual argument is called the receiver local
variable for the corresponding formal argument.
2. In a given sequence instance, a local variable may not be referenced more than
once as a receiver local variable.
3. The structure of the declaration of the named sequence must guarantee that
each argument local variable of direction output or inout be assigned at the
completion of a match of the instance of the named sequence. 10
4. The instance of the named sequence must not admit empty match.

10 In particular, each argument local variable of direction output or inout must flow out of every
match of the sequence expression that results from the body sequence expression of the declaration