Stable for n*8 cycles property

Question

I am learning SVA and trying to get my head around this check: data can only change every 8 cycles.

I know I can do that check by adding a counter that counts clock cycles and checking against it that way:

bit[2:0] count;

always @(posedge clk)
begin
    count++;
end

change_n8cycles: assert property (@(posedge clk) $changed(data) |-> count == 0);

However, I'm interested in a way to do that with only SVA. So far, I was thinking of something like that (which doesn't compile)

property change_n8cycles(valid, ready, data);
    @(posedge clk)
    $changed(data) |=> $stable(data)[*7] ##1 ($stable(data)[*8])[0:$] ##0 $changed(data);
endproperty : change_n8cycles

I feel there is an elegant way using an approach similar; or using recursive properties. However, I couldn't find it.

Answer 1

I would propose to use local variable in order to verify that

property change_n8cycles(valid, ready, data);
int lv_cnt;
@(posedge clk)
($changed(data), lv_cnt=0) ##1 ($stable(data), lv_cnt=lv_cnt+1)[*1:$] ##1 $changed(data) |-> lv_cnt == 8;
endproperty

Or use some modeling layer

always @(posedge clk) begin
  if($changed(data))
    count=0;
  else
    count++;
end

property change_n8cycles(data);
  @(posedge clk)
  $changed(data) |-> $past(count) == 8;
endproperty