VF Horizons:PAPER: SVA Alternative for Complex Assertions

SystemVerilog
,
5

In reply to Tudor Timi:
Below is an update that works.
http://SystemVerilog.us/vf/sva_delay_repeat_pkg.sv
http://SystemVerilog.us/vf/sva_delay_repeat.sv


/*     */
   // SEE UPDATE BELOW 
package sva_delay_repeat_pkg; 
    sequence dynamic_repeat(q_s, count); 
        int v=count; 
        (1, v=count) ##0 first_match((q_s, v=v-1'b1) [*1:$] ##0 v<=0);
        // (v>0, v=count) ##0 ((q_s, v=v-1'b1) [*1:$] ##0 v==0); // Incorrect 
    endsequence
    
    sequence dynamic_delay(count); 
        int v; 
        (1, v=count) ##0 first_match((1, v=v-1'b1) [*0:$] ##1 v<=0); 
    endsequence
endpackage 


/*  The repeat value MUST BE > 0   
   
package sva_delay_repeat_pkg; 
    sequence dynamic_repeat(q_s, count); 
        int v=count; 
        (v>0, v=count) ##0 ((q_s, v=v-1'b1) [*1:$] ##0 v==0); 
    endsequence
    
    sequence dynamic_delay(count); 
        int v; 
        (1, v=count) ##0 first_match((1, v=v-1'b1) [*0:$] ##1 v<=0); 
    endsequence
endpackage */

import uvm_pkg::*; `include "uvm_macros.svh" 
import sva_delay_repeat_pkg::*;
module top; 
    timeunit 1ns;     timeprecision 100ps;  
    bit clk, a, b, c=1;  
    int r=2; 
    default clocking @(posedge clk); 
    endclocking
    initial forever #10 clk=!clk;  
    
    sequence q1; 
        a ##1 b; 
    endsequence 

    ap_abr: assert property(a |-> dynamic_repeat(q1, r) ##1 c); 
    ap_abr_fix2: assert property(a |-> q1[*2] ##1 c); 
    ap_abr_fix0: assert property(a |-> q1[*0] ##1 c); 

    ap_delay:assert property(a |-> dynamic_delay(r) ##0 b);  
    ap_delay_fix2:assert property(a |-> ##2 1'b1 ##0 b); 
    ap_delay_fix0:assert property(a |-> ##0 1'b1 ##0 b);   

    property p_or;
        int v; 
        ($rose(a), v=r) |-> (##1 (1,v=v+1'b1) ##1 dynamic_delay(v) ##0 c) or 
                            (dynamic_delay(v) ##0 c);
    endproperty 
    ap_or: assert property(p_or);  


    initial begin 
        repeat(100) begin 
            @(posedge clk); #2;   
            if (!randomize(a, b, c)  with 
            { a dist {1'b1:=1, 1'b0:=1};
              b dist {1'b1:=1, 1'b0:=1}; 
              c dist {1'b1:=1, 1'b0:=1};            
        }) `uvm_error("MYERR", "This is a randomize error")
        end 
        #1 r=0; 
        repeat(100) begin 
            @(posedge clk); #2;   
            if (!randomize(a, b, c)  with 
            { a dist {1'b1:=1, 1'b0:=1};
              b dist {1'b1:=1, 1'b0:=1}; 
              c dist {1'b1:=1, 1'b0:=1};            
        }) `uvm_error("MYERR", "This is a randomize error")
        end 
        $stop; 
    end 
endmodule

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr