Verifying inevitability of phase-locking in a charge pump phase lock loop using sum of squares programming

Phase-locking in a charge pump (CP) phase lock loop (PLL) is said to be inevitable if all possible states of the CP PLL eventually converge to the equilibrium where the input and output phases are in lock. We verify this property for a CP PLL using a mixed deductive and bounded verification methodology. This involves a positivity check of polynomial inequalities (which is an NP-Hard problem) so we use the sound but incomplete Sum of Squares (SOS) relaxation algorithm to provide a numerical solution.