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

outstanding is declared as a local variable, then any assignment to it is imme-
diately visible to subsequent parts of the sequence or property. Thus, the present
encoding uses nextOutstanding to compute the new number of outstanding
transactions, and outstanding is assigned the old value of nextOutstanding
just before nextOutstanding is updated. The result is that the local variable
outstanding has the same timing as the static variable from Sect. 15.3 . Of course,
the local variable outstanding can be eliminated from p_fifo_all_checks (see
Exercise 15.8 ). An alternative encoding using recursive properties also avoids the
use of two local variables (see Fig. 17.11 ).

15.6 Tag Protocol Revisited

This section shows two alternative encodings of the tag protocol control and data
checks using local variables. One uses a single-bit auxiliary static variable, and the
other requires no auxiliary static variable. These encodings also do not rely on the
existence of the small bound, MAX_ACTIVE , on the number of active transactions.

15.6.1 Tag Protocol Using a Single Static Bit

An encoding of the tag protocol control and data checks using local variables and
a single-bit auxiliary static variable is shown in Fig. 15.16 . It is unlikely that this
encoding is supported in current formal verification tools because assignment to the
static variable is done within a task that is called from within a property. Neverthe-
less, there is nothing in the encoding that is essentially beyond the capabilities of
formal verification tools. Its simplicity and elegance stand in contrast to the more
cumbersome data management of the encodings that rely on MAX_ACTIVE (e.g., as
shown in Fig. 15.14 and explored in Exercise 15.9 ).
Property p_start_and_data_checks captures the values of tagIn and dataIn
in the local variables tag and data whenever start occurs (Line 11 ). Lines 14 - 16
check that, beginning in the next cycle, there is not another occurrence of start
with the same tag until after the nearest occurrence of complete with the same
tag. These lines enforce the rule that an active tag cannot be reused, as specified
in Rule 4 of the tag protocol. When the corresponding complete occurs, Line 19
compares dataOut with the local variable data . This comparison performs the data
check specified in Rule 7 of the tag protocol.
It remains to explain how this encoding performs the check specified in Rule 5 :
complete may occur only if tagOut is an active tag. To gain some insight into why
checking Rule 5 is more difficult than checking the Rule 4 , it is helpful to note that
there is an incomplete symmetry between start and complete in the tag protocol.
The symmetry can be described by the following statements: