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

Question

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:

Does `true mean true for the current cycle? If so what is true for the current cycle?
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?
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.

Answer 1

dave_59

Forum Moderator

9879 posts

In reply to sk7799:

`true not defined in SystemVerilog—it is usually defined by the user as 1'b1. 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 `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).
I think 2) answers this

— Dave Rich, Verification Architect, Siemens EDA