Question

It is possible to define sequences that can never be matched. For example:

(1’b1) intersect(1’b1 ##1 1’b1)

It is also possible to define sequences that admit only empty matches. For example:

1’b1[*0]

A sequence that admits no match or that admits only empty matches is called degenerate. A sequence that admits at least one non-empty match is called non-degenerate. A more precise definition of non-degeneracy is given in Annex H.

The following restrictions apply:

1. Any sequence that is used as a property must be non-degenerate and must not admit any empty match.
2. Any sequence that is used as the antecedent of an overlapping implication (|->) must be non-degenerate.
3. Any sequence that is used as the antecedent of a non-overlapping implication (|=>) must admit at least one match. Such a sequence can admit only empty matches.

The reason for these restrictions is that the use of degenerate sequences the forbidden ways results in counterintuitive property semantics, especially when the property is combined with a disable iff clause.