@hdlcohen ,
Thank you for your explanation. I got your point.
Usage of go-to repetition of 1([->1]) with infinete continuous repetition [*1:$]instead of infinite non-continuous repetition ([=1:$]) usage.
N = 3 ___________________________________
a : __| |__
__ __ ____
b : __| |__| |________| |_______________
v_cnt : 1 2 3 3
|[->1]|[->1]| [->1] |
| [*1:3] | ##[0:$] |
^...................................*
Then, your property should be precisely like below.
property p_pulse_cnt_2 (N);
int v_cnt = 0;
($rose(a), v_cnt=0) ##1 ( ($fell(b), v_cnt++)[*1:$] ##[0:$]) intersect $fell(a)[->1] |=> (v_cnt == num);
endproperty
And I found the following post.
It looks usage of go-to repetition [->n] and non-continuous repetition [=N] to a sequence is not allowed. They are only for boolean.
Therefore,
(xxxx, v_cnt++) cannot be used with [=1:$] or [->1:$] since it is a sequence.
Only continuous repetition (xxxx, v_cnt++)[*1:$] is allowed.
I expect PASS of the property in my test shown above with ALL simulators.
I’ll try with the new property p_pulse_cnt_2.