Unleash the power of formal technology for CDC verification

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.