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)