Open side-bar Menu
 Real Talk
Dr. Roger B. Hughes, Director of Strategic Accounts
Dr. Roger B. Hughes, Director of Strategic Accounts
Dr. Roger B. Hughes is a renowned international expert in formal verification technologies and has over 20 years experience in the EDA industry working both at start-up companies in lead engineering roles and publicly traded companies in managing and directing technical product development. He … More »

CDC Verification of Fast-to-Slow Clocks – Part 2: Formal Checks

January 21st, 2016 by Dr. Roger B. Hughes, Director of Strategic Accounts

We continue the short blog series that addresses the issue of doing clock domain crossing analysis where the clocks differ in frequency. In Part 1, we ended the discussion noting that when there is a fast-to-slow transition, there is a possibility that a short duration control pulse may be completely missed by the receive domain and a formal analysis is required to discover if this is a potential problem. We will look at how formal analysis can verify this kind of transition.

A formal check also is required on a slow-to-fast data crossing with feedback. In such a circuit, as shown in Figure 4, an acknowledge signal coming from the receiving fast-clock domain to the transmitting slow-clock domain also requires a formal Pulse Width check. Although the control pulse (request) is going from slow to fast and does not need a formal pulse width check, the acknowledge pulse-width check is necessary because the acknowledge signal (the feedback circuit) is going from a fast to a slow clock and, in order for the acknowledge to be properly captured, the acknowledge pulse (transmitted from the receiving side) must be sufficiently wide to be captured (received on the transmitting side) by the slower clock domain of the transmitting side flops. Failure to check for this condition is the reason behind many a request/acknowledge circuit not working as expected. Note that feedback circuits in a fast-to-slow crossing are operating in a slow-to-fast mode and the acknowledge signal in such a circuit does not need to be pulse-width checked. In short, all fast-to-slow control signal transitions, whether connected in a feed-forward or a feedback manner need to be formally pulse-width checked to ensure integrity of the control aspect of the clock domain crossing.

Figure 4 – Slow-to-Fast Clock Crossing with Feedback (red flops are slow clock, blue flops are fast clock).

To check if the fast-to-slow clock domain crossings have control signals that can be captured by the receive domain clock, Meridian CDC offers formal analysis capability targeted at the asynchronous clock domain crossings of interest. There is a requirement that the control pulse in the fast transmit domain must be of a certain minimum width in order to be captured by the slower receive domain clock. Figure 5 shows that TX CNTL must be held high for several clock periods of Clk1 for the TX domain flop value to be captured by the RX domain Sync1 flop and then passed into RX domain Sync2 flop. A formal check called PULSE_WIDTH verifies that the transmit domain’s control pulse has sufficient length to be captured by the receive domain’s clock in all circumstances. This check examines all the pulse generation logic and takes into consideration the clock frequency ratio during detailed formal analysis to determine pass or fail. If there is a case in which the pulse length is insufficient, a counter example is generated to show the circumstances in which this would occur. If PULSE_WIDTH passes, the crossing shown always has correct control pulse duration to ensure there will not be a missed control pulse.

Figure 5 – Fast-to-slow clock domain crossing with sufficient pulse length. Here the TX CNTL pulse is held high for a sufficient number of TX Clk1 periods so that an edge of RX Clk2 is able to sample the value on the TX CNTL flop into the RX CNTL Sync1 flop, which then can pass the value to RX CNTL Sync2. This can be formally proven using the PULSE_WIDTH check of Meridian CDC.

There also needs to be a check on the data path. There is a possibility that if the data is not held stable for a long enough period, it might get missed in the receive domain. For example, suppose the transmit domain has the data sequence <D0><D1><D2><D3>, etc. This sequence of data changes is shown in Figure 5. If the data changes before the control signal has been passed to the receive domain, it is possible that the receive domain might miss some data and end up with <D0><D1><D3>… if <D2> was not correctly transmitted to the receive domain. An additional formal check in Meridian CDC called DATA_STABILITY ensures that the data transitions at a slow enough rate to be captured by the transmit domain clock and then transferred to the receive domain. Only a formal check using full sequential analysis of behavior can do this correctly.

Figure 6 – Fast-to-slow clock domain crossing with data instability. It is important that the data is held stable long enough to be captured by the receive clock RX Clk2. If the data changes too quickly, an element of the data will be missing in the receive clock domain, as shown with D2 missing from the data stream in the receiving clock domain. This can be formally proven using the DATA_STABILITY check in Meridian CDC as part of the formal analysis.

For all the formal checks, additional information is required beyond just using the structural checks. In structural checking, the environment can be captured automatically with very little user input required for resets and clocks. In contrast, formal checks require that all the reset signals be very accurately associated with their corresponding clocks. All clock frequencies must be specified for the appropriate formal checks to be made on the fast-to-slow clock domain crossings. So setup for formal is necessarily more complex and requires detailed design knowledge about all the frequencies of clocks and combinations of those frequencies. For example, multi-mode designs also need the selection signals for mode selection to be specified by the user. Where appropriate, automatic multi-frequency analysis also can be addressed by the formal engines within Meridian CDC.

In Part Three, the conclusion for this series, we will discuss doing metastability-aware simulation on the whole design.

Related posts:

Tags: , , , , , ,

One Response to “CDC Verification of Fast-to-Slow Clocks – Part 2: Formal Checks”

  1. […] CDC Verification of Fast-to-Slow Clocks – Part 2: Formal Checks […]

Leave a Reply

Your email address will not be published. Required fields are marked *


You may use these HTML tags and attributes: <a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <cite> <code> <del datetime=""> <em> <i> <q cite=""> <strike> <strong>

CST Webinar Series
S2C: FPGA Base prototyping- Download white paper

Internet Business Systems © 2016 Internet Business Systems, Inc.
595 Millich Dr., Suite 216, Campbell, CA 95008
+1 (408)-337-6870 — Contact Us, or visit our other sites:
TechJobsCafe - Technical Jobs and Resumes EDACafe - Electronic Design Automation GISCafe - Geographical Information Services  MCADCafe - Mechanical Design and Engineering ShareCG - Share Computer Graphic (CG) Animation, 3D Art and 3D Models
  Privacy Policy