Writing assertion for multidimensional logic

SystemVerilog
, ,
1

Hi,
I have some IO similar to the following

logic[9:0][31:0] a;
logic[9:0][31:0] b;
logic c;

I would like to write assertion so b is a delayed 8 cycles after c is 1.
I come up with a few solutions below:

property one;
  c |-> ##8 (b == $past(a,8));
endproperty
a_one: assert property(one);

or

generate
  for(genvar i=0;i<10;i++) begin
    property two[i];
      c |-> ##8 (b[i][31:0] == $past(a[i][31:0],8);
    endproperty
    two_a[i]: assert(two[i]);
  end
endgenerate

from my understanding,
property one won’t work because “==” doesn’t work with 2-d logic.
property two won’t work because we can’t define property with index.

any idea how to write this assertion?

2

In reply to pepes:

== works with arrays.

And you can declare your property two with an argument outside the generate. Only the assert statement goes inside the generate.