Get CDC protocols right with an automated formal-to-simulation flow

Today’s designs are often replete with asynchronous clocks. The signals crossing between these clock domains are prone to functional errors such as metastable events, corrupted data, and lost data.

These clock-domain crossing (CDC) issues are the second most common reason for silicon respins. In an effort to prevent these errors and the propagation of metastable events, designers insert synchronizers on CDC paths, making already complex designs even more complex and verification more complicated. If a CDC synchronizer is not used correctly, the CDC path may experience data loss, data corruption, or, in the worst case, metastability. The rules that define the correct usage of a CDC synchronizer are called CDC protocols.

A serious problem exists when designers overlook the fact that a good structure alone is not sufficient to avoid CDC errors. As a result of this misapprehension, designers often do not implement or verify the correct CDC protocol. Yet, when the set of assumptions or protocols that a synchronizer is dependent upon are violated, the transfer of data can become unreliable.

In an attempt to verify synchronizer protocols, engineers have generated assertions for synchronizer protocols and verified them using formal model checking and simulation techniques. However, project teams often do not utilize this approach to protocol verification due to a multitude of deployment challenges. Three of the most common are:

1. The significant effort and time required to set up the design and assertions for formal and simulation.
2. A lack of integration across the structural analysis, formal verification, and simulation steps.
3. The considerable effort required to review and debug firings in formal and simulation.

Fortunately, there is a more efficacious way: an automated methodology that resolves the shortfalls found in these current CDC protocol verification efforts. Automation reduces the time and errors of manual scripting and set-up. In addition this approach improves debug productivity by correlating structural analysis, formal verification, and simulation results.

This systematic and repeatable CDC protocol verification solution improves the accuracy of formal analysis and reduces false formal firings, and it establishes an easier to use debug environment that allows you to debug and fix protocol errors more quickly and with less effort.

Four-step automated clock-domain crossing protocol verification

Engineers need a way that helps them overcome the challenges of traditional protocol verification methods by leveraging formal model-checking and simulation technologies to improve protocol verification results. The workflow for this automated CDC methodology consists of four steps: static CDC analysis, formal analysis, simulation, and the review and debug of results.

Figure 1. Clock domain crossing protocol verification workflow (Mentor)

1. Static clock-domain crossing analysis

Static CDC analysis is performed on a design to ensure that all the relevant CDC paths are synchronized using proper synchronizers. In addition, during static CDC analysis protocol assertions, formal verification constraints and the set ups for formal verification and simulation are automatically generated.

Based on static CDC analysis, the CDC protocol generation utility automatically generates protocol assertions for each CDC synchronizer. The protocol assertions are generated depending upon the type of synchronizer and its connections (Figure 2).

Figure 2. CDC protocol assertion instantiation (Mentor)

The CDC protocol generation utility converts the CDC information for constant, stable, gray-code signals into SVA assumptions for formal verification. In addition, input and output port clock domain information is converted into formal constraints to improve the accuracy of formal counter-examples.

The CDC protocol generation utility generates formal model checking run scripts. The utility also generates a simulation arguments file to be added to the existing simulation environment, so designers can easily add protocol assertions and avoid manually adding multiple assertion and bind module files to their simulation.

2. Formal analysis

In this step we run formal model checking to verify the auto-generated synchronizer protocol assertions, using the generated formal verification set up and script. The CDC protocol generation utility generates the formal compile and run scripts. Automated formal set-up significantly reduces the effort required to set up the design for formal analysis and also avoids the debug effort to resolve incomplete or incorrect setup issues. In order to run formal analysis, designers simply execute the makefile (i.e., “make all”).

3. Simulation

Next we run simulation by adding the auto-generated setup to the existing simulation environment in order to verify the non-proven protocol assertions. The CDC protocol generation utility generates simulation arguments files for compilation and simulation.

During the formal analysis, the formal analysis script automatically updates the simulation set-up to remove the proven assertions from the list of assertions for simulation. A formal proof for any protocol assertion indicates that the protocol can never be violated for the associated CDC synchronization structure. This proof indicates that the synchronization structure is safe from data loss, data corruption, and the propagation of metastability. Removing the proven assertions from simulation reduces the simulation runtime and reduces the effort of reviewing simulation results for proven assertions that cannot be violated in simulation.

4. Review and debug clock-domain crossing protocol results

Finally, we review the aggregated structural CDC analysis, formal verification, and simulation results. The correlation between the multiple technologies (static CDC analysis, formal model checking, and simulation) allows designers to more quickly and easily debug and resolve protocol errors. Through this correlation, designers can find the CDC structure associated with a protocol failure, then quickly diagnose the cause of the protocol error. This improved review and debug ensures that bugs are correctly analyzed and protocols errors for CDC synchronizers are not missed or incorrectly analyzed.

Real-world comparisons

