In reply to MICRO_91:
On item 1, I wrote the model with my understanding of the requirements. If there is are different requirements, then the model needs to change.
In any case, the nice thing about writing SVA is that it puts on the dots on the requirements.
on
(3) Out of curiosity , what is considered the left sequence_expr for intersect operator ?
rose(sig1) |-> sig2[->1] ##1 !sig2[*1:] intersect sig1[*1:$];
This is resolved in 1800 by the definition of
1800: 16.9.1 Operator precedence Operator precedence and associativity are listed in Table 16-1 . The highest precedence is listed first. Table 16-1—Operator precedence and associativity
Here ## has higher precedence than intersect. Thus,
sig2[->1] ##1 !sig2[*1:] is computed first. In other words,
sig2[->1] ##1 !sig2[*1:] intersect sig1[*1:]
is same as
(sig2[->1] ##1 !sig2[*1:]) intersect sig1[*1:$]