FishTail’s CDC verification solution formally verifies that asynchronous clock domain crossings are correctly synchronized. Either RTL or netlist input is supported.

CDC Verification Features

Formal Verification of Clock Domain Crossing

Our approach to CDC verification is to formally verify each synchronizing structure (such as a FIFO for example) used by an engineering team, and then not revisit this verification when this synchronizing IP is instantiated in a design. We formally verify a synchronizing structure by proving that it is impossible for a zero-cycle path to exist between an asynchronous clock domain crossing after accounting for the functionality of the synchronizing logic and the handshake signals.

CDC Verification

What Makes us Different

Unlike all other CDC solutions that focus on recognizing synchronizing structures that are enumerated by designers, our focus is on formally verifying the correctness of synchronizing logic. This results in less noise. We provide a powerful GUI to debug formal failures.

SDC Verification Solutions