Regarding implication operator in SVA

SystemVerilog
, , ,
1

Hello,

I’m not very familiar with ABV and SVA, but someone a while back mentioned about avoiding the implication operator in cover properties

->/=>

the person was not able to elaborate his answer, so I’d like to know if this is correct? If so that means that cover properties should be always written something like

a##0b //for a->b

or

a##1b //for a=>b

The other question is related to chained implication operator

a->b->c

my understanding is that in case of a occurring but b never happening this type of assertion will not fail, is this the case and why?

Regards,

-R

2

In reply to rgarcia07:

Hello,
I’m not very familiar with ABV and SVA, but someone a while back mentioned about avoiding the implication operator in cover properties

->/=>

the person was not able to elaborate his answer, so I’d like to know if this is correct? If so that means that cover properties should be always written something like

a##0b //for a->b

or

a##1b //for a=>b

The cover property is typically used to cover in tests critical sequences. For example, you want to insure that in testing a FIFO that you address the sequence fifo_full ##1 push ##0 !pop;
The assertion of properties is typically provided by the tool.

The other question is related to chained implication operator

a->b->c

my understanding is that in case of a occurring but b never happening this type of assertion will not fail, is this the case and why?
Regards,
-R

 b |-> c; if b==0 the property is vacuous. 
a |-> (b |-> c) if a==1 you check the property (b |-> c) ;
There, if b==0 the property is vacuous. 
I do not recommend the use of multiple implication operators. You can write multiple small assertions.

Ben systemverilog.us
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
    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
1 Like
3

In reply to ben@SystemVerilog.us:

Thank you very much for your explanation Ben.