The Response Property Pattern is used to specify portions of a design model's execution for cause-effect relationships between a pair of states or events1. An occurrence of the first, the cause, must be followed by an occurrence of the second, the effect. Also known as Follows and Leads-to.
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. Response properties, which specify that a specific cause must be followed by a specific effect, occur quite commonly in specifications of concurrent systems. Perhaps the most common example involves describing a requirement where a resource must be granted after it is requested.
The Response Property Pattern can be useful for specifying control signal handshakes, portions of a protocols, and state transitions.
View & Download:
To view the entire Response Property Pattern, please login with your Verification Academy Full Access account.