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

@( posedge clk)
(1, l_a = 1'b0, l_b[4] = b) ##0 start ##1 ...
endsequence
Or, in the case of a property by using (1, l_a = 1'b0, l_b[4] = b)|-> ...
or (1, l_a = 1'b0, l_b[4] = b)#-# ... .
Declaration assignments are performed in the order that they appear, so there can
be dependency of the right-hand side of a later assignment on a local variable whose
declaration assignment is performed previously. It is illegal, though, for the right-
hand side of the later assignment to depend on a local variable for which there
is no declaration assignment. Here is an example of legal declaration assignments
illustrating such a dependency:
property p1( byte data);
byte l_byte = data, l_byteMasked = l_byte & mask;
...
endproperty
When the declaration assignments are performed, l_byte is first assigned the value
of data , and then l_byteMasked is assigned the bitwise-and of the value just
assigned to l_byte and the value of mask . The following example shows illegal
declaration assignments:
property p1_illegal;
byte l_byte, l_byteMasked = l_byte ^ mask;
...
endproperty
The declaration assignments are illegal because the right-hand side of the
assignment to l_byteMasked references l_byte , for which there is no declaration
assignment.
The timing of declaration assignments involves some subtlety in the presence
of multiple clocks. The key principle is that a declaration assignment is always
performed after aligning with a leading clocking event. This ensures that the
value stored by the declaration assignment comes from a known sampling point.
If a property has multiple leading clocking events, 3 then separate local variables
are created for each leading clocking event and the corresponding declaration
assignments are performed upon reaching alignment with each of those various
clocking events.
Figure 16.1 shows declaration of a property with a local variable dec-
laration assignment and multiple leading clocks. Suppose evaluation of
p_mult_leading_clks begins at time t 0 . At that time, two copies of l_v are
created. One copy is used in the evaluation of the subproperty on Line 3 and
the other copy is used in the evaluation of the subproperty on Line 5 .The
assignment l_v = e for the first copy is performed in the first time step concurrent
or subsequent to t 0

in which posedge clk1 occurs. Similarly, the assignment

3 According to SystemVerilog 2012, only properties can have multiple leading clocking events.
Sequences always have a unique leading clocking event and so do assertions.