SystemVerilog Concurrent Assertion Sequence Dynamic Length

Question

I have an array of length x. A signals output for a given testbench will be each value in the array in its respective order from 0:x-1.

In my problem in particular, the array is filter coefficients and the testbench is the impulse response. The test needs to be self-checking, which will require a sequence with dynamic length, as the coefficients will change from test to test.

The sequence I would like should look something like this:

always @(posedge clk) begin
  assert_sequence : assert property (    
        (data_out == array_1[0])
    |=> (data_out == array_1[1])
    |=> (data_out == array_1[2]) 
    |=> (data_out == array_1[3]) 
    |=> (data_out == array_1[4]) 
    |=> (data_out == 0) ) 
      $info("Seen the sequence");
    else
      $error("Sequence was incorrect");  
  end

Can this be possible to do dynamically? I've tried a genvar for loop but it throws errors. I've searched the forums and can't find anything that meets my requirement like so.

Possibly something like this could give the right answer?

    always @(posedge clk) begin
  assert_sequence : assert property (    
        (data_out == array1[0][0])

  for(genvar i = 1; i < 5, i++) begin
    |=> (data_out == array1[i])
  end

    |=> (data_out == 0) ) 
      $info("Seen the sequence");
    else
      $error("Sequence was incorrect");  
  end

Answer 1

Comments are very useful and had notes of the direction I have taken to resolve this. Just revisited the problem and came up with this un-elegant solution.

for(genvar i = 1; i < 5; i++) begin
  always @(posedge clk) begin
    assert_sequence : assert property (
                                       (data_out == array1[0])
                               |-> ##i (data_out == array1[i])
                               |-> ##(5-i) (data_out == 0) //This line prevents error 
                                                                  //as my coefficients are symmetric
                                    )
      $info("Impulse response Coefficient %0d seen", i);
  else
      $error("Impulse response Coefficient %0d not seen", i);
  end
end

This code creates multiple assertions, and describes that when I see the first coefficient, in i clock cycles I expect to see the (i+1) coefficient, and due to my problems symmetry, in (5-i) clock cycles I will see a 0.

Answer 2

As stated, SVA is probably not the natural choice here. However, indeed an interesting problem so had a little think:

Have you tried using recursive properties? Something along the lines of:

property check_sequence(coefficients);
  (data_out == coefficients[0]) ##0
    ((coefficients.size() == 1) or 
     (##1 check_sequence(coefficients[1:coefficient.size()]));
endproperty

assert_label: check_sequence(array_1);

would still need a trigger - not specified in the original q.

Whether it's the most efficient or readable solution is another matter.