As in a below screenshot, the signal B is driven by DUT based on the config values where we have dynamic delays as well as repetitions (total iterations). The random delays are taken care in the assertion below, but need help to code dynamic repetition.
I want to replace “CFG2_s ##0 CFG3_s ##0 CFG2_s ##0 CFG3_s” in property with something like, “(CFG2_s ##0 CFG3_s)[*CFG4]”.
PS: Theoretically this requirement doesn’t make any sense, so planning to modify the sequences to adopt the ##1 repetition delay, but being a lazy coder, just want to check if it’s possible in any case.
This is the long way for a small fix and I doubt the reusability.
However, the assertion works fine after reusing the dynamic repetition sequence from your package example and modifying a sequence and a property as below.
// Reused Your sequence for dynamic repetition
sequence q1_rpt_simple_range_q2(sequence q1, int range, sequence q2);
int v, diff;
(1, diff=range) ##0
first_match((diff>0 ##0 q1, diff=diff-1'b1) [*1:$] ##1 q2 );
endsequence
// Modified the sequence and property
// CFG3: positive level of B
sequence CFG3_s;
int count;
// Older code
//($rose(B),count=0) ##0 (count<delay(CFG3),count+=1)[*] ##1 (count==delay(CFG3)) && $fell(B);
// Modified as
($rose(B),count=0) ##0 (count<delay(CFG3),count+=1)[*] ##0 (count==delay(CFG3)) && B;
endsequence // CFG3_s
// Property to check A -> B -> C transition
property P1;
// Older code
//@(posedge CLK) CFG1_s |-> ##1 CFG2_s ##0 CFG3_s ##0 CFG2_s ##0 CFG3_s ##0 CFG2_s(1);
// Modified as
@(posedge CLK) CFG1_s |-> ##1 q1_rpt_simple_range_q2((CFG2_s ##0 CFG3_s),(CFG5-1),CFG2_s(1));
endproperty // P1
// I have a comment on your use of
expr[*] ##0 seq // in
($rose(B),count=0) ##0 (count<delay(CFG3),count+=1)[*] ##0 (count==delay(CFG3)) && B;
// Specifically, [*] is equivalent to [*0:$]. Consider the following
a ##0 1[*] ##0 b // same as
a ##0 1[*0:$] ##0 b // same as
a ##0 1[*0] ##0 b or
a ##0 1[*1] ##0 b or
...
a ##0 1[*n] ##0 b // n==infinity
// BUT !!!!!!!
0 1[*0] ##0 b // is an empty match, by definition
// THUS,
($rose(B),count=0) ##0 (count<delay(CFG3),count+=1)[*] ##0 (count==delay(CFG3)) && B;
// IS SAME AS
($rose(B),count=0) ##0 (count<delay(CFG3),count+=1)[*1:$] ##0 (count==delay(CFG3)) && B;
My point:*Avoid structures that include (or infer) seq1[0] ##0 seq2 (where seq is a sequence of one or more terms
It’s a style issue because SVA reflects requirements.
Why do we want to add meaningless requirements?