In reply to bdreku:
// I have a comment on your use of
expr[*] ##0 seq // in
($rose(B),count=0) ##0 (count<delay(CFG3),count+=1)[*] ##0 (count==delay(CFG3)) && B;
// Specifically, [*] is equivalent to [*0:$]. Consider the following
a ##0 1[*] ##0 b // same as
a ##0 1[*0:$] ##0 b // same as
a ##0 1[*0] ##0 b or
a ##0 1[*1] ##0 b or
...
a ##0 1[*n] ##0 b // n==infinity
// BUT !!!!!!!
0 1[*0] ##0 b // is an empty match, by definition
// THUS,
($rose(B),count=0) ##0 (count<delay(CFG3),count+=1)[*] ##0 (count==delay(CFG3)) && B;
// IS SAME AS
($rose(B),count=0) ##0 (count<delay(CFG3),count+=1)[*1:$] ##0 (count==delay(CFG3)) && B;
My point:*Avoid structures that include (or infer) seq1[0] ##0 seq2
(where seq is a sequence of one or more terms
It’s a style issue because SVA reflects requirements.
Why do we want to add meaningless requirements?