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

      • Low Power Verification - 4/29
      • Fault Campaign for Mixed-Signal - 5/4
      • User2User - 5/26
      • Webinar Calendar
    • On-Demand Webinars

      • CDC+RDC Analysis
      • Basic Abstraction Techniques
      • Safety Analysis Techniques
      • QVIP Workflow and Debug for PCIe
      • Writing a Proxy-driven Testbench
      • Achieving High Defect Coverage
      • Visualizer Features
      • All On-Demand Webinars
    • Recording Archive

      • Siemens EDA 2021 Functional Verification Webinar Series
      • Improving Your SystemVerilog & UVM Skills
      • Should I Kill My Formal Run?
      • Visualizer Debug Environment
      • Industry Data & Surveys
      • All Recordings
    • Conferences

      • DVCon 2021
      • DVCon 2020
      • DAC 2019
      • All Conferences
    • Mentor Learning Center

      • SystemVerilog Fundamentals
      • SystemVerilog UVM
      • 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 - March 2021
      • Verification Horizons - November 2020
      • Verification Horizons - July 2020
      • Issue Archive
    • About Us

      • Verification Academy Overview
      • Subject Matter Experts
      • Contact Us
    • Training

      • Questa Basic
      • Questa Advanced
      • Mastering Questa
  • Home
  • Verification Horizons
  • October 2012
  • The Top Five Formal Verification Applications

The Top Five Formal Verification Applications

Verification Horizons - Tom Fitzpatrick, Editor

The Top Five Formal Verification Applications by Roger Sabbagh, Mentor Graphics

It's no secret. Silicon development teams are increasingly adopting formal verification to complement their verification flow in key areas. Formal verification statically analyzes a design's behavior with respect to a given set of properties. Traditional formal verification comes in the form of model checking which requires hand-coded properties, along with design constraints. While there certainly are some design groups who continue to be successful with that approach, what are getting more widespread adoption in the industry are the automatic approaches which require much less manual setup. Let's take a look at the top five applications being used across the industry today.

#5. CONNECTIVITY CHECKING

Today's SoC designs contain large numbers of design IP blocks, interconnected through multiple on-chip bus fabrics and point-to-point connections which can number in the thousands. The designs also have multiple modes of operation which may affect the connectivity and also the activation of the design logic. SoCs are typically pin-constrained and have multi-function I/O pins that are conditionally multiplexed to support the high number of system functions integrated within the device. There are multiple types of connections that must be validated, including, but not limited to:

  • Point-to-point connections at the same level of hierarchy
  • Point-to-point connections through multiple levels of hierarchy
  • Conditional point-to-point connections
  • Point-to-point connections with sequential delay

Then there are combinations of the above, such as conditional point-to-point with sequential delay. You can see where this is going. Using dynamic simulation to validate design assemblies is not very efficient. It typically involves the time consuming task of developing directed tests to toggle all the top level design signals, not to mention the tedious debugging process to determine why signal values did not transition or propagate as expected.

On the other hand, formal tools can be employed to automatically highlight the areas where the expected connectivity behavior doesn't hold true and they provide a much faster route to debug of any problems. A complete property set describing the interconnections in the SoC can be automatically extracted from a specification that details the design assembly requirements, which in most cases is already pre-existing, minimizing the effort required.

#4. X-STATE VERIFICATION

Fundamental differences exist in the way an X-state is interpreted in RTL simulation versus how it is treated by synthesis. The synthesis interpretation of X as don't care can result in silicon that behaves differently than observed in RTL simulation, where X is interpreted as unknown. The unknown RTL simulation semantics of X has two oft discussed pitfalls: x-pessimism and x-optimism. Of these two issues, the latter one is the most worrisome as it can mask true design behavior by blocking the propagation of X-states and instead propagating a deterministic value through the design, when in reality various possible values will be seen in silicon. If the unexplored values cause the physical design to malfunction, then x-optimism has resulted in a silicon bug. Simply eliminating all X-states from RTL simulation is not practical. Due to power and area constraints, not all storage elements in a large design can be reset directly; some will be reset indirectly by loading values computed from other registers that have been reset. Hence, X-states are expected to exist in the design during the initialization phase. Moreover, X-states can arise in RTL simulation due to a number of other events, such as:

  1. Activation of an explicit X-state assignment that was intended as a synthesis don't care and was never expected to be exercised
  2. Bus driver value conflicts
  3. Out of range indexing into an array
  4. Arithmetic exceptions

It's important, therefore, to verify that:

  1. All storage elements which should be initialized (either directly or indirectly) have reached a known good state after the initialization sequence, and,
  2. Storage elements which were initialized correctly are not later contaminated by the unknown values in uninitialized state elements or those which have arisen due to other X-state generating events.

The benefits of a formal approach are two-fold. First, formal can automatically pinpoint the sources of X-states in the design. Through static analysis of design behavior, formal can highlight occurrences of X-states that may have otherwise been masked by X-optimism in RTL simulation.

Second, it can exhaustively and deterministically evaluate all possible design behaviors to determine if X-states can be propagated to corrupt known values. Properties to check for X-state propagation to storage elements or design outputs can be generated automatically, making the setup effort for this process very minimal.

#3. CODE COVERAGE CLOSURE

