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

dreg[i] <= tr[i + 1];
c16: cover property (dreg[i] ##[1:8] tr[i + 1]);
end
end
end
Four evaluation attempts of c16 are initiated when the for-loop gets executed, each
with a different value of index i ,from 0 to 3 . Following their invocations, the
inferred clock, posedge clk , drives each evaluation attempt to progress and finish
independently of the others. Since variable i is an automatic variable, its value is
captured separately at each invocation of c16 and used throughout the respective
evaluation attempt. Thus, c16 behaves like four covers:
always @( posedge clk) begin
if (treg) begin
for ( int i=0;i<4;i++) begin
dreg[i] <= tr[i + 1];
end
c16_0: cover property (dreg[0] ##[1:8] tr[1]);
c16_1: cover property (dreg[1] ##[1:8] tr[2]);
c16_2: cover property (dreg[2] ##[1:8] tr[3]);
c16_3: cover property (dreg[3] ##[1:8] tr[4]);
end
end
The four covers c16_0 , c16_1 , c16_2 , and c16_3 are started whenever the condition
treg is true for a clock tick of posedge clk . An FV tool may actually split the
single assertion into four equivalent assertions as shown here. This technique is
well suited for formal verification, where analysis of assertion behaviors generally
accounts for evaluation attempts differently than simulation. t

In the following example, the number of for-loop iterations is controlled by signal
count , resulting in a varying number of assertion invocations from clock tick to
clock tick. Again, the value of the automatic variable i is captured whenever c17 is
invoked. 2

Example 14.17. A variable for-loop index replicating of assertions:

always @( posedge clk) begin
if (treg) begin
for ( int i = 0; i < count; i++) begin
dreg[i] <= tr[i + 1];
c17: cover property (dreg[i] ##[1:8] tr[i + 1]);
end
end
end

t

2 FV tools may not be able to handle assertions in procedural loops that cannot be statically
unrolled.