Assertion interpretation for `true, x=0 ##0 (!a[*0:$] ##1 a, x=x+data)[*4] ##1 b ##1 c && (data_out==x);

Hi,

I have the following assertion example I came across in a course that I am trying to understand:

sequence rep_v;
int x; //local variable declared
`true, x=0 ##0 (!a[*0:$] ##1 a, x=x+data)[*4] ##1 b ##1 c && (data_out==x);
endsequence

Below are my questions:

  1. Does `true mean true for the current cycle? If so what is true for the current cycle?
  2. Another question is how should the subexpression !a[*0:$] be understood? Does this mean whenever a becomes zero at any time till the end of the simulation? If so, how will the ! work?
  3. Is a[*0:] acceptable because I have read that in the repetition operator with range [*m:n], n cannot be . How should a[*0:$] be understood?

Any help is appreciated.
Thanks in advance.

In reply to sk7799:

  1. **true** not defined in SystemVerilog&mdash;it is usually defined by the user as <span style="font-family:'courier'"> **1'b1**</span>. A **sequence** is a series of boolean expressions that must be *True* or *non-zero* to move the next expression in the sequence. They are using <span style="font-family:'courier'"> \true to unconditionally assign the local variable x to 0 at the beginning of the sequence. Which cycle the beginning of a sequence occurs depends on how it is used in an assertion. You probably need to study this topic more.

*!a[0:$] ##1 a means !a must be true 0 or more times before a becomes true. An open ended range is perfectly legal syntax for a repetition range, but there is usually a more expressive way to write the same thing. In this case
a[->1]
is the goto repetition operator that is a sequence that waits for a to become true (once).
3. I think 2) answers this