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.