SystemVerilog Assertion consecutive repetition for overlapping sequences

Question

I have a specification as follows :

"Check that 'valido' is not asserted when 'validi=1' for only two, one or zero consecutive clk cycles."

the following assertion FAILS (n-3 times) on a sequence of 111..1 :

assert property (@(posedge clk) disable iff (rst) validi[*0:2] |=> !valido);

I guess the problem is in my property, as it does not cover the case of overlapping sequences (?). Is there a way to write a property which would behave right?

Answer 1

Your assertion checks if valido is LOW when validi is HIGH for three consecutive clock cycles, so it is wrong. It will not work even if you change the trigger condition to validi[*0:1] due to overlapping sequences as you guessed.

I don't have a fix in that coding style, but a solution can be built using $past similar to the one on Verification Academy*.

assert property (@(posedge clk) disable iff (rst) 
    ($past(!validi, 0) || 
     $past(!validi, 1) || 
     $past(!validi, 2)) |=> !valido);

Now the assertion expects valido to be LOW if validi is LOW at least one of the last three clock cycles.