Intent:
The Existence Property Pattern is used to specify portions of a design model's verification execution that contains an instance of a certain state or event1. Also known as Eventually or Future.
Motivation:
In the normal execution of an RTL state-based model, there are often specific states or events that must eventually occur. The classic example of existence is specifying termination. For example, on all executions do we eventually reach a terminal state (e.g., a specific FSM can eventually return to its initial state under any condition).
Applicability:
The Existence Property Pattern is useful for specifying that a system will not encounter deadlock, livelock, and starvation.
 View & Download:
To view the entire Existence Property Pattern, please login with your Verification Academy Full Access account.
|
