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?