Clock domain crossing (CDC) verification has become a critical component in ensuring correct design operations for complex SOC. CDC verification is not a nice-to-have checklist item any more for ASIC and FPGA design and verification teams. Adopting special technology for CDC verification has become a must-have item in the verification flow in order to ensure reliable chip operations in the field.

The reason that designers are concerned about CDC is metastability propagation, which is the root cause of all CDC failures. Metastability happens as a result of the domain crossing signal changing its value while being sampled within the setup and hold window of the receiving clock. Due to the asynchronous nature of the transmitting and receiving clocks, metastability is unavoidable. The key is to prevent metastability from propagating to the downstream logics, or in another word, to make sure that the domain crossing signals stay stable during the capture.

Typical design techniques to ensure safe CDC operations include the usage of synchronization schemes to control signal crossings, such as using handshake and FIFO protocols for data transfer. Although structural analysis can provide valuable information on domain crossing signals and identify potential CDC errors, such as missing synchronization, glitch potentials and signal reconvergence, etc, structural analysis alone is not sufficient to detect all possible CDC failures. Furthermore, structural analysis can often be pessimistic and introduces noise in the reported errors. This is where the power of formal analysis comes in for complete and accurate CDC verification.

Traditionally, formal verification has been refered to equivalence checking and model checking (also called property verification). Equivalence checking compares the functionality of two designs to see if they are equivalent. Model checking verifies to see if the functionality of the design conforms to the desired behavior, typically expressed in the form of assertions (also called properties). While equivalence checking has been widely adopted in the verification flow, model checking, hindered by the difficulties of writing assertions, has not been as successful.

In the last decade, formal analysis techniques, enabled by automation, have found wide acceptance and usage among various applications. For example, using automatic formal analysis techniques, designers can verify state machines to make sure there is no single state or pair-wise state deadlock without the need of writing any assertions. Such techniques are popular because of ease of use and exhaustive coverage. Ease of use comes from the fact that no assertion needs to be written and no testbench needs to be created. Exhaustive coverage is the benefit of formal technology. Automatic formal verification increases verification efficiency and promise higher return on investment for design and verification teams.

Formal analysis techniques can also be applied to CDC verification. While designers or verification engineers can potentially write assertions to verify certain aspects of CDC functionality, a thorough verification effort would involve writing assertions for thousands of domain crossing signals in the design. This is not desirable because it takes huge effort besides being an error prone process. Confidence in reliable CDC operations can only be achieved through automatic formal CDC verification.

There are different synchronization schemes that designers can employ to ensure correct data transfer at the CDC boundary, with handshake and FIFO protocols being two of the forms. To offer complete verification and assurance, Formal CDC verification needs to have broader understanding of the design styles and performs appropriate analysis on each crossing, rather than restricting to verifying only aspects of the handshake and FIFO protocols.

Signals crossing asynchronous clock domains typically are either data signals which contain data to be sent downstream, or control signals which control the sampling of the data signals at the domain boundary. Correct identification of the role of the crossing signals and then applying appropriate checks need to be the foundation of formal CDC verification.

Data crossings need to be multi-cycle paths no matter what kind of synchronization scheme is deployed to safe-guard against metastability propagation. This means data being transmitted from the transmit clock domain should NOT be sampled at the next receiving clock edge. If this is not true, then metastability will sure propagate, resulting in undesired design behavior. We call this formal data stability check. One of the benefits of formal technology is the ability to generate a counterexample to show the failure trace if a violation is found.

On control crossings, it is important to make sure no glitch or hazard can be generated. While structural analysis can identify all control crossings with combinational logic on the crossing paths, existence of combinational logic will not always lead to real glitch generation. Formal analysis is needed to identify true glitch potentials from false ones (noise). For control crossings going from fast to slow clock domains, it is also necessary to make sure that the control pulse is wide enough to be sampled by the receiving clock. Formal technology can be exploited here. Because of the exhaustive nature of formal analysis, any possible scenario that could lead to a narrow control pulse being missed at the receiving domain will be identified.

Formal data stability check applies to asynchronous FIFO verification as well to ensure there is no read and write at the same location and at the same time. The read and write addresses need to be gray coded to make sure only one signal changes value at a time. A gray code violation suggests that it is possible to have incorrect read and write addresses because the address bits could lose correlation going across asynchronous domains.

While structural analysis looks at the topology of the design to identify potential error sources, formal analysis understands the real behavior of the design by taking into account operating frequencies and conditions. However this limits formal analysis results to be valid only for the operating conditions verified. Different operating points typically need to be verified separately for complete coverage. More advanced formal solution allows the design clocks to run free, i.e. with no assumption of frequency ratios between the transmitting and receiving clocks. Successful verification will guarantee correct CDC operations at all frequency points. The price to pay is performance, as the exhaustive nature of formal analysis does come with performance and capacity limitations.

Jin Zhangis technical marketing manager at Real Intent Inc.