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
- Any sequence that is used as a property shall be nondegenerate
- 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] )