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

10 20 30 40 50 60 70 80 90 100

clk

start

INV PRG INV READ

ttype

ttype 20 undefined

undefined

INV

l -

undefined undefined

PRG

l ttype 40

-

Fig. 16.9 Waveform for transaction type check

threads. In general, a local variable assigned in a thread of evaluation may be
referenced later in that thread or in a descendent of that thread. However, System-
Verilog provides no mechanism for externally referencing or cross-referencing a
local variable. One evaluation attempt cannot reference the copies of a local variable
from another evaluation attempt. Similarly, a subevaluation thread cannot reference
updates to a sibling's copy of a local variable. If the siblings are subsequence
evaluations that later join (e.g., subevaluations of operands of sequence and or
intersect ), then structural rules described below determine whether or not the
thread of evaluation that proceeds from the join can reference the updates from one
of the siblings. Hierarchical references to local variables are illegal.
As a simple example to illustrate these ideas, suppose ttype is valid with start
and that if there is an occurrence of start with ttype == INV or ttype == PRG ,
then at the next two occurrences of start , ttype must not have the same value that
i t has at the current occurrence of start . This check can be coded as

property p_ttype_check;

1

transType l_ttype;

2

(start && (ttype == INV || ttype == PRG), l_ttype = ttype)

3

|=> start[->1:2]

4

|-> ttype != l_ttype;

5

endproperty

6

Consider the waveform shown in Fig. 16.9 . The evaluation attempt of property
p_ttype_check that begins at time 20 observes an occurrence of start together
with ttype == INV , and so it stores INV in its copy of the local variable l_ttype .
This copy of the local variable is represented by the row labeled l_ttype 20 in
the waveform. Another evaluation attempt of p_ttype_check begins at time 40,
observes an occurrence of start together with ttype == PRG , and stores PRG in
its copy of the local variable, which is labeled l_ttype 40 in the waveform. The
evaluation that begins at time 20 sees only l_ttype 20 , not l_ttype 40 . At time
40, this thread observes the first subsequent occurrence of start , and the check