Understanding the throughout SVA

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