a[=3] ##1 b; //3 non consecutive/consecutive a and then b anytime after last a
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.
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"
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 :