'disable iff' not working when variables used in SVA property

SystemVerilog
, , ,
1

Hello.

Below is the example code using variable in property with disable statement.


property p_test;
    int t;
    @(negedge clk) disable iff (!rstn || a)
    $rose(b) |-> ##0 (1, t = 100)
                 ##1 (b, t = t - 1)[*0:$]
                 ##0 t <= 0;
endproperty
a_test: assert property (p_test) else `uvm_error("debug", "error");

Assume both ‘a’ and ‘b’ are 0.
When ‘b’ is asserted, the property will be enabled.
If ‘a’ is assert 50 clks after the assertion of ‘b’, I expect the property to be canceled.
If the property fails here, will it be a problem of the tool?
Please correct me if I’m wrong.

Below is the similar code without using variable in the property.


property p_test;
    @(negedge clk) disable iff (!rstn || a)
    $rose(b) |-> b[*100];
endproperty
a_test: assert property (p_test) else `uvm_error("debug", "error");

No issue with this type of property.

I would like to know if I am understanding ‘disable iff’ correctly.
If there is nothing wrong with the first code, I might contact the vendor.
(I used VCS and Verdi.)

2

In reply to Jung Ik Moon:

The property should be written aa:

property p_test;
    int t;
    @(negedge clk) disable iff (!rstn || a)
    $rose(b) |-> ##0 (1, t = 100)
                 ##1 (b, t = t - 1)[*0:$]
                 ##1 t <= 0; // <<<---
endproperty 
A[*0]  ##0 b // is a no match
A[*0]  ##1 b // is same as "b" 
//another option 
property p_test;
    int t;
    @(negedge clk) disable iff (!rstn || a)
    $rose(b) |-> ##0 (1, t = 100)
                 ##1 (b, t = t - 1)[*1:$] // <<<---
                 ##0 t <= 0;
endproperty

Aside from that, the disable should work as you described.
Try this change.
Ben Ben@systemverilog.us

3

In reply to ben@SystemVerilog.us:

Hello Ben,
I’ve tried your first suggestion and it works perfect.
Thanks!