Regarding assertion consecutive and goto ops

Team,

  1. a[=3] ##1 b; //3 non consecutive/consecutive a and then b anytime after last a
  2. a[->3] ##1 b; //3 non consecutive/consecutive a and then b immediately after one clock cycle of a

If above understanding is correct , then can we use ##5 instead of ##1 in the first case? my confusion is , if we use ##1 then b should happen just after a clock cycle and not anytime after a, basically what is the use of ##1 in the first case where b don’t care about it.

Thank you.

In reply to megamind:


b[=m] // is equivalent to 
( b [->m] ##1 !b [*0:$] ) // Thus, 
b[=1] //is equivalent to:
!b[*0:$] ##1 b ##1 !b[*0:$]
b[=2] // is equivalent to:
!b[*0:$] ##1 b ##1 !b[*0:$] ##1 b ##1 !b[*0:$]
//--------------
a[=3] ##1 b; //3 non consecutive/consecutive a and then b anytime after last a
// [Ben] Not quite true 
a[=3] ##1 b; //3 non consecutive/consecutive a and then !a until b 
// Between the last "a" and "b"  a==0 
//
// [quote]If above understanding is correct , then can we use ##5 instead of ##1 in the first case? 
// [Ben] Using a repeat of 2 for simplicity 
a[=2] ##5 b; // is same as 
!a[*0:$] ##1 a ##1 !a[*0:$] ##1 a ##1 !a[*0:$] (##5 b) 
// Between the last a and the b there could be 5 cycles where a==1
// Consider this sequence 
a  0 0 1 0 1 0  1 1 1 1 1   // 2 non-consecutive "a"s followed by the sequence (##5 b) 
b  0 0 0 0 0 0 (0 0 0 0 1)  // While (##5 b) "a" can have any value.     
b  0 0 0 0 0 0 (X X X X 1)  // While (##5 b) "b" can be x . 
b  0 0 0 0 0 (X X X X 1)  // While (##5 b) "b" can be x . 

// [quote] if we use ##1 then b should happen just after a clock cycle 
//  and not anytime after a, 
// basically what is the use of ##1 in the first case where b don't care about it
// [Ben] Not true on the statement  "b should happen just after a clock cycle" 
// TRUE for "b can happen just after a clock cycle, but if it happen later, then a==0 until b==1"

In reply to ben@SystemVerilog.us:

Thank you Ben.
Should not

[*0:$] be replaced with [*1:$] everywhere?

Question: Should not [*0:] be replaced with [*1:] everywhere?
Answer: NO.


a[*0:$] ##1 b  // is equivalent to
a[*0] ##1 b or  // <<< same as "b"   (no ##1) 
a[*1] ##1 b or 
...
// THUS, 
a[=2] ##1 b; // is same as 
(!a[*0:$] ##1 a ##1 !a[*0:$]) (##1 a ##1 !a[*0:$]) ##1 b 
// Sequences that satisfy this 
let sq1= (!a[*0:$] ##1 a ##1 !a[*0:$])
a  0 0 1 0 1 0      // 2  non-consecutive "a"s followed by the sequence (##1 b) 
b  0 0 0 0 0 1      // sq1 (##1 a ##1 !a[*0]) ##1 b  
//             reduces sq1 (##1 a ##1             b   
//
a  0 0 1 0 1 0 0     // 2  non-consecutive "a"s followed by the sequence (##1 b) 
b  0 0 0 0 0 0 1      // sq1 (##1 a ##1 !a[*1]) ##1 b 
//
//
a  0 0 1 0 1 0 0 0   // 2  non-consecutive "a"s followed by the sequence (##1 b) 
b  0 0 0 0 0 0 0 1      // sq1 (##1 a ##1 !a[*2]) ##1 b     

More on this empty match:
*[0 : m] Repetition range with zero
 Rule: The [*0:m] repetition declares that the element in the SEQUENCE must repeat 0 times (i.e., can be skipped altogether), or 1 times, or 2 times, or … m times. The example, b[*0:3] means that b may either be skipped (i.e., no cycle spent on b), or b may be repeated once, twice, or three times. In the sequence (b[*0:3] ##1 c), if c holds at the start of this sequence, then a check on b is skipped altogether, as if it were not there. However, if c does not hold at the start of the sequence, then b needs to hold a maximum of three cycles. As a result, this construct creates a set of different threads that can occur. The following describes the expected behavior for this assertion.

a |-> (b[*0:3] ##1 c); // one thread at each attempt
// equivalent to
a |-> ( c ) or // (b[*0] ##1 c ) is equivalent to c
(b[*1] ##1 c ) or
(b[*2] ##1 c ) or
(b[*3] ##1 c );
endproperty :