In reply to Have_A_Doubt:
Shouldn’t ( !b[*1] ##1 b[*0] ) be equivalent to ( !b[*1] ##0 true )
[Ben] The below analysis seem to indicate that
b[>0] is equivalent to empty or !b[*1] ##0 true or !b[*2] ##0 true or …
However, 1800 pg 446 states:
1800 16.12.22 Nondegeneracy 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 zero consecutive repetition means that there is no sample taken at any clock tick. Therefore, such a sequence can only match on an empty trace (as formally defined in F.4.3 ). *A sequence may admit both empty and nonempty matches, for example, a[0:2]. This sequence admits an empty match and up to two nonempty matches: a and a[*2]. A sequence that admits no match or that admits only empty matches is called degenerate. A sequence that admits at least one nonempty match is called nondegenerate. A more precise definition of nondegeneracy is given in F.5.2 and F.5.5 . The following restrictions apply:
a) Any sequence that is used as a property shall be nondegenerate and shall not admit any empty match.
b) Any sequence that is used as the antecedent of an overlapping implication (|->) shall be nondegenerate.
c) Any sequence that is used as the antecedent of a nonoverlapping implication (|=>) shall admit at least one match. Such a sequence can admit only empty matches. The reason for these restrictions is because the use of degenerate sequences in forbidden ways results in counterintuitive property semantics, especially when the property is combined with a disable iff clause.
This 1800 limitation causes b[->0] to be inadmissible, regardless on how you expand it.
a) Any sequence that is used as a property shall be nondegenerate and shall not admit any empty match.
a |-> (b [-> 0])
A sequence that is used as property must be non-degenerate and admit no
empty match.
1800’2017 16.9.2.1 Repetition, concatenation, and empty matches Using 0 as a sequence repetition number, an empty sequence (see 16.7 ) results, as in this example: a [*0]
Because empty matches occur over an interval of zero clock ticks and are thus of length 0, they follow the set of concatenation rules specified below. In the following rules, an empty sequence is denoted as empty, and another sequence (which may be empty or nonempty) is denoted as seq.
— (empty ##0 seq) does not result in a match.
— (seq ##0 empty) does not result in a match.
— (empty ##n seq), where n is greater than 0, is equivalent to (##(n-1) seq).
— (seq ##n empty), where n is greater than 0, is equivalent to (seq ##(n-1) true). Using simple decomposition, once would think that the following is true: b[->0] is equivalent to !b[*0:$] ##1 b[*0] // expanding to **!b[*0] ##1 b[*0] or** // (empty ##n seq) same as (seq ##(n-1) true)
b[*0] ##0 `true // (empty ##0 seq) does not result in a match.
// !b[*0] ##1 b[*0] is a no match
**!b[1] ##1 b[0] or // (seq ##n empty) same as (seq ##(n-1) true). !b[*1] ##0 true
**!b[2] ##1 b[0] or
!b[*2] ##0 `true
…
Shouldn’t ( !b[*1] ##1 b[*0] ) be equivalent to ( !b[*1] ##0 true )
My mistake, it looks like it should be equivalent to
empty or !b[*1] ##0 true or !b[*2] ##0 true or …
But 1800 prevents the use of b[->0] as mentioned above
Thanks for asking,
Ben