Formal verification of a digital PLL
department or school: Science, Faculty of
department or school: Computer Science, Department of
data provider: DSpace
degree campus: UBCV
creator: Wei, Jijie
issued: 2014-08-19T17:27:23Z
issued: 2014
related degree: Master of Science - MSc
degree grantor: University of British Columbia
description: 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…
aggregated CHO: https://circle.library.ubc.ca/rest/handle/2429/50048
note: Formal Verification of A Digital PLLbyJijie WeiB. Computer Science, Harbin Normal University, 2009M. Computer Science, Harbin Engineering University, 2012A THESIS SUBMITTED IN PARTIAL FULFILLMENTOF THE REQUIREMENTS FOR THE DEGREE OFMaster of ScienceinTHE FACULTY OF GRADUATE AND POSTDOCTORALSTUDIES(Computer Science)The University Of British Columbia(Vancouver)August 2014c© Jijie Wei, 2014AbstractCommon AMS circuit are composed from blocks that can be modeled accuratelyusing linear differential inclusions to enable verification of important properties us-ing reachability analysis. This dissertation presents a formal verification of DigitalPhase Locked Loop (PLL) using reachability techniques.PLLs are ubiquitous in analog mixed signal (AMS) designs and are widely usedin modern communication equipment, clock generation for CPUs in computers,clock-acquisition in high-speed links etc. The most important property of a PLLis convergence, which means starting from any possible initial conditions, the PLLwill eventually lock to the desired equilibrium. We model the digital PLL as aset of Ordinary Differential equation (ODEs), and discretize the weakly non-linearODEs to linear differential inclusions. The transformation not only provides us anover approximation of the verification problem but also provides the basis for asound proof.We present the verification of a digital PLL using real tools, SPACEEX andCOHO-REACH. In particular, we show how each component of the digital PLLcan be modelled as a hybrid automaton. Due to the large number of transitionscaused by the model, the whole proof is established by several lemmas. Interest-ing problems such as a timing glitch in the Phase Frequency Detector (PFD) arediscussed and triggering conditions are formally proved in the dissertation. Globalconvergence is demonstrated by both tools.Based on the digital PLL circuit and the challenges that arose during our ver-ification, the error bounds, limitations, implementation differences and…
has type: Thesis/Dissertation
date issued: 2014-09
is shown at: 10.14288/1.0165974
language: eng
degree discipline: Computer Science
provider: Vancouver : University of British Columbia Library
publisher: University of British Columbia
rights: Attribution-NonCommercial-NoDerivs 2.5 Canada
rights URI: http://creativecommons.org/licenses/by-nc-nd/2.5/ca/
scholar level: Graduate
type: Text
identifier URI: http://hdl.handle.net/2429/50048