Formal Equivalence Verification of Phase Locked Loops

Abstract

Ever-growing complexity in VLSI is forcing logic design to move above the register transfer level (RTL). For example, functional specifications are being written in software. These specifications are written for clarity, and are not optimized or intended for synthesis. The Logic Synthesis as a process is prone to Bugs. There are too many transformations happening in logic synthesis which can alter the netlist in a wrong manner and make it infer functionality other than what was intended in the original RTL. These bugs are not intentional but happen by accident during synthesis tool development. So Formal Equivalence Verification (FEV) between the software specification and the implementation is needed.

In today's high-performance integrated circuits for clock & data recovery, modulation & demodulation, clock generation and frequency synthesis, PLLs are widely adopted. As the speed of systems increases, PLLs with higher operating frequency, faster lock acquisition and lower jitter are urgently in demand. The phase frequency detector (PFD), which helps PLLs achieve simultaneous phase and frequency error detection, is an indispensable functional block and plays an important role in improving the performance of the whole PLL system.

This report introduces the Formal Equivalence Verification approach for PLLs. It describes the method for formal equivalence verification. It also introduces the algorithm by which the FEV tool runs. This report imposes upon the importance of the Formal equivalence verification in VLSI design flow. Apart from FEV, this report also contains study work of various types of phase frequency detectors, its limitations and approaches to overcome those limitations and improve performance.