SVA not triggering

SystemVerilog
,
1

Hi all

I was trying to write an SVA property as below:

property alushort(rst_condn, sig);
@(posedge clk_in) disable iff(rst_condn)
	$rose(sig) |-> overflow;
endproperty
short:assert property(alushort(!add, carry&add))
else $error ("ADDSHORT failed at %t", $time);

The issue is when add signal is high, which is when I want the SVA to trigger, it doesn’t seem to work fine even when there is a carry going high.
I have ensured that the clk_in is a free running clock.

Please help me out with this.

Regards

2

In reply to Sirius44:
The issue I see is when carry&add rises and add then falls.
$rose(add && carry)is sampled a the clocking event in the Preponed Region.
add goes to zero in the NBA region, thus the property reset occurs in that region (maybe tool dependent, but the disable is asynchronous. The assertion is evaluated in the Observed region, by then the disabled already took effect.

carry == 1 at all cycles 
clk  +------+      +------+
            +------+  
add         +------+
      ------+      +------+

disable  ---+      +------+
            +------+

The SOLUTION: Use disable iff($sampled(rst_condn))


import uvm_pkg::*; `include "uvm_macros.svh" 
module top; 
    timeunit 1ns;     timeprecision 100ps;    
    bit clk_in, add, carry, overflow=1'b1;  
    int count; 
    initial forever #10 clk_in=!clk_in;  
    property alushort(rst_condn, sig);
        @(posedge clk_in) disable iff($sampled(rst_condn)) // <------ Use this 
                     // disable iff(rst_condn)  // <--- MOT this 
        $rose(sig) |-> overflow;
    endproperty
    short:assert property(alushort(!add, carry&add)) count <= count+1'b1; 
    else $error ("ADDSHORT failed at %t", $time);  
    
    initial begin 
        bit vadd, vcarry; 
        repeat(200) begin 
            if (!randomize(vadd, vcarry)  with 
            { vadd dist {1'b1:=3, 1'b0:=1};
              vcarry dist {1'b1:=1, 1'b0:=0};            
            }) `uvm_error("MYERR", "This is a randomize error")
            @(posedge clk_in); 
            add <= vadd; carry <= vcarry; 
        end 
        $display("%t count=%d", $realtime, count);
        $stop; 
    end 
endmodule

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

See Paper: VF Horizons:PAPER: SVA Alternative for Complex Assertions | Verification Academy

3

In reply to ben@SystemVerilog.us:

Hi Ben

Thanks for the reply!

There are multiple SVAs instances using the same property.

  1. In this case, add is already high, but I am checking when a carry comes, add&carry would be 1, so I look for the rise of (add&carry) to check the SVA - tHis is still not resolved

        +--------------------------------------------------------+

add ±-----+ ±-----------
±----------------
carry----------+
±----------------
overflow-------+

Expected SVA----*trigger here when it sees a $rose(carry)

  1. SVA itself not triggering - $sampled doesn’t seem to address the issue.

Thanks!

4

In reply to Sirius44:

932×625 71.8 KB

but I am checking when a carry comes, add&carry would be 1,
If you are oncerned avbout th ecarry only, then use
$rose(carry) |-> overflow;
The assertion is doing what you wrote, $rose(carry && add) |-> overflow;

 
Expected SVA----*trigger here when it sees a $rose(carry)
Thus, a rise in carry with add== 1 and no rose, or 
      a rose(add) and carry==1, no rose, 
      would cause a trigger. BTW, use the && instead of the &  

property alushort(rst_condn, sig);
        @(posedge clk_in) disable iff($sampled(!add))  
        $rose(carry && add) |-> overflow;
endproperty

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact http://cvcblr.com/home

See Paper: VF Horizons:PAPER: SVA Alternative for Complex Assertions - SystemVerilog - Verification Academy

5

In reply to ben@SystemVerilog.us:
Thanks Ben for the solution.