In reply to gidon:
I would think that for formal verification, your 2nd suggestion is best because you document the assumptions of your design or zones.
2.write assumptions for the different situations and use the relevant assumptions when running the assertion (separating the design to different ‘zones’).
When you say model the specific situation to check the specific assertion (this can be done inline the property itself but will result in a very robust property or outside the property with some extra logic)
Are you saying that the property itself takes into account the assumptions?
That looks complex. Also, it does not separate the properties from the assumptions that model the outside environment. By documenting and reviewing the assumptions, you get a higher level of assurance that this is indeed the expected environment. The formal verification tool should be able to handle the analysis of all scenarios.
My 2 cents …
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
- Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 978-1539769712
- 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
- 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
See Paper: VF Horizons:PAPER: SVA Alternative for Complex Assertions | Verification Academy