Procedural concurrent assertions within for loop

SystemVerilog
, ,
1

Hi All,
LRM 2017 Section 16.14.6.1 mentions ::

// Assume for this example that (posedge clk) will not occur at time 0
always @(posedge clk) begin
int i = 10; // My Comment :: Incorrect , should be explicitly declared as static OR automatic here
 for (i=0; i<10; i++) begin
  a1: assert property (foo[i] && bar[i]); // My Comment :: Infers leading clock as @(posedge clk)
 end
end
In any given clock cycle, each of these assertions will result in 10 queued executions.
Every execution of assertion a1, however, will be checking the value of (foo[10] && bar[10]) ,
since the sampled value of i will always be 10, its final value from the previous execution of the procedure

I have a few questions related to it

[Q1] I am not clear on the last line ::

Every execution of assertion a1, however, will be checking the value of (foo[10] && bar[10]),since the sampled value of i will always be 10

Why doesn’t it result in :: (foo[0] && bar[0]) , (foo[1] && bar[1]) , … (foo[9] && bar[9]) ?

My intuition is that the unlooping of for-loop would occur in Active region
whereas the concurrent assertion gets evaluated in Observed region.
Would the value of ‘i’ be 10 in Observed region ?

[Q2] Assume that variables ‘foo’ , ‘bar’ are declared as

logic [9:0] foo , bar ; // 10-bit wide

Essentially foo[10] , bar[10] are invalid indexes.
So won’t (foo[10] && bar[10]) result in ( 1’bX && 1’bX ) i.e 1’bX i.e False ?

[Q3] What if the assumption is not true i.e posedge of clk occurs at time 0 ? What difference would it make ?

[Q4] I want to add a fail action block to ‘a1’ that displays the index ( i.e ‘i’ ) for which the failure occurs. What would the correct way be ?

always @(posedge clk) begin
  for ( int i=0; i<10; i++) begin // 'i' is now automatic
  //  Will the following approach work ?
  a1: assert property (foo[i] && bar[i]) else $display("Failure for foo[%0d] is %1b, bar[%0d] is %1b",$sampled(i),foo[$sampled(i)],$sampled(i),bar[$sampled(i)]); 
  end
end
2

Blockquote
Every execution of assertion a1, however, will be checking the value of (foo[10] && bar[10]),since the sampled value of i will always be 10

Why doesn’t it result in :: (foo[0] && bar[0]) , (foo[1] && bar[1]) , … (foo[9] && bar[9]) ?

Blockquote

// When using a **const cast**, the value of the expression is treated as if it 
// were defined as a constant variable of the same type.
const'(j) // treats the loop iterator j as a constant within the loop.
always @(posedge clk) begin
    // variable declared outside for statement is static (see 6.21)
   int i; // i is a static variable; it retains its LAST value at the end of the loop 
  for (i=0; i<10; i++) begin
     a1: assert property (foo[i] && bar[i]);
     a2: assert property (foo[const'(i)] && bar[i]);
     a3: assert property (foo[const'(i)] && bar[const'(i)]);
  end
end
// Because of the loop, the simulator will produce for each assertion statement 10 assertions. Something like: 
always @(posedge clk) begin
   int i; // static local variable
  for (i=0; i<10; i++) begin ; end // sets the value of i
                            // nothing else 
   a1_0: assert property (foo[i] && bar[i]);
   ...
  a1_9 : assert property (foo[i] && bar[i]);
  a2_0: assert property (foo[0] && bar[i]);
  ...
   a2_9: assert property (foo[9] && bar[i]);
   a3_0: assert property (foo[0] && bar[0]);
  ...
  a3_9: assert property (foo[9] && bar[9]);
end
// In the very 1st (posedge clk), i==0 (its default value). 
// After the 1st (posedge clk), i-==10 (the last iteration)
// At (posedge clk) clocking event , the simulator sees 30 assertions 
//  At the clocking event , the simulation samples the  values foo[i],  bar[i] 
// using the sampled value of "i" (i==0 at init, i==10 after processing of 1st posedge clk).  This explains why
a1_9 : assert property (foo[i] && bar[i]); // is same as 
a1_9 : assert property (foo[0] && bar[0]); // in the 1st clocking event  
a1_9 : assert property (foo[10] && bar[10]); // after the 1st cycle
3

Because of no delay (either #1; or clk cycle delay) located in the fir loop which leads to property check in a simulation tick of 0ns. For loop finishes execution in a single go.

4

Sorry, but your answer does not address the question as to why (foo[i] && bar[i]) becomes (foo[10] && bar[10]) after the 1st cycle.