Understanding the performance impact of SVA construct

SystemVerilog
,
1

Requirement -
RTL.sb shouldn’t change between cond_a and cond_b.

Though there are multiple ways to write assertion for this requirement, I have chosen below one.
Can someone please help me understand the performance impact of this style of coding (mainly due to the use of [*0:$])?
Is it good/bad?


 property p_sb_check;
      logic [5:0] temp_sb;
      @(posedge clk) disable iff (reset)
      (cond_a, temp_sb = RTL.sb) |-> (temp_sb === RTL.sb) [*0:$] ##1 cond_b ##0 (temp_sb === RTL.sb) ;
 endproperty

Thanks in advance.

PS: I have not used $rose in the antecedent because till cond_b becomes true, cond_a will never trigger and also cond_a is 1 clock pulse. (There are separate checks for all these)

2

In reply to naveensv:

Looks OK to me. You may want to qualify the consequent as “strong”.
Ben systemverilog.us

3

In reply to naveensv:

You can also write this as

property p_sb_check;
      @(posedge clk) disable iff (reset)
      cond_a |=> $stable(RTL.sb) until_with cond_b;
endproperty
4

In reply to dave_59:
There is a saying “All roads lead to Rome!”
Your assertion is OK. Is Dave’s approach better? The way I see it, it really does not matter. Yours (and generally my style) is more waveform-like in defining the requirements. Dave’s is more English, higher-level definition; however, it requires some mental exercises to convert the stable until_with to its meaning.

Addressing your concern *"the performance impact of this style of coding (mainly due to the use of [0:$])? Is it good/bad?".
I don’t believe that this is a concern. I am not a simulator builder, thus, I don’t know the implementation. However, In my paper SVA Alternative for Complex Assertions
Verification Horizons - March 2018 Issue | Verification Academy
I demonstrate a model for the assertions. Your model is of the form:


 (a, v = c) |-> (v === c) [*0:$] ##1 b ##0 (v === c) ; 
// Using task triggered with a fork join_none, it looks like this 
// Note the while loop that represents the [*0:$]
//  I don't see a heavy load or complexity here, though the consequent is multithreaded
task automatic t_b();
        //  (a, v = c) |-> (v === c) [*0:$] ##1 b ##0 (v === c) ; 
        logic [5:0] v; 
        if(a) v=c;
        else return;  // (a, v = c) |->
        //
        while (b==1'b0) begin
            v_eql_c_till_b: assert(v === c); // (v === c) [*0:$] ##1 b
            if(v != c) begin 
                -> e_fail; 
                return; 
            end
            else -> e_pass;// for debug 
            @(posedge clk); 
        end
        // b==1'b1
        v_eql_c_at_b: assert (v === c); // ##0 (v === c) ;  
        if(v != c) -> e_fail; else -> e_pass;// for debug    
    endtask : t_b

// This is the testbench


import uvm_pkg::*; `include "uvm_macros.svh" 
module top; 
    bit clk, a, b, reset=0; 
    logic [5:0] c=6'b100001;  
    event e_pass, e_fail;  // for debug  
    event e_delay; 
    let tID="My model";
    initial forever #10 clk=!clk; 
    property p_sb_check;
        logic [5:0] v;
        @(posedge clk) disable iff (reset)
        (a, v = c) |-> (v === c) [*0:$] ##1 b ##0 (v === c) ; 
    endproperty     
    
    ap_sb_check : assert property(p_sb_check);
    // Action block is not used here 
    //  t_b(i, last_range, failing, done);
    task automatic t_b();
        //  (a, v = c) |-> (v === c) [*0:$] ##1 b ##0 (v === c) ; 
        logic [5:0] v; 
        if(a) v=c;
        else return;  // (a, v = c) |->
        //
        while (b==1'b0) begin
            v_eql_c_till_b: assert(v === c); // (v === c) [*0:$] ##1 b
            if(v != c) begin 
                -> e_fail; 
                return; 
            end
            else -> e_pass;// for debug 
            @(posedge clk); 
        end
        // b==1'b1
        v_eql_c_at_b: assert (v === c); // ##0 (v === c) ;  
        if(v != c) -> e_fail; else -> e_pass;// for debug    
    endtask : t_b  
    
    always  @(posedge clk)  begin // emulate the assertion firing
        fork 
            t_b();  // Assertion for the above property emulated with a task 
            // .. other tasks representing properties 
        join_none
    end
    
    initial begin  
        repeat(200) begin 
            repeat(1) @(posedge clk); #2;   
            if (!randomize(a, b, c)  with 
            { c dist {6'b100000:=1, 6'b011111:=1}; 
        }) `uvm_error("MYERR", "This is a randomize error");
    end 
    $finish; 
    end 
endmodule

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

  1. SVA Alternative for Complex Assertions
    Verification Horizons - March 2018 Issue | Verification Academy
  2. SVA: Package for dynamic and range delays and repeats | Verification Academy
  3. SVA in a UVM Class-based Environment
    SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy
5

In reply to ben@SystemVerilog.us:

Thank you both :)

6

shouldn’t it be

property p_sb_check;
      @(posedge clk) disable iff (reset)
      cond_a |-> $stable(RTL.sb) until_with cond_b;
endproperty

?