Achieving Glitch-Free Clock Domain Crossing Signals Using Formal Verification, Static Timing Analysis, and Sequential Equivalence Checking

Current System-on-a-chip (SoC) designs contain increased levels of functional and structural complexities within a single system. With the integration of multiple designs, various clock domains are introduced. In this paper, we present a solution for finding clock domain crossing glitch using a combination of formal verification and static timing analysis techniques. This paper also talks about leveraging a formal verification tool to do sequential equivalence checking between a buggy design and bug fixed design if CDC glitch is found in late design stages.