Inevitability of Phase-locking in a Charge Pump Phase Lock Loop using Deductive Verification

Asad, H. & Jones, K. (2015). Inevitability of Phase-locking in a Charge Pump Phase Lock Loop using Deductive Verification. Paper presented at the 25th edition on Great Lakes Symposium on VLSI, 20-05-2015 - 22-05-2015, Pittsburgh, USA.

[img]
Preview
Text - Accepted Version
Download (881kB) | Preview

Abstract

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 and the node voltages vanish. We verify this property for a CP PLL using deductive verification. We split this complex property into two sub-properties defined in two disjoint subsets of the state space. We deductively verify the first property using multiple Lyapunov certificates for hybrid systems, and use the Escape certificate for the verification of the second property. Construction of deductive certificates involves 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.

Item Type: Conference or Workshop Item (Paper)
Additional Information: © Ul Asad | ACM 2015. This is the author's version of the work. It is posted here for your personal use. Not for redistribution. The definitive Version of Record was published in GLSVLSI '15 Proceedings of the 25th edition on Great Lakes Symposium on VLSI, http://dx.doi.org/10.1145/2742060.2742072
Uncontrolled Keywords: Deductive Verification; AMS Circuits; Lyapunov Certificate; Escape Certificate; SOS Programming
Subjects: T Technology > TA Engineering (General). Civil engineering (General)
Divisions: School of Informatics > Department of Computing
URI: http://openaccess.city.ac.uk/id/eprint/12327

Actions (login required)

View Item View Item

Downloads

Downloads per month over past year

View more statistics