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

needs to keep track of the number of outstanding transactions internally by using
local variables. This encoding is shown in Fig. 15.15 .
The style of this encoding is somewhat more complicated than those shown in
Sect. 15.3 , although each of its parts corresponds to a part of the encoding using
local variables that appears in that section. This encoding uses a typedef on
Line 1 to provide the type counterType that simplifies the declarations on Lines 2
and 10 . The top-level property p_fifo_all_checks is responsible for accounting
for the number of outstanding transactions, performing the control checks, and
calling property p_fifo_data_check to perform the data check. The accounting
of the number of transactions is done in the repetition in Lines 11 - 15 , and this
approach, which will be explained in more detail below, assumes that there is
only one evaluation attempt of p_fifo_all_checks running. For this reason the
assertion a_fifo_all_checks on Line 24 appears in an initial procedure. See
Exercise 15.7 .
The data checking property p_fifo_data_check is very similar to the property
of the same name from Sect. 15.3 , so we focus on the differences. In Line 2 ,
numAhead is declared as a formal argument. The keywords local input in this
declaration specify that the formal argument numAhead is in fact a local variable
that will receive an initial value from its actual argument. p_fifo_all_checks
computes the value of outstanding in Line 13 and passes it in to numAhead through
the instantiation in Line 19 . In all other respects, numAhead behaves the same here as
it did in Sect. 15.3 .InLine 3 , the local variable data is declared, and the declaration
includes a declaration assignment to the value of dataIn . The meaning of this
assignment is that whenever evaluation of p_fifo_data_check begins, the copy
of data for that evaluation begins with the value of dataIn at that time. Line 17
guarantees that p_fifo_data_check is called only when start occurs, so dataIn
is valid whenever the declaration assignment of Line 3 is performed. The rest of
p_fifo_data_check is identical to the encoding from Sect. 15.3 and behaves the
same.
The structure of p_fifo_all_checks is an implication whose antecedent is an
unbounded repetition (Lines 11 - 15 ) and whose consequent enforces the control
checks (Lines 18 and 21 ) and the data check (Line 19 ). There are two local variables,
outstanding and nextOutstanding , both declared in Line 10 . The reason for
having two local variables will be explained below. Note that nextOutstanding is
declared with a declaration assignment to the value '0 . This assignment corresponds
to the nonblocking assignment on Line 3 of Fig. 15.6 .
The repetition in Lines 11 - 15 uses a pattern similar to the decrementing counter
from Line 5 of Fig. 15.9 . In this case, successive iterations of the repetition match
each time a start or complete occurs. The assignments in Lines 13 and 14
are executed for each iteration and are performed in the order that they appear.
The assignment to nextOutstanding is analogous to Line 5 of Fig. 15.6 and
accomplishes the basic accounting of the number of outstanding transactions.
The reason for using the two local variables is that when outstanding is
declared as a static variable as in Sect. 15.3 , references to it from within sequences
and properties resolve to the sampled value for that cycle. On the contrary, when