Local variable in SVA

ben2 · February 2, 2023, 8:03am

My solution works:
Code: Edit code - EDA Playground
I copied the needed sequences instead of compiling the package for this demo
Waverforms: busy4_3.png - Google Drive

module m;
// from
// import sva_delay_repeat_range_pkg::*;
bit busy, er, ok, clk;
bit[1:0] max=2'b11;
initial forever #10 clk = !clk;
sequence dynamic_delay(count);
int v;
(count<=0) or ((1, v=count) ##0 (v>0, v=v-1) [*0:$] ##1 v<=0);
endsequence // dynamic_delay
sequence dynamic_delay_lohi_sq(d1, d2, sq);
int v1, vdiff;
( (1, v1=d1, vdiff=d2-d1) ##0 dynamic_delay(v1)   ##0
(vdiff>=0, vdiff=vdiff - 1)[*1:$] ##0 sq);
endsequence
assert property (@(posedge clk) $rose(busy) |->
dynamic_delay_lohi_sq(1, max, $fell (busy)))  ok=1; else er=1;   //##[1:max] $fell (busy))
initial begin
$dumpfile("dump.vcd"); $dumpvars;
@(posedge clk) busy<= 1'b1;
repeat(3) @(posedge clk);
busy<=1'b0;
repeat(3) @(posedge clk);
$finish;
end
endmodule

Your code has errors. This is what you meant

property p_2busy;
int count = 0;
@(posedge clk) $rose(busy) |->
first_match((busy, count = count+1, $display("c=%d", count))[*1:$] ##1 $fell(busy)) ##0 (count <= max);
endproperty
// **** The first_match is not need here, SEE MY LASR RESPONSE
ap_2busy:  assert property(p_2busy) ok2=1; else er2=1;

FUll code + waveforms:

module m; 
    // from 
    // import sva_delay_repeat_range_pkg::*;
     bit busy, er, ok, ok2, er2, clk; 
     bit[1:0] max=2'b11; 
     initial forever #10 clk = !clk;
   
     sequence dynamic_delay(count);
       int v;
     (count<=0) or ((1, v=count) ##0 (v>0, v=v-1) [*0:$] ##1 v<=0);
     endsequence // dynamic_delay
   
     sequence dynamic_delay_lohi_sq(d1, d2, sq);
       int v1, vdiff;
         ( (1, v1=d1, vdiff=d2-d1) ##0 dynamic_delay(v1)   ##0     
             (vdiff>=0, vdiff=vdiff - 1)[*1:$] ##0 sq); 
     endsequence
   
    ap_tobusy:  assert property (@(posedge clk) $rose(busy) |-> 
           dynamic_delay_lohi_sq(1, max, $fell (busy)))  ok=1; else er=1;   //##[1:max] $fell (busy))

    property p_2busy; 
        int count = 0;
        @(posedge clk) $rose(busy) |-> 
      first_match((busy, count = count+1, $display("c=%d", count))[*1:$] ##1 $fell(busy)) ##0 (count <= max); 
    endproperty
// the first_match() is needed here to test the count. 
    ap_2busy:  assert property(p_2busy) ok2=1; else er2=1;
   
     initial begin
       $dumpfile("dump.vcd"); $dumpvars;
       @(posedge clk) busy<= 1'b1; 
       repeat(4) @(posedge clk);
       busy<=1'b0; 
       repeat(3) @(posedge clk); 
       //
       repeat(1) @(posedge clk);
       busy<=1'b1; 
       repeat(3) @(posedge clk);
       busy<=1'b0; 
       repeat(3) @(posedge clk); 

       $finish;
      end
   endmodule

// sim 

# c=          1
# c=          2
# c=          3
# c=          4
# c=          1
# c=          2
# c=          3

Code

Ben