In reply to ben@SystemVerilog.us:
Hi Ben,
As mentioned in Pg2 of your paper
ap1:assert property( a intersect (b ##1 c) ); // Illegal as it admits 'no match' i.e it's a degenerate sequence
Similarly can I state the following are illegal ?
ap2:assert property( $rose(sig) |-> sig[*4] intersect 1[*10] ); // Ideally RHS should be 1[*4:10] / 1[*1:10]
ap3:assert property( (1'b1) intersect(1'b1 ##1 1'b1) );
From a strict LRM perspective as both ‘ap2’ and ‘ap3’ would never match, shouldn’t they be considered as degenerate sequences ?
i.e ideally both ‘ap2’ and ‘ap3’ should give a compilation error
As you have stated in the paper :
Vendors’ approach to handling degeneracy depends on the specific tools and versions. Certain tools will flatly reject the compilation when faced with degeneracy, whereas others might issue a warning or choose to entirely overlook the issue.
I observe that tools have different behavior for ‘ap2’ and ‘ap3’, hence wanted to confirm with you
From a human perspective it’s clear that ‘ap2’ would never match( due to unequal length of the sequences ) but it seems that tools instead of throwing a compilation error, throw an assertion failure once LHS sequence (sig[*4]) ends ( for scenario where ‘sig’ is high throughout simulation )