Code coverage is a metric used by the majority of today's project teams with the goal of providing a clear, quantitative, objective measure for assessing their progress towards completeness. One of the big advantages of code coverage is that it is measured automatically. The designers do not have to instrument their code with coverage collectors, as they are automatically generated in simulation. So, coverage results can be obtained with low effort, but, interpreting those results and achieving closure is a lengthy process that involves a lot of manual intervention. Typically, ›90% of coverage items in a design are covered in a full regression, but it's the process of analyzing that last ~10% which is problematic. Each uncovered point in the code must be reviewed to determine if it is safe to ignore or if the test environment must be enhanced to cover it, typically through writing directed tests.

Due to design reuse, not all IP block modes or functions are expected to be covered. In addition certain coding styles lead to branches of code that are never expected to be traversed. What if a tool could analyze the code under expected operating modes and prune out the unreachable coverage bins? Enter formal verification. Formal analysis can find and report these unreachable goals and improve the accuracy of the code coverage metrics. In addition it can demonstrate how to hit the reachable ones, and in doing, provide a guide for the process of generating additional tests to cover them in simulation. As with simulation, formal infers the coverage targets automatically from the code, so there is very little effort required to set up the tool.

#2. AUTOMATIC FORMAL

Getting back to the concept of model checking mentioned earlier – what if the properties for commonly occurring RTL functions could be automatically generated? That would certainly make it easier to use. Well, that's precisely what automatic formal tools do. They automatically generate
properties for RTL elements such as registers, FSMs and memories. Then, they find a variety of issues such as FSM deadlock, counter overflow and out of range memory addressing.

Automatic formal tools require little to no set up and can bring a lot of value by eliminating design bugs before getting the design running in simulation. Simulation debug can be very costly in terms of time and engineering resources. By
filtering out a whole class of bugs that can be found through automatic formal analysis before simulation, much time can be saved.

#1. CLOCK-DOMAIN CROSSING VERIFICATION

One of the by-products of the high levels of integration associated with today's complex designs is an ever increasing number of asynchronous clocks and a burgeoning number of CDC signals. It is not uncommon to find designs with hundreds of asynchronous clocks and tens of thousands of CDC signals. Unique functional clocking requirements are introduced by virtually each new added external interface or internal functional block. Also, physical design limitations on the size of balanced clock tree and power reduction techniques introduce additional asynchronous domains. As data moves through the device to and from interface controllers and between functional blocks, it must be safely transferred across the clock domain boundaries. RTL simulation does not model the silicon behavior of asynchronous clock crossings, so CDC signals have to be verified through alternate methods.

CDC verification has thus become a critical step in the design process and most design teams have adopted automated CDC verification tools to address this requirement. Automated CDC tools make it easy to use static analysis to perform comprehensive CDC verification. They find all the clock domains and clock domain crossing signals and check for correct synchronization of those signals. The most commonly used synchronization schemes are recognized by the tools in an attempt to report only true metastability issues due to missing synchronizers. They also alert the designer to occurrences of common structural synchronization issues with the existing synchronizers, such as glitch generating combinational logic that drives a synchronizer input. Finally, they also report more complex CDC issues such as redundant synchronization and divergence/reconvergence of synchronizer signals.

Very commonly, there are many IP block design teams that contribute to the chip-level design. For the chip team to review and resolve all the block level CDC issues from the various IP blocks would be very time consuming and impractical. Hence, a partitioned approach to top level CDC verification is often employed. With a partitioned methodology, CDC analysis is performed piece-wise, in a bottom-up fashion. The design team that owns each IP block is tasked with running CDC analysis on their logic, refining the constraints, fixing any CDC issues internal to the block and creating the waivers. The tools also generate abstract, block-level CDC models for use at the top level. This takes the intra-block CDC path verification off the table for the chip level integration team, allowing them to focus strictly on the inter-block asynchronous signals.

Due to their automated nature CDC tools are easy to use. They also accept SDC timing constraints to define the relationship between clocks and the clock domain of I/O ports, making it even easier to get results.

That completes our top 5 list of formal verification applications in use in the industry today. In future articles, we will explore each of these methods further, including some results from their application on real world designs.

Back to Top

Table of Contents

Verification Horizons Articles:

  • There's Productivity. And Then There's Productivity

  • ST-Ericsson Speeds Time to Functional Verification Closure with Questa Verification Platform

  • The Top Five Formal Verification Applications

  • Three Steps to Unified SoC Design and Verification

  • Evolution of UPF: Getting Better All the Time

  • Improving Analog/Mixed-Signal Verification Productivity

  • VHDL-2008: Why It Matters

Siemens Digital Industries Software

Siemens Digital Industries Software

##TodayMeetsTomorrow

Solutions

  • Cloud
  • Mendix
  • Siemens EDA
  • MindSphere
  • Siemens PLM
  • View all portfolio

Explore

  • Digital Journeys
  • Community
  • Blog
  • Online Store

Siemens

  • About Us
  • Careers
  • Events
  • News and Press
  • Newsletter
  • Customer Stories

Contact Us

USA:

phone-office +1 800 547 3000

See our Worldwide Directory

  • Contact Us
  • Support Center
  • Give us Feedback
©2021 Siemens Digital Industries Software. All Rights Reserved.
Terms of Use Privacy Cookie Policy