The Absence Property Pattern is used to specify portions of a design model's verification execution where a specific state or event1 should never occur. Also known Never.
In the normal execution of an RTL state-based model, there are often specific events or states that should never occur. One of the most common examples of the Absence Property Pattern is mutual exclusion.
Any event that can be expressed as a proposition (e.g., Boolean equation), and describes undesirable behavior in a design, can be formulated into an absence property.
View & Download:
To view the entire Absence Property Pattern, please login with your Verification Academy Full Access account.