Throughout construct in SVA

SystemVerilog
1

I am using throughout construct in the snippet shown below:

@posedge(clk)
( (z==3|| z==4 || z==6) && ($changed(c) && (c==0)) ) → ##3 !a ##2 b ##1 ( !a && b throughout !c);

Here
after ##3 + ##2 = ##5ns I see my assertion working fine till b is high.

Now
after ##5 + ##1 = ##6ns, I am checking for ( !a && b throughout !c);

I want a=0 and b=1 to stay the same until c=0 (Correction: while c=0), so I used throughout but it doesn’t seem to be working.

In my simulation b changed its value to 0 at approximately ##8ns while c was still==0, and my assertion still didn’t fail. The assertion should have failed.

Is this the right way of handling throughout construct?

2

In reply to abhi9891:

"( !a && b throughout !c);

I want a=0 and b=1 to stay the same until c=0 so I used throughout"
Use the goto

... ( !a && b throughout !c[->1]);

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
3

In reply to ben@SystemVerilog.us:

Hi Ben,
Could you please explain why the absence of goto operator does not make the assertion fail when b==0 and c==0?

4

In reply to ManjunathBhat:

In reply to ben@SystemVerilog.us:
Hi Ben,
Could you please explain why the absence of goto operator does not make the assertion fail when b==0 and c==0?


!a && b throughout !c)
// states that you want (!a && b) to be True during the ONE-CYCLE sequence (!c) 
// Which is then the same as 
!a && b && !c
// However, 
!c[->1] is equivalent to  c[*0:$] ##1 c // OOPS, that should be ..##1!c
!c[->1] is equivalent to  c[*0:$] ##1 !c

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr

  1. SVA Alternative for Complex Assertions
    https://verificationacademy.com/news/verification-horizons-march-2018-issue
  2. SVA: Package for dynamic and range delays and repeats - SystemVerilog - Verification Academy
  3. SVA in a UVM Class-based Environment
    https://verificationacademy.com/verification-horizons/february-2013-volume-9-issue-1/SVA-in-a-UVM-Class-based-Environment
5

In reply to ben@SystemVerilog.us:

"// However,
!c[->1] is equivalent to c[*0:$] ##1 c "

Its not !c[*0:] ##1 !c instead of c[*0:] ##1 c ?

6

In reply to ben@SystemVerilog.us:

“I want a=0 and b=1 to stay the same until c=0 so I used throughout.”

I meant I want a=0 and b=1 when c=0.

So (!a && b throughout !c[->1]); does the same check right?

7

In reply to abhi9891:

 
!c[->1] is equivalent to  c[*0:$] ##1 c // OOPS, that should be ..##1!c
!c[->1] is equivalent to  c[*0:$] ##1 !c 
a[->1] is equivalent to !a[*0:$] ##1 a
8

In reply to abhi9891:


// "I want a=0 and b=1 to stay the same until c=0 so I used throughout."
// (!a && b throughout !c[->1]); does the same check right?
( b throughout R ) is equivalent to ( b [*0:$] intersect R )
/* thus !a && b  is true at al cycles until (and inclusive) !c 
//  !c[->1] is equivalent to  c[*0:$] ##1 !c // Updated my error in previous reply
  
// I meant I want a=0 and b=1 when c=0. */
// If you mean a and  b can be anything until c==0, at which cycle you expect a=0 and b=1  
( (z==3|| z==4 || z==6) && $fell(c) ) -> 
        ##3 !a ##2 b   ( ##1:$] [!a && b && !c);

// BTW
  ($changed(c) && (c==0))  is same as $fell(c)

Ben SystemVerilog.us

9

In reply to ben@SystemVerilog.us:

In reply to abhi9891:

 
!c[->1] is equivalent to  c[*0:$] ##1 c // OOPS, that should be ..##1!c
!c[->1] is equivalent to  c[*0:$] ##1 !c 
a[->1] is equivalent to !a[*0:$] ##1 a

Thanks a lot once again for the responses.

…(!a &&b throughout c[->1]); works for my requirement.

@posedge(clk)
( (z==3|| z==4 || z==6) && ($changed(c) && (c==0)) ) → ##3 !a ##2 b ##1 ( !a && b throughout c[->1]);

where,
*c[->1] is !c[0:$] ##1 c

Hence in,
…(!a && b throughout c[->1]);

  • !a && b are checked for true while c is low throughout.
  • Assertion fails when !a && b return false, throughout when c is low.
  • Assertion stops when c goes high.