Formal Verification of Behavioral Models of Phase-Locked Loops (PLLs) Made Tractable With New Methods for Computing Reachable Sets for Hybrid Dynamic Systems

CMACS Post-Doctoral Researcher Matthais Althoff developed a number of new techniques for computing tight over-approximations of reachable sets for hybrid dynamic systems, dynamic systems with both continuous and discrete state variables. In collaboration with CMACS Professor Bruce Krogh, CMU ECE Ph.D. student Akshay Rahjans, and researchers in the CMU Center for Silicon System Implementation (CSSI), Altoff applied his techniques to develop a new scalable and formal technique to verify locking time and stability for charge-pump phase-locked loops (PLLs). The dynamics of the PLL are described by a hybrid automaton, which incorporates the differential equations of the analog circuit elements as well as the switching logic of the digital circuit elements. Existing methods for computing reachable sets for hybrid automata cannot be used to verify the PLL model due to large number of cycles required for locking. We develop a new method for computing effective over-approximations of the sets of states reached on each cycle by using uncertain parameters in a discrete-time model to represent the sets of possible states that will be reached over the range of possible switching times, a technique we call continuization. Using this new method for reachability analysis, it is possible to verify locking specifications for a charge-pump PLL design for all possible initial states and parameter values in time comparable to the time required for a few simulation runs of the same behavioral model.

This research, which first appeared in a paper that won the Best Paper Award at the 2011 International Conference on Computer Aided Design (ICCAD), is described in the following ACM Research Highlights paper: Formal Verification of Phase-Locked Loops Using Reachability Analysis and Continuization

M. Althoff, A. Rajhans, B. H. Krogh, S. Yaldiz, X. Li, L. Pileggi, Formal Verification of Phase-Locked Loops Using Reachability Analysis and Continuization, Communications of the ACM, Vol. 56 No. 10, Pages 97-104.

Matthias Althoff is now an assistant professor in the Department of Robotics and Embedded Systems at the Technical University of Munich ( www6.in.tum.de/Main/Althoff ).