Hi everyone,
I’m a beginner in SVA and I’m having some trouble understanding the throughout assertion. It’s specified in the LRM that it uses the intersect assertion in the following manner:

(Expression) [*0:$] intersect SequenceExpr

I’m confused on why is it [*0:$] and not [*1:$], because wouldn’t the Expression evaluate to true everytime since its lower bound is 0?

On one of the tools I observe compilation error ::

A sequence that is used as property must be non-degenerate and admit no empty match

LRM section 16.9.9 mentions

sequence_expr ::=
...
| expression_or_dist throughout sequence_expr
The construct exp throughout seq is an abbreviation for the following:
(exp) [*0:$] intersect seq

As Cecil pointed shouldn’t the LHS sequence be [*1:$] ] ?
For the intersect operator to succeed it’s necessary that the LHS sequence matches ,
wouldn’t this require [*1] ?

I had a discussion with a colleague on our 1800 SVA committee.

sequence_expr ::=
...
| expression_or_dist throughout sequence_expr
The construct exp throughout seq is an abbreviation for the following:
(exp) [*0:$] intersect seq

The intersection need not have an empty match. It is not the components but the sequence resulting from the intersection.
Bottom line, no change to

LRM section 16.9.9 mentions
sequence_expr ::=
...
| expression_or_dist throughout sequence_expr
The construct exp throughout seq is an abbreviation for the following:
(exp) [*0:$] intersect seq

I noticed from edaplayground that some tools (not the latest ones there) complain about the empty while others do not.
This is the way it is!
Ben
match while others do not

Assuming $rose(sig1) and $rose(sig2) are true on same clock ::

For throughout operator to succeed the lhs expr must match on the clock that rhs sequence matches.
Hence I still believe that the equivalent expression using intersect should have [*1:$] for the lhs expr

I
I honestly think that this is a boderline issue, and as you experienced,
there is disagreement among vendors on how the s[*0] is handled.
1800 i s clear though:
Any sequence that is used as a property shall be nondegenerate and
shall not admit any empty match.

https://www.edaplayground.com/x/GWjF
( 1 |-> s1[*0:1] intersect 1[*1]) // s1==1
The assertion passes with 2 vndors.
s1[*0:1] intersect 1[*1]) // same as
s1[*0] intersect 1[*1]) or // fail
s1[*1] intersect 1[*1]) // pass if s1==1
Thus, one could interpret the s1[*0] as non-essential or immaterial
Yet, with

BTW, I like your posts challenging 1800.
In thhe furure, please provide the link toeda and use
waveforms (instead of $display) as it is easier to debug.
In the action block, increment the pass or fail variables of type int.
e.g, assert property(t) p1++; else f1++;

Thanks,
Ben Cohen Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.