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
  • June 2019
  • Don’t Forget the Protocol! A CDC Protocol Methodology to Avoid Bugs in Silicon

Don’t Forget the Protocol! A CDC Protocol Methodology to Avoid Bugs in Silicon

Verification Horizons - Tom Fitzpatrick, Editor

Don’t Forget the Protocol! A CDC Protocol Methodology t o Avoid Bugs in Silicon Sukriti Bisht, Sulabh Kumar Khare, Ashish Hari, and Kurt Takara - Mentor, A Siemens Business

Clock-Domain Crossing (CDC) issues are the second most common reason for silicon re-spins. Most modern day designs have more than one clock, many of which are asynchronous. Signals that pass between logic clocked by different asynchronous clocks are called clock-domain crossing (CDC) signals. Due to the asynchronous nature of clocks, there is a possibility of CDC signals going metastable and propagating incorrect logic downstream resulting in functional failure of the design. To mitigate these problems, synchronizers are used on CDC paths.

Each synchronizer is dependent on a set of assumptions or protocols, which when violated can make the transfer unreliable. To avoid such issues, it is crucial to validate each synchronizer for its reliability. Engineers have been using assertion-based verification methods to verify synchronizer protocols in Formal and Simulation environments, but have fallen short of addressing the issue.

In this article, we will present the most prominent challenges faced with the existing methodology currently being used to verify synchronizer protocols and propose a new methodology to overcome them. Following are the key challenges:

  • Significant effort and time is required to setup the design before starting verification using Formal and Simulation. The setup also includes translation of design configurations and settings to both environments which requires technical expertise
  • Considerable debug effort required to review firings in Formal and Simulation
  • Missing correlation between protocol assertion checks in Formal, Simulation and associated CDC paths
  • Lack of re-utilization of benefits and efforts of both Formal, Simulation for faster design closure

The proposed methodology automates the progression of setup, constraint and results from CDC to Formal to Simulation. The methodology also addresses the important issue of correlating Formal and Simulation results to CDC results by using a new technique. In this technique, we add hooks to Formal and Simulation that enable us to extract important information and associate them to the CDC results. The proposed approach has also been automated for the seamless adoption of this methodology.

The article concludes with a demonstration of the proposed methodology on a set of real life designs. The demonstration proves that the methodology significantly reduces design and verification engineers’ effort and helps in achieving faster design closure.

INTRODUCTION

Most designs now-a-days have multiple asynchronous clocks. Logic clocked by each asynchronous clock forms the clock-domain for that clock. Signals that cross the boundaries of these clock-domains are called Clock-Domain Crossing (CDC) signals. Asynchronous nature of these CDC signals may cause setup or hold time violation of flip flops resulting in metastability. To ensure that these signals are properly synchronized, synchronizers are used. Synchronizers help protect the receiver domain from sampling metastable values and prevent data loss or corruption.

However, adding a synchronizer is just part of the solution. Despite the presence of synchronizers on CDC paths, there is still a possibility of data loss or corruption due to incorrect usage or interfacing of synchronizers. Reliability of every synchronizer depends on a set of assumptions or protocols. If the logic associated to the synchronizer does not interact as per the synchronizer’s protocol, the reliability of the synchronizer might break. For example data loss can occur if the input to a two DFF synchronizer is not stable for at least two clock cycles, or if the request and acknowledge signals in a handshake synchronizer do not occur in a particular order. The figure below illustrates these scenarios.

Figure 1 - Data loss in two DFF and Handshake synchronizers due to protocol violation


The issues of data loss or corruption due to synchronizer protocol violation must be identified and addressed early in the design cycle, otherwise they can lead to functional failures in later stages. These functional failures can further result in increased iterations and even silicon re-spins. To ensure such issues are not missed, designers and verification engineers verify synchronizer protocols. This Dynamic CDC Protocol Verification is done by extracting assertions for synchronizer protocols and verifying them using Formal and Simulation methods.

EXISTING DYNAMIC CDC PROTOCOL VERIFICATION METHODOLOGY

Figure 2 illustrates the existing approach for Dynamic CDC Protocol Verification. First step is to perform Static CDC analysis to ensure the presence of synchronizing logic on CDC paths. Post this step, assertions for synchronizer protocols are extracted based on CDC results. These assertions are then verified to ensure that the synchronizers present in the design are reliable.

Figure 2 - Existing methodology flowchart


To verify these protocol assertions, Simulation and/or Formal tools are used. The setup for each of these tools is different and has to be done manually, which increases the verification time and effort. Once the setup is complete, engineers perform protocol assertion verification using the Formal, Simulation tools and their results are debugged separately. While this methodology promises to identify CDC protocol bugs, it suffers from many issues such as substantial effort required for setup and debug, lack of correlation with CDC results, among others.

CHALLENGES FACED WITH EXISTING METHODOLOGY

