Hi All,
I was referring to Ben’s thread for modeling dynamic repeat range
For dynamic repeat range the code has limitation for a case when both dynamic variables are 0
Eg: *seq1 |-> seq2[dyn_var1:dyn_var2] ##1 seq3 // where dyn_var1 and dyn_var2 are 0
So I decided to try an example which overcomes the limitation : edalink
For the different stimulus I tried, the code does work as per intention. Just wanted to confirm with the forum moderators if there are any limitations ?
In reply to MICRO_91:
That’s the only way I could solve this.
SVA: Dynamic repeats with count that may include 0.
// write a procedural assertion with the if-else
// example:
int n=0; bit a, b, clk;
// assert property( w |-> a[*n] ##1 b);
always @(posedge clk)
if(count==0)
ap_wb0: assert property( w |-> b);
else if(count>0)
ap_wb: assert property( w |-> sq_rpt_simple_count(a,n) ##1 b);
// Note that instead of the always procedure, you can just write
ap_wb0: assert property(@(posedge clk) (count ==0) ##0 w |-> b);
ap_wb: assert property(@(posedge clk)
(count > 0) ##0 w |-> dynamic_repeat(a,n) ##1 b);
In reply to ben@SystemVerilog.us:
Ben ,
Would like to hear your views on sequence ‘dynamic_repeat_range’ in the above edalink.
One limitation I am aware of is of Case 5 i.e *seq1 |-> seq2[0:0] ##0 seq3; // ‘N’ is 0
The consequent shouldn’t match (ideally code shouldn’t compile) however using sequence ‘dynamic_repeat_range’ the assertions passes at T:5.
On changing LHS sequence of ‘or’ operator to : ((v == 0) ##(N-1) seq3)
This throws a Compilation error (due to ##(0-1) ) as per expectation!!
The code does work as per intention for *seq1 |-> seq2[0:0] ##1 seq3;