The Precedence Property Pattern is used to specify portions of a design model's execution for relationships between a pair of states or events,1 where the occurrence of the first is a necessary pre-condition for an occurrence of the second. We say that an occurrence of the second is enabled by an occurrence of the first.
In the normal execution of an RTL state-based model, there is often a cause and effect relative order in which multiple states or events occur during system execution. Precedence properties, which specify that a specific effect must have been preceded by a specific cause, occur quite commonly in specifications of concurrent systems. Perhaps the most common example involves describing a requirement where a grant must have been preceded by a request.
The Precedence Property Pattern can be useful for specifyingcontrol signal handshakes, portions of a protocols, and state transitions.
View & Download:
To view the entire Precedence Property Pattern, please login with your Verification Academy Full Access account.