In the existing methodology, engineers use Simulation and Formal methods separately to generate and verify assertions for synchronizer protocols. However, the methodology entails the following common challenges:

  • Setup: Significant effort and time is required to set up the design for Formal and Simulation runs. Design constraints and directives that were already specified in the CDC step, need to be translated and propagated to both the Formal and Simulation tools separately. For example, constant values, clock frequencies of design and so on. Issues at this step can result in unexpected design behavior in dynamic environment. Figure 3 shows an example where constant specified on input signal at the time of Static CDC was not propagated to Formal setup resulting in false two DFF protocol firing.

  • Figure 3 - False two DFF firing in Formal due to constants missing in setup


  • Debug: Analyzing and debugging Formal and Simulation results requires expert knowledge about both the environments. Issues in setup or inaccurate assertions can result in large number of false firings, which further increase the problem. For example, incorrect clock frequency or domain specified on ports can result in unexpected behavior. Figure 4 shows an example of a false two DFF stability check firing in Formal where unspecified clock frequency in Formal setup resulted in clock incorrectly changing as per fastest clock’s frequency.

  • Figure 4 - False 2DFF Formal firing due to unspecified clock frequency


  • Correlation to CDC: The existing methodology suffers from lack of relation between CDC, Formal and Simulation results. The debug environments of Formal and Simulation are very different from CDC. Hence, establishing a relation between CDC, Formal and Simulation results for the purpose of coverage and review of CDC paths is cumbersome and time consuming. For example, complex synchronizers such as FIFO or handshake have multiple assertions that are treated as separate entities by both Formal and Simulation, but relate back to a single CDC path. Issues or errors during correlating results can lead to missed bugs. Figure 5 shows various handshake synchronizer protocol assertions that relate back to the same crossing. If not correlated properly, some uncovered or fired assertions may be missed resulting in data loss or corruption in the design.

  • Figure 5 - Multiple handshake protocol assertions


  • Lack of effort re-utilization: Due to limitations of both Formal and Simulation methods, to save time and to ensure sufficient coverage, verification engineers may have to change from one method to another, or adopt both simultaneously. In such scenarios, the challenge faced is in terms of redundancy and lack of verification effort re-utilization. For example, if Formal step is followed by Simulation step, assertions that were already proven by Formal will have to be re-verified in Simulation.

Apart from these common challenges, both Formal and Simulation methods have their own advantages and disadvantages. While Simulation is more intuitive to understand, it runs into coverage issues. Bugs can go undetected if the quality of testbench is not good. On the other hand, Formal offers exhaustive proofs but runs into infrastructural and capacity issues.

For a design of considerable size, covering all scenarios in Simulation can take infinite amount of time, which may lead to missed deadlines. On the other hand, obtaining conclusive proofs for an entire design in Formal may require infinite memory due to state space explosion problem, resulting in increased cost.

PROPOSED METHODOLOGY FOR DYNAMIC CDC PROTOCOL VERIFICATION

In this article, we propose a methodology that not only helps overcome the common challenges of Formal and Simulation verification, but also utilizes the advantages and efforts of both the methods. Figure 6 illustrates the proposed methodology.

Figure 6 - Proposed methodology flowchart


With this methodology, we propose the automated propagation of setup from CDC to Formal and Simulation tools to help reduce the time and manual effort required in setting the design. This propagated setup includes design settings like clocks, resets, constants, port clock-domains, amongst others that are easily available at the CDC step. This automation ensures easy and correct propagation of setup without the hurdles of technical expertise required on the engineer’s part to setup each tool’s environment.

The protocol assertion generation step inserts hooks into Formal and Simulation to get insights into the status of each assertion. These insights help to correlate the Formal and Simulation results back to the associated CDC paths. This helps ensure that design and verification engineers can view the dynamic verification status of each CDC path.

The methodology aims to not only save but also re-utilize designer and verification engineer’s effort for faster design closure. Ensuring automated propagation of setup and barring the propagation of Formal proven assertions to Simulation helps in achieving the objective.

The proposed methodology has the following workflow:

  1. Static CDC Analysis: Perform static CDC analysis on the design to ensure that all the relevant CDC paths are synchronized using proper synchronizers.
  2. Protocol Assertion Generation: Generate assertions for protocols of synchronizers present in the design. Based on static CDC analysis, each synchronizer on a CDC path is analyzed and protocol assertions are generated depending upon the type of synchronizer and its connections. Simultaneously, the design settings and configurations passed to the CDC step are translated to Formal and Simulation language, generating the required setup for running both environments. This step also includes inserting hooks in both environments, which helps in correlating Formal and Simulation results back to the CDC environment.
  3. Formal Analysis: Verify the generated synchronizer protocol assertions in Formal environment using the setup generated. The automated setup reduces significant effort required to setup the design and also avoids the possibility of false firings due to incomplete or incorrect setup.
  4. Formal Debug: Debug the assertion firings generated by Formal tool by analyzing the counter example. Design constraints, if any, can be added to eliminate false scenarios and the design can be re-run incrementally with the added constraints.
  5. Simulation: Run Simulation on the design using the auto-generated setup to verify the protocol assertions that are non-proven by the Formal tool. After Formal analysis, the Simulation setup is updated incrementally to ensure only non-proven assertions are promoted to Simulation environment. This helps ensure that the effort put in to get conclusive results in Formal is re-utilized resulting in faster design closure.
  6. Review CDCs: Review the combined results of Formal and Simulation along with CDC results. The hooks inserted in Formal and Simulation are used to extract status of various protocol assertions associated to a crossing and correlate them back to CDC environment. This helps in ensuring that bugs are not missed and protocols for synchronizers on CDC paths are not violated. Figure 7 shows the view of a combined result set along with the related CDC paths, for a unit design.

  7. Figure 7 - Formal, Simulation result correlation to CDC paths


