Usage of Throughout and Intersect in SVA

SystemVerilog
, , ,
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