Procedural Concurrent Assertions - SVA: The Power of Assertions in SystemVerilog - page 309

than the automatic variables. Even though the values of static variables are in
progress during the simulation execution, references to those variables in the
assertion expression use the Preponed region values, following the same paradigm
as all other concurrent assertions. Using Preponed region values is essential to
obtaining a deterministic result. This is due to the fact that continuing temporal
evaluation from one clock tick to the next takes place in its own thread of execution,
which is apart from the execution of the enclosing procedural block.

The value of an automatic variable is captured at the time a procedural
concurrent assertion is invoked.

The semantics for an automatic variable in a procedural concurrent assertion
is, however, to capture its value at the time the assertion is invoked, i.e., when
procedural execution reaches the assertion. The captured value is used for the
variable throughout that evaluation attempt of the assertion.
In the next examples, we assume that store and ptr are static variables and that
ev is an event variable.
Example 14.13.

Automatic variable in a procedural assertion and a timing problem:

always @(ev) begin
automatic dataT d = pipeline.pop_front();
store[ptr] = d;
a13: assert property (@( posedge clk) store[ptr] == d);
ptr = next_ptr(ptr);
end
Each time a13 is invoked, the value of automatic variable d is recorded at that point,
and this value is used to compare to store[ptr] at posedge clk . Since store and
ptr are static variables, their references in a13 use Preponed region values. This
causes a timing problem because ptr will typically have been updated before the
time step of the next posedge clk ,sothevalueof d is compared to the wrong
element of store . t

The following variant solves the timing problem by using another automatic
variable to capture the value of ptr for use in the assertion.
Example 14.14. Automatic variables in procedural assertion:

always @(ev) begin
automatic dataT d = pipeline.pop_front();
automatic ptrT ptr_copy = ptr;
store[ptr] = d;
a14: assert property (@( posedge clk) store[ptr_copy] == d);
ptr = next_ptr(ptr);
end