I have a question on GOTO sequence operator. I am reproducing an example given on Page no. 41 of the “System Verilog Assertions Handboook 4th edition by Ben Cohen” as follows:
a|-> a[-> 1] //is equivalent to
a|-> !a[*0:$] ## 1 a;//same as
a|-> (!a[*0] ##1 a) or (!a[*1] ## 1 a) or (!a[*2] ## 1 a) … (!a[*n] ## 1 a);
however, !a[*0] ##1 a is equivalent to “a”. Thus ,
a |-> a; //final equivalence, which is not the intended property.
**I am not clear how the statement
a|-> (!a[*0] ##1 a) or (!a[*1] ## 1 a) or (!a[*2] ## 1 a) … (!a[*n] ## 1 a);
**
is equivalent to a|->a
What happens to all the or terms after the first term?
Can anyone help me to understand this.
Also statement a|->a will be same as
a |-> 1 since if a is true then in the same clock a also occurs!
In reply to puranik.sunil@tcs.com:
a|-> a[-> 1] says that if at sampling time t a==1 then anytime between now (time t because of the overlapping implication operator) or at any time in future sampling events a==1.
Thus, if a==1 at time t the consequent evaluates the value of “a” at the current sampling time, and WOW a IS equal to 1.
// ON "I am not clear how the statement"
a|-> (!a[*0] ##1 a) or (!a[*1] ## 1 a) or (!a[*2] ## 1 a) ... (!a[*n] ## 1 a);
// <----------->
a |-> a // because of rules of the repeat operator
// if a==1 then a |-> a if true, the assertion completes as success
// The same can be said about
ap_a1: assert property(@ (posedge clk) a |-> 1 ); // because
//it will simulate the same as
ap2: assert property(@ (posedge clk) a|-> !a[*0:$] ## 1 a);
//
// Note: To express the notion that "if a, then another a at some time in the future
a |=> strong(a[->1]); // OK
a |-> strong(##[1:$] a);