Assertion for signal stability inside a window

[alexkidd84]

Hi all,
my purpose is to check that ‘c’ is stable since a fell down (and b is low) and until a goes high again.

I wrote this SVA:

assert property (@(posedge clk) disable iff (!reset_n) (!a && !b |=> ($stable(c) throughout (a) [-> 1])))

I’ve uploaded the image here…

The problem is that the assertion fails because it’s checking the clock next a returns high
Can anyone help me with this?

[ben2]

In reply to alexkidd84:

Your requirements are not clear; I believe that this is what you are trying to express:
At (fell(a) && !b) then starting from the next clock “c” holds the value it had at the fell(a)
until a rose(a). At the rose(a), “c” can change value.

//my purpose is to check that 'c' is stable since a fell down (and b is low) 
    //and until a goes high again. 
    property p_cstable;
        bit v; 
        @(posedge clk) disable iff (!reset_n)
        ($fell(a) && !b, v=c )|=>  c==v s_until  $rose(a);
    endproperty 
    ap_c_stable: assert property(p_cstable);  

If this is not your requirements, then please re-express them again.
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr

• SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
• 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 978-1539769712
• 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

---

1. SVA Alternative for Complex Assertions
   Verification Horizons - March 2018 Issue | Verification Academy
2. SVA: Package for dynamic and range delays and repeats | Verification Academy
3. SVA in a UVM Class-based Environment
   SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy

[ben2]

In reply to ben@SystemVerilog.us:

// Ths is equivalent to the  property p_cstable
ap_c_stable2: assert property(@ (posedge clk) disable iff (!reset_n)
       ($fell(a) && !b)|=> $stable(c) s_until  $rose(a));  

    property p_cstable;
        bit v; 
        @(posedge clk) disable iff (!reset_n)
        ($fell(a) && !b, v=c )|=>  c==v s_until  $rose(a);
    endproperty  
    ap_c_stable: assert property(p_cstable);  
      

[alexkidd84]

Thanks Ben!!
I was using 2005 sv version and I didn’t know the construct s_until.