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

Since both d and ptr_copy are automatic, their values are captured at the invocation
of a14 . The reference to store still uses Preponed region values in the time step of
posedge clk ,but ptr_copy holds the value that ptr had when the assignment to
store was made in the preceding line of the procedure.

t

Another good option exists to control whether a procedural assertion uses
Preponed region values of static variables or captures their values at invocation
of the assertion. By using const cast, as in const '(v) , the value of variable v
is captured when procedural execution reaches the assertion, and this value is used
throughout that evaluation attempt, regardless of the way v may be updated. In this
way, a static variable can be treated as automatic in assertion evaluation without
having to create an auxiliary automatic variable.

Example 14.15. Use of const cast for a static variable:

always @(ev) begin
automatic dataT d = pipeline.pop_front();
store[ptr] = d;
a15: assert property (@( posedge clk) store[ const '(ptr)] == d);
ptr = next_ptr(ptr);
end
By using const cast for static variable ptr , the behavior of assertion a15 is the
same as a14 .

t

The same rules apply to references to automatic variables and const cast
expressions in the action blocks of procedural concurrent assertions. The values
of automatic variables and const cast expressions are captured when the assertion
is invoked, and these values are used in the assertion evaluation and when any action
blocks execute for that attempt. Recall that at the time of execution of action blocks,
references to static variables use Reactive region values, not Preponed region values.

14.4 Assertions in a For-Loop

So far we have seen how clocks and values are applied to procedural assertions.
In this section, we show a form in which an assertion is replicated and activated
under nested conditions. This form is well suited and natural to express a variety of
scenarios and is based on dynamic values of the surrounding procedural conditions.

Example 14.16. Replication of assertions using for-loop:

logic treg;
logic [3:0] dreg;
logic [7:0] tr;
//...
always @( posedge clk) begin
if (treg) begin
for ( int i=0;i<4;i++) begin