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

the declaration of property p_pipeline_data_check . Local variable declarations
follow the same format as other variable declarations in SystemVerilog. Line 3 is
an example of attaching a local variable assignment to a Boolean expression. The
Boolean start is separated from the local variable assignment data = dataIn by
a comma, and the two are enclosed in parentheses. (start, data = dataIn) is a
sequence (not a Boolean) with the following meaning:

￿Thevalueof start is tested when evaluation of the sequence begins.
￿Ifthevalueof start is high, then the value of dataIn is assigned to the local
variable data and the sequence matches at that point.
￿ Otherwise, the sequence fails to match and no assignment to the local variable
data occurs.
If start is high when evaluation of p_pipeline_data_check begins, then the
value of dataIn is assigned to data and the antecedent of the implication |-> in
Line 4 matches. Therefore, the consequent specified in Line 5 must match. Line 5
says that LATENCY cycles should be advanced and then the value of dataOut must
equal the value stored in the local variable data . In summary, when start is high,
the value of dataIn is captured in the local variable data , and this value is compared
LATENCY cycles later to the value of dataOut .
From a data storage perspective, the simulation performance of the encoding with
the local variable should never be worse than that of the encoding using $past .This
is because at most LATENCY threads of evaluation of p_data_pipeline_LATENCY
can be active simultaneously, each with its own copy of the local variable data .
The storage needed for the local variable encoding varies in direct proportion to the
frequency of occurrences of start , while the storage needed for the encoding using
$past is fixed by the parameter LATENCY .

15.2 Sequential Protocol

Now let us switch from a fixed latency pipeline to a protocol that is sequential in
the sense that its transactions do not overlap. This is the same protocol that was
discussed in Sect. 9.1 . We repeat here, with minor modifications, the sequential
protocol description and the module-based implementation without local variables.
In the sequential protocol, there is not a constant latency from dataIn to
dataOut . Instead, a Boolean signal complete determines when dataOut is valid.
Here is the English description:

1. start and complete are signals of type logic . dataIn and dataOut are signals
of type dataType .
2. Whenever start is high, dataIn is valid. Whenever complete is high, dataOut
is valid.