Understanding the throughout SVA

SystemVerilog
,
1

Hi everyone,
I’m a beginner in SVA and I’m having some trouble understanding the throughout assertion. It’s specified in the LRM that it uses the intersect assertion in the following manner:

(Expression) [*0:$] intersect SequenceExpr

I’m confused on why is it [*0:$] and not [*1:$], because wouldn’t the Expression evaluate to true everytime since its lower bound is 0?

Thanks,
Cecil

2

See my paper: Reflections on Users’ Experiences with SVA, part 2

Addresses the usage of these four relationship operators: throughout, until, intersect, implies

Ben Cohen ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.
https://systemverilog.us/vf/Cohen_Links_to_papers_books.pdf

3

Hi Ben,
I was trying the following SVA from your paper

ap_sig1_stable_intersect_sig2 : assert property(@(posedge clk)   
     $rose(sig2) |=> ($stable(sig1)[*0:$] ) intersect  !sig2[->1]);

On one of the tools I observe compilation error ::

A sequence that is used as property must be non-degenerate and admit no empty match

LRM section 16.9.9 mentions

sequence_expr ::= 
...
| expression_or_dist throughout sequence_expr

The construct exp throughout seq is an abbreviation for the following:
(exp) [*0:$] intersect seq

As Cecil pointed shouldn’t the LHS sequence be [*1:$] ] ?
For the intersect operator to succeed it’s necessary that the LHS sequence matches ,
wouldn’t this require [*1] ?

1 Like
4

You are absolutely correct!
My error, possibly not detected by a tool when I wrote the paper.
Thanls for pointing this out.
Ben

1 Like
5

Ben,
This would also mean that correction is required in Section 16.9.9 of the LRM , right ?

The construct exp throughout seq is an abbreviation for the following:
(exp) [*0:$] intersect seq

[*0] in the above line should be corrected to [*1]

The construct exp throughout seq is an abbreviation for the following:
(exp) [*1:$] intersect seq
1 Like
6

Yes, that is exactly what I want to know

7

I had a discussion with a colleague on our 1800 SVA committee.

sequence_expr ::= 
...
| expression_or_dist throughout sequence_expr

The construct exp throughout seq is an abbreviation for the following:
(exp) [*0:$] intersect seq

The intersection need not have an empty match. It is not the components but the sequence resulting from the intersection.
Bottom line, no change to

LRM section 16.9.9 mentions

sequence_expr ::= 
...
| expression_or_dist throughout sequence_expr

The construct exp throughout seq is an abbreviation for the following:
(exp) [*0:$] intersect seq

I noticed from edaplayground that some tools (not the latest ones there) complain about the empty while others do not.
This is the way it is!
Ben
match while others do not

1 Like
8

Thanks a lot for your response. Could you please elaborate on the following statement, I’m not able to understand it clearly.

Thanks,
Cecil

9

I tested the following on licensed tools at work ( Questa 2023.1,xcelium 23.03.07, VCS U-2023.03-SP2 )

 ap1:assert property( @(posedge clk) $rose(sig1) |-> sig1 throughout $rose(sig2)[->1] ) $display("T:%0t ap1 Passes",$time);

 ap2:assert property( @(posedge clk) $rose(sig1) |-> sig1[*0:$] intersect $rose(sig2)[->1] ) $display("T:%0t ap2 Passes",$time);

Only VCS throws a compilation error with ap2

Assuming $rose(sig1) and $rose(sig2) are true on same clock ::

For throughout operator to succeed the lhs expr must match on the clock that rhs sequence matches.
Hence I still believe that the equivalent expression using intersect should have [*1:$] for the lhs expr

10

I
I honestly think that this is a boderline issue, and as you experienced,
there is disagreement among vendors on how the s[*0] is handled.
1800 i s clear though:
Any sequence that is used as a property shall be nondegenerate and
shall not admit any empty match.

https://www.edaplayground.com/x/GWjF
( 1 |-> s1[*0:1] intersect 1[*1])   // s1==1
The assertion passes with 2 vndors. 
s1[*0:1] intersect 1[*1])   // same as 
  s1[*0] intersect 1[*1])  or // fail
  s1[*1] intersect 1[*1])  // pass if s1==1
Thus, one could interpret the s1[*0] as non-essential or immaterial 
Yet, with

SVA Dynamic Variable until/until_with usage(2) - EDA Playground
( 1 |-> s1[*0] intersect 1[*0]) // s1==1
s1[*0:1] intersect 1[*0]) // same as
s1[*0] intersect 1[*0]) or // fail

  BTW, I like your posts challenging 1800. 
  In thhe furure, please provide the link toeda and use 
  waveforms (instead of $display) as it is easier to debug. 
  In the action block, increment the pass or fail variables of type int. 
    e.g, assert property(t)  p1++; else f1++;

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

11

Thank you for the clarification