Pragmatic Formal Verification Methodology for Clock Domain Crossing (CDC)
Aman Kumar, Muhammad Ul Haque Khan, Bijitendra Mittra
TL;DR
Clock Domain Crossing in multi-clock SoCs is prone to metastability, and conventional verification often misses metastability propagation and data loss issues, driving costly silicon re-spins. The paper proposes a pragmatic formal verification methodology that integrates metastability injection with both formal and simulation-based verification, plus a CDC coverage model and an automated CDC code generator. The approach connects design sign-off and verification sign-off through a metamodel-based framework and leverages MSI to reveal metastability effects at IP and SoC levels. Results demonstrate the method finds hard-to-detect CDC bugs across designs, reduces verification gaps, and offers a scalable path toward robust CDC verification with practical silicon-readiness benefits.
Abstract
Modern System-on-Chip (SoC) designs are becoming more and more complex due to the technology upscaling. SoC designs often operate on multiple asynchronous clock domains, further adding to the complexity of the overall design. To make the devices power efficient, designers take a Globally-Asynchronous Locally-Synchronous (GALS) approach that creates multiple asynchronous domains. These Clock Domain Crossings (CDC) are prone to metastability effects, and functional verification of such CDC is very important to ensure that no bug escapes. Conventional verification methods, such as register transfer level (RTL) simulations and static timing analysis, are not enough to address these CDC issues, which may lead to verification gaps. Additionally, identifying these CDC-related bugs is very time-consuming and is one of the most common reasons for costly silicon re-spins. This paper is focused on the development of a pragmatic formal verification methodology to minimize the CDC issues by exercising Metastability Injection (MSI) in different CDC paths.