Vaishnav Gorur, Sr. Applications Engineer
Prior to joining Real Intent, Vaishnav was a logic design engineer at MIPS Technologies where he was responsible for the microarchitecture and RTL Design of the Load-Store Unit and Graduation Unit of the 15-stage out-of-order asymmetric dual-issue superscalar pipeline in the MIPS32® 74K® fully … More »
Lending a ‘Formal’ Hand to CDC Verification: A Case Study of Non-Intuitive Failure Signatures — Part 1
June 13th, 2013 by Vaishnav Gorur, Sr. Applications Engineer
In Austin, at the 50th DAC earlier this month, I delivered a poster presentation on “Lending a ‘Formal’ Hand to CDC Verification: A Case Study of Non-Intuitive Failure Signatures”. In this first blog in a series, I will set the stage for the issues around the case study of failures in a common clock domain crossing synchronizer.
At DAC 2012 last year, we surveyed more than 300 participants to understand trends in the CDC verification space. More than half had a new design project starting within 3 months, which indicates reduced design cycles. Almost 1/3rd had over 50 clock domains in their design. Extrapolating from our DAC 2011 survey, we see a definite trend of increasing CDC complexity. Almost 2/3rd had to incur the penalty of an ECO due to a CDC bug.
For the reasons above, CDC Analysis tools topped their shopping list.
As CDC verification is becoming mainstream, it is imperative to refine and fine tune the CDC flow to balance the verification effort. As indicated by the pie-chart on the bottom-right, ‘Automatic Formal’ is another technology that the industry is looking to leverage. In this presentation, we show how the application of formal analysis in the CDC space can be used by design engineers to verify their CDC constructs and how this can alleviate the CDC verification challenge from the shoulders of verification engineers.
Whenever a signal changes too close to the clock edge it is being sampled on, the captured value is non-deterministic due to setup/hold violations. This phenomenon is called Metastability and without proper prevention and verification, metastability propagation could cause serious design errors. For synchronous designs, this is not a major issue as Static Timing Analysis (STA) tools can flag these issues with setup/hold checks.
However, metastability is an unavoidable issue for signals crossing asynchronous clock domains as clock domain crossings are not timed by STA tools. Due to the asynchronous nature of the transmit and receive clocks, it is possible that the transmit data might change within the setup and hold window of the receive clock, hence resulting in an unpredictable value and delay at the output of the flop.
To avoid the pitfalls of Metastability, designers use certain synchronization schemes to ensure correct exchange of information between asynchronous clock domains. One such common scheme is depicted below, where a synchronized control signal is used to enable the loading of the data being sent from the transmitting domain to the receiving domain.
A ‘control’ signal is one that is synchronized directly by a multi-flop synchronizer. A ‘data’ signal is one that is not directly synchronized but whose synchronization is controlled by a corresponding ‘control’ signal.
The conditions that need to be met by the control and data signals in such a scheme are outlined below. The two conditions highlighted in Green are candidates for formal analysis to verify. These two conditions are the focus of this presentation and are described later on.
Design flows that do not currently leverage a dedicated CDC verification tool attempt to fill in the gap by using custom scripts wrapped around STA tools and custom gate-level simulation environments. Typically, these are cumbersome to maintain and are not scalable.
Due to the adoption of the above approaches, the CDC problem has traditionally been deemed a back-end issue and left to the verification and CAD engineers to tackle. This often leads to lengthy verification and debug iterations due to incomplete understanding of the CDC nuances of the design. Additionally, CDC verification done later in the flow translates to a longer delay waiting for the design fix to be rerun through all the earlier stages in the flow.
Our recommendation is to move CDC verification to the design team and adopt a flow involving automatic formal CDC technology. By being automatic and not requiring the developement of a testbench or specification of assertions, automatic formal technologies preclude the traditional verification maxim that a designer should not verify his/her own block. At the same time, it leverages the fact that a designer understands the CDC constructs in the design and can quickly comprehend a failure signature and make an appropriate design fix. This shortens the CDC verification cycle and results in higher quality RTL handoffs to downstream teams.
In the next blog, I will discuss a case study involving non-intuitive failure signatures to support this recommendation.