CASE STUDY

Both existing and proposed methodologies were compared by using them for Dynamic CDC Protocol Verification of real life designs. The comparisons were performed on a set of real life designs, ranging from 1 to 30 million gates. The setup time required and results obtained with both the methodologies were recorded and analyzed.

A. Static CDC Analysis, Protocol Assertion Generation

The designs first underwent Static CDC analysis to ensure the presence of synchronizers on all relevant CDC paths. Post Static CDC analysis, assertions for synchronizer protocols were generated and verified in Dynamic environment as per each methodology.

B. Formal Verification

In the existing methodology, the protocol assertions were validated first in a Formal environment. The design settings and constraints like clocks, resets, constants, and so on were translated from Static CDC environment and re-specified in the Formal tool’s language manually. This required significant effort and expertise. Once the Formal tool environment setup was complete, the design was verified formally and the assertion firings were debugged.

Similarly, in the proposed methodology, the first step was protocol assertion verification in Formal environment. The design configurations and constraints for Formal were auto-generated by using the proposed methodology. This auto-generated setup was reviewed and used to verify design formally. The setup automation saved a lot of manual effort and expertise that was earlier required to port the setup from CDC to Formal.

C. Simulation

Post Formal verification, the engineer decided to take the Simulation path. With the existing methodology, protocol assertions that were proven formally were re-verified in Simulation environment. The design, testbench were compiled and setup for Simulation. On completion of Simulation, the results were analyzed and firings were debugged.

In the proposed methodology, only the assertions that were non-proven in the Formal environment, were verified in Simulation. The auto-generated set-up along with testbench, was used to run Simulation. This was followed by debugging the Simulation firings. Significant reduction in debug effort and time was observed due to running Simulation only for Formal non-proven assertions.

Tables 1 and 2 summarize the comparison between existing and proposed methodology performed on a set of real life designs, ranging from 1 to 30 million gates. Significant reduction in Formal setup time was observed. Setup time for Simulation was also reduced. Firings in Formal also reduced for each design due to reduction in false firings caused by setup issues. Assertions passed to Simulation step also reduced due to exclusion of Formal proven assertions thereby reducing the verification effort required.

Table 1 - Results using existing methodology

Table 2 - Results using recommended methodology

* Formal Coverage = ((Failed Assertions + Proven Assertions) / Total Assertions) * 100

** Simulation tool coverage = Coverage metric of Simulation tool = ((Failed Assertions + Covered non-failed Assertions) / Total Assertions) * 100

CONCLUSION

The proposed methodology significantly reduces the time and effort required for Dynamic CDC Protocol Verification closure of designs. Not only does this approach help design and verification engineers overcome the challenges faced during Formal and Simulation verification but also enable them to reap the benefits of both the methods. The methodology is seamless to adopt and saves both time and effort to achieve faster closure.

REFERENCES

[1] Mark Litterick, “Pragmatic Simulation-Based Verification of Clock Domain Crossing Signals and Jitter using System Verilog Assertions”, Verilab
[2] William K. Lam, “Hardware Design Verification: Simulation and Formal Method-Based Approaches”, Prentice Hall, Mar 3, 2005
[3] Sulabh K. Khare, Ashish Hari, “Systematic Speedup Techniques for Functional CDC Verification Closure”, Mentor Graphics, advanced verification white paper
[4] Ping Yeung, “Five Steps to Quality CDC Verification,” Mentor Graphics, advanced verification white paper

Back to Top

Table of Contents

Verification Horizons Articles:

  • Is Your Verification in Jeopardy?

  • SystemC FMU for Verification of Advanced Driver Assistance Systems

  • Fun with UVM Sequences - Coding and Debugging

  • Creating Tests the PSS Way in SystemVerilog

  • Formal Bug Hunting with “River Fishing” Techniques

  • Don’t Forget the Protocol! A CDC Protocol Methodology to Avoid Bugs in Silicon

  • Auto-Generating Implementation-Level Sequences for PSS

  • UVMF, Beyond the ALU Generator Tutorial Extending Actual Test Control of the DUT Inputs

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