Verification Academy

Search form

My Account Menu

  • Register
  • Log In
  • Topics
  • Courses
  • Forums
  • Patterns Library
  • Cookbooks
  • Events
  • More
  • All Topics
    The Verification Academy offers users multiple entry points to find the information they need. One of these entry points is through Topic collections. These topics are industry standards that all design and verification engineers should recognize. While we continue to add new topics, users are encourage to further refine collection information to meet their specific interests.

    • Languages & Standards

      • Portable Test and Stimulus
      • Functional Safety
      • Design & Verification Languages

    • Methodologies

      • UVM - Universal Verification Methodology
      • UVM Framework
      • UVM Connect
      • FPGA Verification
      • Coverage

    • Techniques & Tools

      • Verification IP
      • Simulation-Based Techniques
      • Planning, Measurement, and Analysis
      • Formal-Based Techniques
      • Debug
      • Clock-Domain Crossing
      • Acceleration
  • All Courses
    The Verification Academy is organized into a collection of free online courses, focusing on various key aspects of advanced functional verification. Each course consists of multiple sessions—allowing the participant to pick and choose specific topics of interest, as well as revisit any specific topics for future reference. After completing a specific course, the participant should be armed with enough knowledge to then understand the necessary steps required for maturing their own organization’s skills and infrastructure on the specific topic of interest. The Verification Academy will provide you with a unique opportunity to develop an understanding of how to mature your organization’s processes so that you can then reap the benefits that advanced functional verification offers.

    • Universal Verification Methodology (UVM)

      • Advanced UVM
      • Basic UVM
      • Introduction to UVM
      • UVM Connect
      • UVM Debug
      • UVMF - One Bite at a Time

    • Featured Courses

      • Introduction to ISO 26262
      • Introduction to DO-254
      • Clock-Domain Crossing Verification
      • Portable Stimulus Basics
      • Power Aware CDC Verification
      • Power Aware Verification
      • SystemVerilog OOP for UVM Verification

    • Additional Courses

      • Assertion-Based Verification
      • An Introduction to Unit Testing with SVUnit
      • Evolving FPGA Verification Capabilities
      • Metrics in SoC Verification
      • SystemVerilog Testbench Acceleration
      • Testbench Co-Emulation: SystemC & TLM-2.0
      • Verification Planning and Management
      • VHDL-2008 Why It Matters

    • Formal-Based Techniques

      • Formal Assertion-Based Verification
      • Formal-Based Technology: Automatic Formal Solutions
      • Formal Coverage
      • Getting Started with Formal-Based Technology
      • Handling Inconclusive Assertions in Formal Verification
      • Sequential Logic Equivalence Checking

    • Analog/Mixed Signal

      • AMS Design Configuration Schemes
      • Improve AMS Verification Performance
      • Improve AMS Verification Quality
  • All Forum Topics
    The Verification Community is eager to answer your UVM, SystemVerilog and Coverage related questions. We encourage you to take an active role in the Forums by answering and commenting to any questions that you are able to.

    • UVM Forum

      • Active Questions
      • Solutions
      • Replies
      • No Replies
      • Search
      • UVM Forum

    • SystemVerilog Forum

      • Active Questions
      • Solutions
      • Replies
      • No Replies
      • Search
      • SystemVerilog Forum

    • Coverage Forum

      • Active Questions
      • Solutions
      • Replies
      • No Replies
      • Search
      • Coverage Forum

    • Additional Forums

      • Announcements
      • Downloads
      • OVM Forum
  • Patterns Library
    The Verification Academy Patterns Library contains a collection of solutions to many of today's verification problems. The patterns contained in the library span across the entire domain of verification (i.e., from specification to methodology to implementation—and across multiple verification engines such as formal, simulation, and emulation).

    • Implementation Patterns

      • Environment Patterns
      • Stimulus Patterns
      • Analysis Patterns
      • All Implementation Patterns

    • Specification Patterns

      • Occurrence Property Patterns
      • Order Property Patterns
      • All Specification Patterns

    • Pattern Resources

      • Start Here - Patterns Library Overview
      • Whitepaper - Taking Reuse to the Next Level
      • Verification Horizons - The Verification Academy Patterns Library
      • Contribute a Pattern to the Library
  • All Cookbooks
    Find all the methodology you need in this comprehensive and vast collection. The UVM and Coverage Cookbooks contain dozens of informative, executable articles covering all aspects of UVM and Coverage.

    • UVM Cookbook

      • UVM Basics
      • Testbench Architecture
      • DUT-Testbench Connections
      • Configuring a Test Environment
      • Analysis Components & Techniques
      • End Of Test Mechanisms
      • Sequences
      • The UVM Messaging System
      • Other Stimulus Techniques
      • Register Abstraction Layer
      • Testbench Acceleration through Co-Emulation
      • Debug of SV and UVM
      • UVM Connect - SV-SystemC interoperability
      • UVM Versions and Compatibility
      • UVM Cookbook

    • Coding Guidelines & Deployment

      • Code Examples
      • UVM Verification Component
      • Package/Organization
      • Questa/Compiling UVM
      • SystemVerilog Guidelines
      • SystemVerilog Performance Guidelines
      • UVM Guidelines
      • UVM Performance Guidelines

    • Coverage Cookbook

      • Introduction
      • What is Coverage?
      • Kinds of Coverage
      • Specification to Testplan
      • Testplan to Functional Coverage
      • Bus Protocol Coverage
      • Block Level Coverage
      • Datapath Coverage
      • SoC Coverage Example
      • Requirements Writing Guidelines
      • Coverage Cookbook
  • All Events
    No one argues that the challenges of verification are growing exponentially. What is needed to meet these challenges are tools, methodologies and processes that can help you transform your verification environment. These recorded seminars from Verification Academy trainers and users provide examples for adoption of new technologies and how to evolve your verification process.

    • Upcoming & Featured Events

      • Debug with Codelink and Visualizer - December 8th
      • U2U MARLUG - January 26th
      • Events Calendar

    • On Demand Seminars

      • I'm Excited About Formal...My Journey From Skeptic To Believer
      • Interactive Debug Techniques
      • Formal-based ‘X’ Verification
      • 2020 Functional Verification Study
      • All On-Demand Seminars

    • Recording Archive

      • Improving Your SystemVerilog & UVM Skills
      • Should I Kill My Formal Run?
      • Visualizer Debug Environment
      • All Recordings

    • Mentor Training Center

      • SystemVerilog for Verification
      • SystemVerilog UVM
      • UVM Framework
      • Instructor-led Training

    • Mentor Learning Center

      • SystemVerilog Fundamentals
      • SystemVerilog UVM
      • Questa Simulation Coverage Acceleration Apps with inFact
      • View all Learning Paths
  • About Verification Academy
    The Verification Academy will provide you with a unique opportunity to develop an understanding of how to mature your organization's processes so that you can then reap the benefits that advanced functional verification offers.

    • Blog & News

      • Verification Horizons Blog
      • Academy News
      • Academy Newsletter
      • Technical Resources

    • Verification Horizons Publication

      • Verification Horizons - November 2020
      • Verification Horizons - July 2020
      • Verification Horizons - March 2020
      • Issue Archive

    • About Us

      • Verification Academy Overview
      • Subject Matter Experts
      • Contact Us

    • Training

      • Questa® & ModelSim®
      • Questa® inFact
      • Functional Verification Library
  • Home /
  • Patterns Library /
  • Specification Patterns

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 Verification Patterns—Taking Reuse to the Next Level our paper, Verification Patterns—Taking Reuse to the Next Level.

