Ben,
(1) I was referring to following quote from Degeneracy_1800_2028.pdf
5) Never be matched, no match can exist
(ii) a ##1 1’b0-- logically impossible- a followed by false
case (5.ii) is attributed to a false logical value resulting from parameter substitution. In both scenarios, if utilized in a property, they would lead to an unsatisfied property
I am not clear on “attributed to a false logical value resulting from parameter substitution”
I found a thread related to using hard zero in concurrent assertion where Dave commented
“In the hard_zero assertion, the (0) does not get evaluated until run-time”
(2) In the original post the irony is that the same tool ( VCS ) that throws compilation error for edalink treats ‘sva2’ in edalink2 as legal.
It seems like a tool issue/limitation as in both cases the consequent is equivalent to
( 1'b0 ) or ( Non_Degenerate_Sequence ) i.e ( Non_Degenerate_Sequence )
As consequent :: ( 1'b0 ) or ( Non_Degenerate_Sequence ) doesn’t violate the following LRM quote
Any sequence that is used as a property shall be nondegenerate and shall not admit any empty match.
I am of the opinion that consequent is legal in edalink
Please correct me if I am wrong in my interpretation.