Intent:
The Bounded Existence Property Pattern is used to specify portions of a model's verification execution that contains at most a specified number of instances of designated state transitions or events1.
Motivation:
In the normal execution of an RTL state-based model, there are often specific states or events that must occur at most a limited number of times. For example, if we wish to specify that client 1 can access a memory at most twice while client 2 is waiting, we would apply the Bounded Existence Property Pattern.
Applicability:
The Bounded Existence Property Pattern is natural for specifying bounded overtaking properties, such as granting a client at most a fixed number of accesses to a shared resource while another client is waiting.
 View & Download:
To view the entire Bounded Existence Property Pattern, please login with your Verification Academy Full Access account.
|
