Specification Patterns

Specification Patterns provide solutions to notational problems when specifying design intent. Probably the most prevalent form of formally specifying design intent in the digital verification domain is through the use of properties, which can be implemented as either assertions or cover properties.

The specification patterns contained in our library are divided into the follow two subcategories are: Occurrence Properties and Order Properties. Occurrence Property patterns require that either some state or event must occur or not occur. Alternatively, Order Property patterns constrain the order of states and events.

To learn more about the details of the Verification Academy Patterns Library and Specification Patterns, View | Download our paper, Verification Patterns—Taking Reuse to the Next Level.

Occurrence Property Patterns:

Order Property Patterns:

Occurrence Property Patterns

Universality Property Pattern

Intent:

The Universality Property Pattern is used to specify portions of a design model’s verification execution that contains states or events¹ that have a desired property. Also known as Henceforth and Always.

Motivation:

In the verification execution of an RTL state-based model, there are often specific conditions (i.e., events or states) that must always hold true at every clock cycle. As an example, let us consider the case of a FIFO of size N, where a FIFO controller keeps track of the next available position in the FIFO storage through a write counter (representing locations 0 through N-1). If the write counter indicates that the current FIFO depth is N-1 (that is, the FIFO is currently full), then the FIFO full status bit should be set. Similarly, if the FIFO depth is less than N-1, then the FIFO full status bit should not be set.

Applicability:

Any condition (i.e., event or state) that can be expressed as a Boolean equation and describes desirable state or behavior in a design for each clock cycle can be formulated into a Universality Property.

To view the entire Universality Property Pattern , please login with your Verification Academy Full Access account.

Existence Property Pattern

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 event¹. 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.

To view the entire Existence Property Pattern , please login with your Verification Academy Full Access account.

Bounded Existence Property Pattern

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 events¹.

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.

To view the entire Bounded Existence Property Pattern , please login with your Verification Academy Full Access account.

Forbidden Sequence Property Pattern

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 events¹.

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.

To view the entire Forbidden Sequence Property Pattern , please login with your Verification Academy Full Access account.

Order Property Patterns

Precedence Property Pattern

Intent:

The Precedence Property Pattern is used to specify portions of a design model’s execution for relationships between a pair of states or events,¹ 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.

Motivation:

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.

Applicability:

The Precedence Property Pattern can be useful for specifyingcontrol signal handshakes, portions of a protocols, and state transitions.

To view the entire Precedence Property Pattern , please login with your Verification Academy Full Access account.

Response Property Pattern

Intent:

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 events¹. 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.

Motivation:

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.

Applicability:

The Response Property Pattern can be useful for specifying control signal handshakes, portions of a protocols, and state transitions.

To view the entire Response Property Pattern , please login with your Verification Academy Full Access account.

Response Chain Property Pattern

Intent:

The Response Chain Property Pattern is used to specify portions of a design model’s execution for relationships between chains (i.e., sequence of states or events), where an occurrence of the cause chain must be followed by an occurrence of the effect chain.

Motivation:

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 Chain properties, which specify that a specific cause chain must be followed by a specific effect chain, occur quite commonly in specifications of concurrent systems. Perhaps the most common example would be specifying legal bus state transitions. For instance, if the bus transitions through a specific sequence of states S1, then the bus must transition through a sequence of states S2.

Applicability:

The Response Chain Property Pattern can be useful for specifying control handshake sequences, portions of a protocol, and sequences of state transitions.

To view the entire Response Chain Property Pattern , please login with your Verification Academy Full Access account.

Precedence Chain Property Pattern

Intent:

The Precedence Chain Property Pattern is used to specify portions of a design model’s execution for relationships between chains (i.e., sequence of states or events¹), where an occurrence of a cause chain must be have been preceded by an occurrence of an effect chain. We say that an occurrence of the effect chain is enabled by an occurrence of the cause chain.

Motivation:

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 Chain 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 complex request-grant-start-done transaction.

Applicability:

The Precedence Chain Property Pattern can be useful for specifying control handshake sequences, portions of a protocols, and state transitions.

To view the entire Precedence Chain Property Pattern , please login with your Verification Academy Full Access account.

This site uses cookies to improve your user experience and to provide you with content we believe will be of interest to you. Detailed information on the use of cookies on this website is provided in our Privacy Policy. By using this website, you consent to the use of our cookies.

Languages & Standards

Methodologies

Techniques & Tools

Universal Verification Methodology (UVM)

Featured Courses

Additional Courses

Formal-Based Techniques

Analog/Mixed Signal

UVM Forum

SystemVerilog Forum

Coverage Forum

Additional Forums

Implementation Patterns

Pattern Resources

UVM Cookbook

Coding Guidelines & Deployment

Coverage Cookbook

Featured & On-Demand

On-Demand Library

Recording Archive

Conferences & WRG

Siemens EDA Learning Center

Blog & News

Verification Horizons Publication

About Us

Training

Portfolio

Explore

Siemens

Contact