Paper: Understanding SVA Degeneracy

SystemVerilog
,
1

A MUST READ PAPER FOR SVA USERS!

  • Explains “degenerate sequences” and restrictions.
  • Explains “empty match” when integrating into other sequences.
  • Intriguing case study illustrates potential issues caused by ‘empty’ and ‘within’.

I express my gratitude to Ed Cerny for his advice in reviewing and formulating this paper.

Ben Cohen

2

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 )

3

In reply to Have_A_Doubt:
e on what you say.
Per my last version with added sequence rule

There are legitimate cases where specifying a property using a macro or a generate parameter can render a property degenerate (and thus useless) for some configurations while remaining meaningful for others. In practical applications, the generation of degenerate and illegal sequences can be subtle for the user, influenced by factors like configuration options or generate loop statements.

It would be inconvenient to force tool customers to change the code.
I am not a tool vendor, but my guess is that each vendor took the approach that they felt was best for their customers.
Ben

4

In reply to ben@SystemVerilog.us:

IMHO that’s an incorrect argument - tools do flatten the generate/expand macros, etc. and hence statically can spot degenerate sequences. Do you have specific examples of such?

Thanks

5

In reply to Have_A_Doubt:

Interesting examples - are they not more of “tautology” (Of always-fail-to-match) than a NO-MATCH?

6

In reply to Srini @ CVCblr.com:

are they not more of “tautology” (Of always-fail-to-match) than a NO-MATCH?

They are synonymous, what we would call as “always-fail-to-match” is termed as “No-match” by the LRM