Usage of Throughout and Intersect in SVA

SystemVerilog
, , ,
1

Hello All,

I am trying to understand an example from the internet on the usage of ‘throughout’ and ‘intersect’. Below is the property described with ‘throughout’:

The property below requires that when a rises, b should be high in the next cycle and c in the third cycle after that AND that a should remain high until and including the cycle in which c must be high. As shown below:

 assert property ( $rose(a) |=> (a throughout (b ##3 c)));

It further says this can be written with ‘intersect’ operator as :

 assert property ( $rose(a) |=> (a[*0:$] intersect (b ##3 c)));

My Question is it necessary that a is described as a[*0:$] rather than below, will that be correct?

 assert property ( $rose(a) |=> (a intersect (b ##3 c)));

Thanks
Irshad

2

In reply to Mohammed Irshad Ahmed:

When we use S1 intersect S2 , it means both the sequences S1 & S2 should start and end at the same time.

assert property ( $rose(a) |=> (a intersect (b ##3 c)));

Now in your example , a intersect (b ##3 c) both sequences a & (b ##3 c) have same start point, but the sequence a takes only one clock cycle where as the sequence (b ##3 c) takes 4 clock cycles. As their end points are different, the property fails.

As the sequence a has to be repeated through out the b##3C, we have to use *a[0:$] intersect (b ##3 c)

3

Hi, in this example a[*0:$] wil have length of 0 to infinity the S2 will have length of 4 cycles so why it will pass.

4

@LearnChipDesign, there are 2 things to note ::

(1) Using LHS of the intersect operator as a[*0:$] is Illegal ( only 1 tool catches this ) ( Also refer :: understanding-the-throughout-sva/46326/3 )

Error-[SVA-SEQPROPEMPTYMATCH] Invalid sequence as property
testbench.sv, 9
"((a[*0:$]) intersect (b ##3 c))"
  A sequence that is used as property must be non-degenerate and admit no empty match.

    One should write the consequent as 

$rose(a) |=> (a[*1:$] intersect (b ##3 c))

(2) Consequent have an implicit first_match ( unlike antecedent )

The consequent a[*1:$] intersect (b ##3 c)) could be written as ::

first_match( 
( a[*1] intersect (b ##3 c ) ) or ( a[*2] intersect (b ##3 c ) ) or 
( a[*3] intersect (b ##3 c ) ) or ( a[*4] intersect (b ##3 c ) ) or 
( a[*5] intersect (b ##3 c ) ) or ( a[*6] intersect (b ##3 c ) ) or 
 ........  )

The first 3 sub-sequences would Never Match i.e 1’b0
Only sub-sequence ( a[*4] intersect (b ##3 c ) ) has a possibility of a match

1 Like
5

Yes, even I am getting the above error with one of the tool :grinning: Thanks for the clarification - learning SVA is altogther learning a new language… .I feel it should have a separate LRM also lots of new things are getting added like sync_reject_on - s_eventually While working on active project and keeping eye on new things is quite a task …

6

My paper on this topic
16. (intersect) vs (throughout, until, until_with, within) https://SystemVerilog.us/vf/intersect_vs_others_v11_27_24.pdf

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