Assertions

SystemVerilog
6

In reply to Mechanic:

In reply to ben@SystemVerilog.us:
if the property is a sequence then:

  1. req until gnt; == req[*1:]##1gnt;? or req until gnt == req[*0:] ##1gnt?

This is the equivalent when the properties are sequences
req until gnt == req[*0:$] ##1 gnt

  1. req until_with gnt; == req[*1:]##0gnt;? or req until_with gnt; == req[*0:]##0gnt?
    I am bit confused in using [*1:] and [*0:] please let me know
(p until_with q) is equivalent to ((p until (p and q)).
Thus, 
req until_with gnt; == req[*0:$] ##1 req && gnt 
NOTE:  a[*0:2] |-> b; // This is equivalent to
a[*0] or // a_sequence[*0] is called an empty match
a[*1] or a[*2] |=> (b ##1 c);
a[*0] is the empty match, it is not repeated, it does not exist.  SVA defines the zero repetition 
Also, a[*0] ##0 1 is equivalent to 
      empty_match ##0 1, and that results to zero (or empty). 
      enpty cannot be immediately followed at the same sample by anything, even true.  It results in zero 
a[*0] ##1 b is equivalent to b