TY - GEN
T1 - Formal verification of phase-locked loops using reachability analysis and continuization
AU - Althoff, Matthias
AU - Yaldiz, Soner
AU - Rajhans, Akshay
AU - Li, Xin
AU - Krogh, Bruce H.
AU - Pileggi, Larry
PY - 2011
Y1 - 2011
N2 - We present an approach for verifying locking of charge-pump phase-locked loops by performing reachability analysis on a behavioral model of the circuit. Bounded uncertain parameters in the behavioral model make it possible to represent all possible behaviors of more detailed models. The dynamics of the behavioral model is hybrid (i.e., discrete and continuous) due to the switching of charge pumps that drive the analog control circuits. A unique feature of phase-locked loops compared to most other hybrid systems is that they require thousands of switchings in the continuous dynamics to converge sufficiently close to a limit cycle. This makes reachability analysis a challenging task since switches in the dynamics are expensive to compute and result in conservative overapproximations. We solve this problem by overapproximating the effects of the switching conditions with uncertain parameters in linear continuous models, a method we call continuization. Using efficient reachability algorithms for discrete-time linear systems, locking is verified over the complete range of possible initial states of a charge-pump PLL designed in 32nm CMOS SOI technology in comparable time required for Monte Carlo simulations of the same behavioral model.
AB - We present an approach for verifying locking of charge-pump phase-locked loops by performing reachability analysis on a behavioral model of the circuit. Bounded uncertain parameters in the behavioral model make it possible to represent all possible behaviors of more detailed models. The dynamics of the behavioral model is hybrid (i.e., discrete and continuous) due to the switching of charge pumps that drive the analog control circuits. A unique feature of phase-locked loops compared to most other hybrid systems is that they require thousands of switchings in the continuous dynamics to converge sufficiently close to a limit cycle. This makes reachability analysis a challenging task since switches in the dynamics are expensive to compute and result in conservative overapproximations. We solve this problem by overapproximating the effects of the switching conditions with uncertain parameters in linear continuous models, a method we call continuization. Using efficient reachability algorithms for discrete-time linear systems, locking is verified over the complete range of possible initial states of a charge-pump PLL designed in 32nm CMOS SOI technology in comparable time required for Monte Carlo simulations of the same behavioral model.
UR - http://www.scopus.com/inward/record.url?scp=84862953445&partnerID=8YFLogxK
U2 - 10.1109/ICCAD.2011.6105400
DO - 10.1109/ICCAD.2011.6105400
M3 - Conference contribution
AN - SCOPUS:84862953445
SN - 9781457713989
T3 - IEEE/ACM International Conference on Computer-Aided Design, Digest of Technical Papers, ICCAD
SP - 659
EP - 666
BT - 2011 IEEE/ACM International Conference on Computer-Aided Design, ICCAD 2011
T2 - 2011 IEEE/ACM International Conference on Computer-Aided Design, ICCAD 2011
Y2 - 7 November 2011 through 10 November 2011
ER -