In reply to ben@SystemVerilog.us:
Yup, got it. This assertion will fail because I am highlighting infinite consecutive repetition of signal-s1. For this, we need to use first_match, right? But I have read somewhere probably in some thread here or on any website that we use this construct if this problem occurs on the antecedent side. Could you tell me about this?
Another thing, I just observed. The example you mentioned, according to that assertion will fail at the 7th cycle when done will be asserted. But our requirement is something else, I guess. It’s been said that after 4th cycle assertion should pass.
property check;
int count=0;
@ (posedge clk)
$rose(enable) |->
(s1,count=count+1)[*1:$] ##1(count == no_of_repetition) ##0 $rose(done);
endproperty
I think this one is doable and we don’t need to use first_match.