Meaning of "sequence used as a property"

SystemVerilog
,
1

Section 16.12.22 of the LRM says

Any sequence that is used as a property shall be nondegenerate and shall not admit any empty match

I am intrigued by the starting of the sentence “Any sequence that is used as a property” i.e what does it mean ?

Consider the following scenarios:


// Case 1: sequence used as consequent
   sequence s1;
     <some_seq_expression1>
   endsequence
   ap_case1:assert property( a |=> s1 );

// Case 2: sequence directly asserted
   sequence s2;
     <some_seq_expression2>
   endsequence
   ap_case2:assert property( s2 ); // Same as ap_case2:assert property( <some_seq_expression2> );

// Case 3: sequence_expr used as consequent
   ap_case3:assert property( <some_seq_expr3> |=> <some_seq_expr4> );

[Q1] Since a property_expr can’t be part of sequence body, would s1 be interpreted as sequence_expr ( rather than a property_expr ) ?
I am aware that a sequence_expr is by default a property_expr and consequent is a property_expr

[Q2] Are all 3 cases ap_case1,ap_case2 and ap_cse3 examples of “sequence used as a property” ?

2

In reply to Have_A_Doubt:

Section 16.12.22 of the LRM says

Any sequence that is used as a property shall be nondegenerate and shall not admit any empty match

[Q1] Since a property_expr can’t be part of sequence body, would s1 be interpreted as sequence_expr ( rather than a property_expr ) ?
I am aware that a sequence_expr is by default a property_expr and consequent is a property_expr

s1 is interpreted as sequence_expr, which is one of the many options as to what represents a property. Thus,


 ap_case1:assert property( a |=> s1 ##1 a); // s1 is definitely a sequence here, not a property
 ap_case1:assert property( a |=> s1[*2] );  // s1 is definitely a sequence here

[Q2] Are all 3 cases ap_case1,ap_case2 and ap_cse3 examples of “sequence used as a property” ?

Yes