Issue with SVA

Hi,
I am trying to write following property. As per my understanding of ‘or’ construct if sig is deasserted or if $time-t3 becomes > 100ns antecedent should become true. But I see that even though sig is deasserted much before consequent is evaluated only when $time-t3>100ns. What is wrong with following property.

property test1;
time t3,t4;
@(posedge clk)disable iff(reset==1)($rose(sig),t3=$time) ##1 ((!sig[->1]) or (($time-t3)>100ns)[->1]) |-> !sig;
endproperty:test1


// You need a first_match because you have multiple threads, 
// and all threads of an antecedent must be tested before the assertion terminates. 
// Thus, if sig==1'b1 before ($time-t3)>100ns), the assertion will terminate when 
// ($time-t3)>100ns) is true.  Thus, change the property to: 
//--------------------------------------------------------------------------
property test1;
time t3,t4;
@(posedge clk)disable iff(reset==1)
   first_match(
     (($rose(sig),t3=$time) ##1 !sig[->1]) or (($time-t3)>100ns)[->1]
              ) |-> !sig;
endproperty:test1

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us

  • SystemVerilog Assertions Handbook 3rd Edition, 2013 ISBN 878-0-9705394-3-6
  • A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
  • Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004, ISBN 0-9705394-6-0
  • Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 0-9705394-2-8
  • Component Design by Example ", 2001 ISBN 0-9705394-0-1
  • VHDL Coding Styles and Methodologies, 2nd Edition, 1999 ISBN 0-7923-8474-1
  • VHDL Answers to Frequently Asked Questions, 2nd Edition ISBN 0-7923-8115

In reply to ben@SystemVerilog.us:

Thanks Ben. It works