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 Two: Formal Checks
January 16th, 2014 by Dr. Roger B. Hughes, Director of Strategic Accounts
In Part One, 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.
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.
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.
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.