Hi,
I am trying following code
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
In reply to dave_59:
Hi Dave,
A few follow-up questions
[Q1] With the parenthesis, is there a precedence involved ? i.e can I state that it is due to parenthesis that (a[*0] ##0 c) won’t have a match
the subsequence a[*0] ##0 c is degenerate and should not be allowed.
Consider the following property
property prop;
@(posedge clk) (a |-> b[*0:3]);
endproperty
As per LRM 16.12.22
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] .
*[Q2] Shouldn’t the consequent b[0:3] be considered a non-degenerate ? ( as it has three nonempty matches b[*1],b[*2] and b[*3]] )
When tested across tools I observe different output. Some throw an error while some consider the code legal. I understand that the forum isn’t meant to discuss tool specific issues, hence I checked the LRM.
LRM 16.12.22 says :
Any sequence that is used as a property shall be nondegenerate and shall not admit any empty match.
I find this statement a little confusing as a non-degenerate sequence can be an ‘or’ of empty as well as non-empty sequences used as property
i.e a non-degenerate sequence can comprise of empty as well non-empty sequences
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]
[Q3] So from a strict LRM perspective doesn’t this mean that consequent b[*0:3] is illegal ?
*[Q4] Does the above LRM quote mean that a sequence that is used as a property should be a strictly non-degenerate sequence ?
i.e a sequence which admits only non-empty match ( Eg: b[1:3] )