Pragmatic Formal Verification Methodology for Clock Domain Crossing (CDC)

TL;DR

This paper proposes a practical formal verification approach for Clock Domain Crossings in complex SoC designs, aiming to reduce metastability issues and improve bug detection over traditional methods.

Contribution

It introduces a formal verification methodology that employs Metastability Injection to effectively identify CDC-related bugs in modern asynchronous and GALS-based SoC designs.

Findings

Enhanced bug detection in CDC paths

Reduced verification time for CDC issues

Improved reliability of SoC designs

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.