This CDC protocol verification methodology has been tested on real-world designs. We also compared its efficacy against the existing methodology.

First, using the traditional protocol verification methodology, the protocol assertions were validated in a formal verification environment. The design settings and constraints — like clocks, resets, constants, and input port constraints — were manually translated from the static CDC environment and re-specified as formal constraints. This constraints translation required significant manual effort and formal expertise. Once the formal tool environment set up was complete, the design was verified formally and the assertion firing counter-examples were debugged.

Similarly, in our new methodology, the first step was protocol assertion verification in a formal verification environment. The design configurations and constraints for formal analysis were auto-generated. This auto-generated setup was reviewed, then used to run formal analysis on the design and assertions. The setup automation avoided the manual set up effort and eliminated the need for the formal expertise that would be required by a traditional approach to port the setup from CDC to formal.

Formal verification results included proofs, firings, and inconclusives for CDC protocol assertions. The auto-generated formal setup did not include a complete set of design constraints, so the firings produced unconstrained formal assertion violations that are, in most cases, counter-examples with illegal stimulus sets. For designers without formal model checking expertise, it is difficult to debug and/or resolve fired and inconclusive assertions, so instead of debugging these difficult cases, designers promote these assertions to simulation.

With the traditional methodologies, proven protocol assertions are re-verified in a simulation environment or must be manually removed from the simulation setup. In our methodology, only non-proven assertions from formal analysis are verified in simulation. The proven assertions are automatically removed from the simulation setup. The auto-generated simulation arguments file is added to the existing simulation environment. Any simulation assertion firings indicate a violation of the CDC synchronizer protocol that would result in data loss, data corruption, or metastability propagation on the associated CDC path. Designers must debug simulation firings and fix the CDC logic to adhere to the synchronizer protocol rules. Significant reduction in debug effort and time was observed due to running simulation only for formally non-proven assertions.

Tables 1 and 2 summarize the comparison between the traditional and new methodologies performed on a set of real life designs, ranging from 1 to 30 million gates.

Table 1. Results using traditional protocol verification methodology (Mentor)

Table 2. Results using new protocol verification methodology (Mentor)

The improvements delivered by this new, automated CDC protocol verification methodology can be summarized as follows:

• There was a significant reduction in formal set-up time. The set-up time was reduced due to the automated set-up generation. In addition to the reduction in set-up time, the set-up debug effort was reduced by avoiding the incremental debug iterations of incomplete and incorrect setups. The set-up time was reduced by 3x-5x.
• There was a reduction in set-up time for simulation. The set-up time was reduced due to the automated set-up generation. In addition to the reduction in set-up time, the set-up debug effort was reduced by avoiding the incremental debug iterations of incomplete and incorrect setups. For design C, the set-up time was reduced by 6x-17x.
• There was a reduction in false firings in formal analysis. The automated set-up generation and the import of CDC design constraints into formal analysis reduced the formal set-up errors and caused a reduction in false firings. The formal assertion firings were reduced by 59%-68%.
• There was an increase in formal coverage. The improved formal set-up and constraints resulted in less inconclusive assertions and more proofs and firings.
• There was an increase in simulation coverage. Removing proven assertions from simulation resulted in a higher percentage of fired and covered simulation assertions. Since the proven assertions were not simulated in the proposed methodology, the proven assertions were considered covered in order to maintain simulation coverage consistency between the traditional and new methodologies.
• There was a reduction in simulation verification time and effort. There was a reduction in the number of assertions passed to simulation due to exclusion of formally proven assertions, thereby reducing the verification effort required for reviewing proven assertions in simulation. The correlation of structural CDC analysis, formal verification, and simulation results improved debug productivity and led to easier association of protocol errors with their associated CDC paths. The time and effort for reviewing and debugging simulation results was not measured for these design case studies.
• There was a minimal change in simulation runtime. The reduction in the number of assertions run in simulation due to exclusion of formally proven assertions did not significantly change the simulation runtime.

This demonstration on real-world designs proves that our new methodology significantly reduces design and verification effort and helps achieve faster design closure.

For more information on verifying clock-domain crossing protocols, also check out this webinar: “What Is CDC Protocol Verification, and Why You Absolutely Need It To Prevent Bugs in Your Silicon”.

About the authors

Sulabh Kumar Khare is an engineering manager who oversees the development of the clock-domain crossing product line at Mentor, a Siemens Business. Sulabh has over 13 years of experience in developing EDA software for the design and verification domain. He holds a Masters degree in VLSI design from IIT Kharagpur.

Kurt Takara has over 20 years of experience in engineering design and verification, technical marketing and engineering services. Kurt is a Product Engineer at Mentor and specializes in assertion-based verification methods and applications, including formal and clock-domain crossing (CDC) verification. He holds a BSEE from Purdue University and an MBA from Santa Clara University.