Is sequence: b[*0:3] valid as consequent?

SystemVerilog
,
1

Consider the following property


 always #5 clk = !clk;
  
  property prop;
    @(posedge clk) a |-> b[*0:3] ; // Is consequent legal ?
  endproperty 
  
  assert property(prop) $display("T:%0t Pass",$time); else $display("T:%0t Fails",$time);
 
  initial begin
    #4 ; a = 1;
         b = 1;
    #2; $finish();    
  end

I observe different results across tools.

Two tools throw a compilation error :
Error-[SVA-SEQPROPEMPTYMATCH] Invalid sequence as property. A sequence that is used as property must be non-degenerate and admit no empty match.
while a 3rd tool shows pass report at T:5 ( due to b[*1] match at T:5 )

LRM 16.12.22 Nondegeneracy ::

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 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]

Hence sequence b[*0:3] would be non-degenerate sequence as it is comprised of empty sequence b[*0] and three nonempty sequences ( b[*1],b[*2] and b[*3]] )

LRM 16.12.22 further states ::
The following restrictions apply:
a) Any sequence that is used as a property shall be nondegenerate and shall not admit any empty match

NOTE: The above quote is an ‘and’ of two conditions

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

Due to the ‘and’ in the above LRM quote,
does the above line mean that a sequence that is used as a property consist of non-empty sequence(s) only ?
i.e There shouldn’t be an empty sequence in the equivalent expression of the sequence that is used as a property

It seems that tools have their own interpretation of the above LRM quote.
As consequent b[*0:3] consists of an empty sequence b[*0] it is treated as invalid by some tools.

While some tools seem to ignore the empty sequence ( as it can’t match ) and trigger the pass action block as soon as one of the non-empty sequences match ( b[*1] )

2

In reply to Have_A_Doubt:

It seems that tools have their own interpretation of the above LRM quote.
As consequent b[*0:3] consists of an empty sequence b[*0] it is treated as invalid by some tools.
While some tools seem to ignore the empty sequence ( as it can’t match ) and trigger the pass action block as soon as one of the non-empty sequences match ( b[*1] )

You are correct about the ambiguity, but as you well quoted 1800, b[*0:3] as a consequent is degenerate. Usually, *b[0:3] is used with a followup sequence, like *b[0:3] ##1 c. b[*0] has no real meaning; I read it as something that is not repeated. What is its significance, it’s not there. What I am saying is that b[*0] as an option by itself is meaningless and should not be used in an asertion. Of course, *b[0] ##1 c is ok since it is equivalent to c.
Ben

3

In reply to ben@SystemVerilog.us:

Hi Ben,
Wanted to confirm a few things

as you well quoted 1800, b[*0:3] as a consequent is degenerate.

[Q1] Wouldn’t b[*0:3] be a non-degenerate sequence ?( Non-degenerate as it consist of 3 non-empty sequences ( b[*1],b[*2] and b[*3]] ) )

This is based on LRM’s definition: “A sequence that admits at least one nonempty match is called nondegenerate.”

(2) LRM’s perspective on consequent: b[*0:3]

LRM 16.12.22 :

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

The above LRM quote is an ‘and’ of 2 conditions i.e both conditions should be met
Condition1: Any sequence that is used as a property shall be nondegenerate
Condition2: Any sequence that is used as a property shall not admit any empty match

Although sequence b[*0:3] satisfies condition1, *it doesn’t meet condition2 as it has an empty sequence b[0]

*[Q2] So from a strict LRM perspective doesn’t this mean that consequent b[0:3] is illegal ?

(3) Usage of empty sequence [*0] :

Consider the following concurrent assertion


  always #5 clk = !clk;
  property p1;
    @(posedge clk) b ##1 (a[*0] ##0 c);
  endproperty  
 
  assert property(p1) $display("T:%0t Pass",$time); else $display("T:%0t Fails",$time);
 
  initial begin
    #4; b = 1; c = 1;
    #12; $finish();
  end

My understanding is that the equivalent expression for : b ##1 (a[*0] ##0 c) would be (b ##1 c) so I expected a pass at T:15.
However 2 tools throw a compilation error whereas the 3rd tool shows failure at T:15.

*[Q3] With the parenthesis is there a precedence involved ? i.e can I state that due to parenthesis, (a[0] ##0 c) won’t have a match

4

In reply to Have_A_Doubt:

on (3) I think (a[*0] ##0 c) is considered a fusion, I remember a book mentioned this is not allowed.