Sequence ##N ( No_match_sequence )

SystemVerilog
,
1

Hi Forum,
While referring to empty-sequence I came across the empty sequence pdf that Ben shared in his response.

Here is one example out of the many that I tried in relation to the topic of empty sequences and sequences that admit no match.


assert property( @(posedge ip_clk) req ##1( rdy[*0] ##0 ack ) ); // Is the code legal ?

Sequence ( rdy[*0] ##0 ack ) is a no match i.e 0 as it can never match. 1800 terms it degenerate sequence.
So the entire sequence expression would be equivalent to

 @(posedge ip_clk) req ##1 0 ;

So once ‘req’ is sampled high at t0 then shouldn’t the assertion fail at t1 ?
When tested on edaplayground the result varies. I even observe a compilation error “A sequence that is used as property must be non-degenerate and admit no empty match.”
As ‘req’ admits either a ‘match’ or ‘no match’, how is the entire expression considered a non-degenerate sequence with an empty match ?
Isn’t a ‘no match’ (eg: rdy[*0] ##0 ack ) different than ‘empty match’ (eg: rdy[*0] ) ?

Thanks in advance

2

In reply to mohabhat:

You are referring to y paper: Understanding SVA Degeneracy
A MUST READ PAPER FOR SVA USERS!

Section 1.2.1 Empty match rules
1 (empty ##0 seq) does not result in a match
Since (empty ##0 seq) is a NO MATCH. 1.2 rules 2a, 2b (above) make this sequence degenerate and thus illegal regardless of where it is used, a property or as an antecedent

Section 1.5 HOW TOOLS HANDLE DEGENERACY points out that 1800nisa spec, thus does not address how tools address the issue. In simulation, vendors’ approaches to handling degeneracy depend on the specific tools and versions. Some tools outright reject compilation when faced with degeneracy, while others may issue a warning or choose to entirely overlook the issue and treat a degenerate sequence as not matched. In the case of a formal verification tool, it may likely allow a degenerate sequence; however, you won’t see the property successfully proven or covered.

Your question:

So once ‘req’ is sampled high at t0 then shouldn’t the assertion fail at t1 ?
When tested on edaplayground the result varies. I even observe a compilation error “A sequence that is used as property must be non-degenerate and admit no empty match.”
As ‘req’ admits either a ‘match’ or ‘no match’, how is the entire expression considered a non-degenerate sequence with an empty match ?
Isn’t a ‘no match’ (eg: rdy[*0] ##0 ack ) different than ‘empty match’ (eg: rdy[*0] ) ?

*rdy[0] ##0 ack is different than empty. rdy[*0] is empty and cannot be sampled.
1800 considers *rdy[0] ##0 ack as degenerate and illegal.

Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.

3

In reply to ben@SystemVerilog.us:

Note:


assert property( @(posedge ip_clk) req ##1 rdy[*0] ##0 ack); // Is legal because
req ##1 rdy[*0] ##0 ack // is reduced to 
req ##0 1 ##0 ack // using left associativity 
    
assert property( @(posedge ip_clk) req ##1( rdy[*0] ##0 ack ) ); // Is  illegal because 
( rdy[*0] ##0 ack ) is bracketed, thus, 
( rdy[*0] ##0 ack ) is degenerate.

Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.

4

In reply to ben@SystemVerilog.us:

Thank your Sir for your response.

Would like to hear your comments on the following

  1. Although ‘req’ is a non-degenerate (admits either a match/not match) one clock later we have a sequence that admits no match.
    Essentially the entire expression is equivalent to
non_degenerate_sequence_exp ##1 no_match_sequence_exp

Now this entire expression itself is a degenerate as it can never match. Hence it’s illegal
Is my understanding correct ?
2. Are the following two SVAs equivalent ?


sva_1:assert property( @(posedge clk) req ##1 (rdy[*0] ##0 ack) ); // (rdy[*0] ##0 ack) is no match i.e hard 0
sva_2:assert property( @(posedge clk) req ##1 (0) );
  1. How is that following concurrent assertions are considered legal ?

sva1:assert property( @(posedge clk) req ##1 (0) );
sva2:assert property( @(posedge clk) req ##1 0 );
sva3:assert property( @(posedge clk) 0 );

As these sequences can never match, shouldn’t these be considered degenerate sequences as well ? ( thereby making them illegal )

5

In reply to mohabhat:

Referring to my paper: Paper: Understanding SVA Degeneracy
A MUST READ PAPER FOR SVA USERS!

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.
The following restrictions apply:
Any sequence that is used as a property shall be nondegenerate and shall not admit any empty match.[/quote]
Also, in the paper:

How tools handle degeneracy
As discussed in Section 1.2, 1800 establishes rules, specifying, for instance, that any sequence utilized as a property must be nondegenerate and must not allow any empty match. However, 1800 lacks clarification on how tools should manage these conditions or offer guidance on potential actions; 1800 is a specification, it does not address tools. When encountering degeneracy, should a tool outright reject the compilation? Should it provide a compilation warning and disregard the assertion? Alternatively, should it simply overlook the issue and treat the degenerate sequence as not a match?
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. For example, in scenarios like:
special_ack |-> SPECIAL_RESOURCE_IN_CONFIG, where the parameter in caps may vary by config, users might not want compilation errors in the cases where the current configuration makes that particular property useless. Another example is with the use of the generate, such as:
generate
genvar i, j;
for (i = 0; i < 2; i++) begin
for (j = 0; j < 2; j++) begin
ap_abc: assert property (@ (posedge clk)
$rose(a) |-> b[*j] ##i c);
end
end
endgenerate
// equivalent t0:
ap_abc00: assert property (@ (posedge clk) $rose(a) |-> b[*0] ##0 c); // degenerate
ap_abc01: assert property (@ (posedge clk) $rose(a) |-> b[*1] ##0 c); // legal
ap_abc10: assert property (@ (posedge clk) $rose(a) |-> b[*0] ##1 c); // same as ##0 c
ap_abc11: assert property (@ (posedge clk) $rose(a) |-> b[*1] ##1 c); // legal
So how do simulation and formal verification tools handle degeneracy?
I observed that, in simulation, vendors’ approaches to handling degeneracy depend on the specific tools and versions. Some tools outright reject compilation when faced with degeneracy, while others may issue a warning or choose to entirely overlook the issue and treat a degenerate sequence as not matched. In the case of a formal verification tool, it may likely allow a degenerate sequence; however, you won’t see the property successfully proven or covered.

Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.