  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.
