SVA: throughout corner case | sig1 must be stable throughout sig2

SystemVerilog
, ,
3

In reply to Ankit Bhange:

Disabling the assertion when sig2 goes down seems to do the trick. Is this approach correct?

NO!


// The throughout operator specifies that a signal (expression) must hold throughout a sequence.
 ( b throughout R )[/b] is equivalent to [b]( b [*0:$] intersect R ) 
// Use the 
sequenc1 interesect sequence2 // and sequence1 is 
 ($stable(sig1)[*1:$] ##1 !sig2) // Thus, if sig2==0 after 4 cycles, 
//                          the consequent thread that will match will be 
 ($stable(sig1)[*3] ##1 !sig2 // sig2==0 at cycle 4 

property sig1_stable_throughout_sig2 (logic sig1, sig2);
     $rose(sig2) |-> ##1 ($stable(sig1)[*1:$] ##1 !sig2) intersect !sig2[->1];
endproperty 
// As mentioned in a previous post, I prefer to use |-> ##1 instead |=> 
// See my next post

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact http://cvcblr.com/home.html
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
…

  1. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats - SystemVerilog - Verification Academy
  2. Free books: Component Design by Example https://rb.gy/9tcbhl
    Real Chip Design and Verification Using Verilog and VHDL($3) https://rb.gy/cwy7nb
  3. Papers: