Search code examples
system-verilogverificationformal-verificationsystem-verilog-assertions

How to write a property in System verilog assertions?

I want to write a property in SVA to formally verify a behavior.

Here is what I want to:

property prop1(sig1,sig2,sig3,sig4);
    @(posedge clk)
    $fell(sig1) ##[1:$] first_match($fell(sig2)) ##0 sig3 |-> sig4 == sig3;
endproperty

How can I rewrite the above property so that after sig1 falls, it stays LOW during remaining Evaluation cycles?

Note: I do not want to put sig1 as disable iff (sig1)

Solution 
  • property prop1(sig1,sig2,sig3,sig4);
    @(posedge clk)
    (!sig1) throughout (##[1:$] first_match($fell(sig2)) ##0 sig3) 
          |-> sig4 == sig3;
endproperty

    See section 16.9.9 Conditions over sequences in the 1800-2012 LRM