Intersect Operator in SVA clarification

SystemVerilog
, ,
1

Hi everybody,

Another clarification help needed in SystemVerilog Assertion. There are a few things I need help with. First is that I don’t understand what `true[*1:4] means in this context.
Also, I get the sequence after the intersect operator where Retry is consecutively repeated for a certain number of clock cycles, but does it mean that it is getting repeated infintely until $rose(dataRead) is true?

How is this assertion property block lies well with what the specification requires?

I have screenshot of the example in question below.

image
image751×342 58.1 KB

Thank you!

3

For the intersect operator to succeed :

lhs_seq intersect rhs_seq

The length of both sequences must be same
i.e both sequences must start at the same clock as well as end at the same clock.

The consequent is equivalent to

( 1[*1] intersect ( Retry ##[1:$] $rose(dataRead) )  ) or
( 1[*2] intersect ( Retry ##[1:$] $rose(dataRead) )  ) or
( 1[*3] intersect ( Retry ##[1:$] $rose(dataRead) )  ) or
( 1[*4] intersect ( Retry ##[1:$] $rose(dataRead) )  )

For the intersect operator to succeed one of the following sequences must match

( 1[*2] intersect ( Retry ##1 $rose(dataRead) )  ) or
( 1[*3] intersect ( Retry ##2 $rose(dataRead) )  ) or
( 1[*4] intersect ( Retry ##3 $rose(dataRead) )  )

I believe the RHS sequence should be re-written as

( Retry ##[0:$] $rose(dataRead) )

for a scenario where both $rose(Retry) and $rose(dataRead) are true at the same clock.

4

Thank you, I think that was a good explanation.

However, what does the `true[*1:4] mean and its role in this screenshot example?

5

At the top of the screenshot you see a define :

`define true 1'b1

So `true[*1:4] essentially means 1[*1:4] .
Due to 1[*1:4] the RHS sequence must match within 4 clocks ( which is essentially the requirement )
The lhs sequence helps in establishing the 1 to 4 clock window ( via 1[*1] , 1[*2] , 1[*3] , 1[*4] ) for the intersect operator