UBC Theses and Dissertations

UBC Theses Logo

UBC Theses and Dissertations

Formal verification of a digital PLL Wei, Jijie


Common AMS circuit are composed from blocks that can be modeled accurately using linear differential inclusions to enable verification of important properties using reachability analysis. This dissertation presents a formal verification of Digital Phase Locked Loop (PLL) using reachability techniques. PLLs are ubiquitous in analog mixed signal (AMS) designs and are widely used in modern communication equipment, clock generation for CPUs in computers, clock-acquisition in high-speed links etc. The most important property of a PLL is convergence, which means starting from any possible initial conditions, the PLL will eventually lock to the desired equilibrium. We model the digital PLL as a set of Ordinary Differential equation (ODEs), and discretize the weakly non-linear ODEs to linear differential inclusions. The transformation not only provides us an over approximation of the verification problem but also provides the basis for a sound proof. We present the verification of a digital PLL using real tools, SpaceEx and Coho. In particular, we show how each component of the digital PLL can be modelled as a hybrid automaton. Due to the large number of transitions caused by the model, the whole proof is established by several lemmas. Interesting problems such as a timing glitch in the Phase Frequency Detector (PFD) are discussed and triggering conditions are formally proved in the dissertation. Global convergence is demonstrated by both tools. Based on the digital PLL circuit and the challenges that arose during our verification, the error bounds, limitations, implementation differences and usability of the two leading tools are carefully evaluated. SpaceEx provides a graphical user interface that makes it easy to get started with simple examples but requires extensive user interaction for larger problems. The interface to Coho is a MATLAB API. While this lacks the packaged-tool feel of SpaceEx, it provides a flexible way to break a large verification problem into smaller lemmas and allows the proof to be ''re-executed'' simply by re-executing the MATLAB script.

Item Media

Item Citations and Data


Attribution-NonCommercial-NoDerivs 2.5 Canada