Can someone point me out the differences between a checker and assertions?
Thanks in advance
In reply to shrads13:
The word checker has several meanings depending upon the context.
- Plain casual English In the context of verification, a checker is anything that is used to verify a design. Often, it implies some assertions which could be written in code, PSL, or SVA. In that sense, it is a loose term.
- SystemVerilog In the context of SystemVerilog 1800’2012 Chapter 17, a checker is a SystemVerilog construct that encapsulates assertions and supporting code. That checker can be instantiated or bound to a module, just like any other module instantiation. However, the checker has one other characteristic in that it can also be instantiated inline within several statements of a module or interface, given precise rules (e.g., inside always, initial, final, generate, …).
In my SVA Handbook 4th Edition, 2016 I provide a detailed explanation of those rules with lots of examples. Below is a brief intro into this topic.
The origin of the checker construct stems from the formal verification world, and hence, certain restrictions are imposed in the modeling styles of a checker. A checker is not intended to be a replacement to a module/interface, as its goal is strictly for verification, including formal verification. Hence the modeling styles allowed in a checker represent a subset suitable for the definition of assertions and coverage with the supporting environment.
IEEE 1800-2012 significantly enhanced the 1800-2009 version of a checker to encapsulate a set of properties, assertions, cover statements, assumptions, and any auxiliary procedural code needed to validate the behavior of the design in simulation and in formal verification. It is expected that the checker will play a significant role in the adoption of assertions and in the definition of assertion libraries. Since its last update, some vendors are now supporting the checker construct in simulation; however, as of the date of this publication, checker are weakly supported by very few formal verification tools with restrictions on types of assertions (e.g., static) and types of instantiations (e.g., static, rather than procedural). Checkers are ignored in synthesis, As users become more comfortable with checkers, it is expected to see more support in formal verification.
One significant advantage of checkers is that they clearly mark the scope of any auxiliary code used to support assertion and verification libraries. This clear demarcation between assertion library code and RTL code enhances code understanding; eliminates potential conflicts between RTL code and supporting code for assertions (such as the use of always blocks and updates of variables needed for assertions); and allows synthesis or other processing tools to concentrate on one specific region of the model, such as the RTL only.
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
- 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