Occurrence Property Patterns:

  • Absence Property Pattern
  • Universality Property Pattern
  • Existence Property Pattern
  • Bounded Existence Property Pattern
  • Forbidden Sequence Property Pattern

Order Property Patterns:

  • Precedence Property Pattern
  • Response Property Pattern
  • Response Chain Property Pattern
  • Precedence Chain Property Pattern

 

Occurrence Property Patterns

  • Absence Property Pattern
  • Universality Property Pattern
  • Existence Property Pattern
  • Bounded Existence Property Pattern
  • Forbidden Sequence Property Pattern

Absence Property Pattern

Intent:

The Absence Property Pattern is used to specify portions of a design model’s verification execution where a specific state or event1 should never occur. Also known Never.

Motivation:

In the normal execution of an RTL state-based model, there are often specific events or states that should never occur. One of the most common examples of the Absence Property Pattern is mutual exclusion.

Applicability:

Any event that can be expressed as a proposition (e.g., Boolean equation), and describes undesirable behavior in a design, can be formulated into an absence property.

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

Universality Property Pattern

Intent:

The Universality Property Pattern is used to specify portions of a design model’s verification execution that contains states or events1 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 event1. 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 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.

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

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

Order Property Patterns

  • Precedence Property Pattern
  • Response Property Pattern
  • Response Chain Property Pattern
  • Precedence Chain Property Pattern

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,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.

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

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 events1), 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.

© Mentor, a Siemens Business, All rights reserved www.mentor.com

Footer Menu

  • Sitemap
  • Terms & Conditions
  • Verification Horizons Blog
  • LinkedIn Group
SiteLock