Intent:
The Forbidden Sequence Property Pattern is used to specify portions of a design model's verification execution that forbids a specified sequence of designated states or events1.
Motivation:
In the normal verification execution of an RTL model, there are often specific sequences of states or events that must never occur. The classic example of applying the Forbidden Sequence Property Patterns relates to checking fairness in an arbiter. For example, if a specific client A issues a request to the arbiter, and the arbiter issues a sequence of multiple grants to client B before client A is issued a grant, then the arbiter is not fair.
Applicability:
Any sequence of states or events that describes undesirable behavior in a design, can be formulated into an forbidden sequence property.
 View & Download:
To view the entire Forbidden Sequence Property Pattern, please login with your Verification Academy Full Access account.
|
