Skip to main content

Formal verification of phase-locked loops using reachability analysis and continuization

Publication ,  Conference
Althoff, M; Yaldiz, S; Rajhans, A; Li, X; Krogh, BH; Pileggi, L
Published in: IEEE/ACM International Conference on Computer-Aided Design, Digest of Technical Papers, ICCAD
December 1, 2011

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. © 2011 IEEE.

Duke Scholars

Altmetric Attention Stats
Dimensions Citation Stats

Published In

IEEE/ACM International Conference on Computer-Aided Design, Digest of Technical Papers, ICCAD

DOI

ISSN

1092-3152

ISBN

9781457713989

Publication Date

December 1, 2011

Start / End Page

659 / 666
 

Citation

APA
Chicago
ICMJE
MLA
NLM
Althoff, M., Yaldiz, S., Rajhans, A., Li, X., Krogh, B. H., & Pileggi, L. (2011). Formal verification of phase-locked loops using reachability analysis and continuization. In IEEE/ACM International Conference on Computer-Aided Design, Digest of Technical Papers, ICCAD (pp. 659–666). https://doi.org/10.1109/ICCAD.2011.6105400
Althoff, M., S. Yaldiz, A. Rajhans, X. Li, B. H. Krogh, and L. Pileggi. “Formal verification of phase-locked loops using reachability analysis and continuization.” In IEEE/ACM International Conference on Computer-Aided Design, Digest of Technical Papers, ICCAD, 659–66, 2011. https://doi.org/10.1109/ICCAD.2011.6105400.
Althoff M, Yaldiz S, Rajhans A, Li X, Krogh BH, Pileggi L. Formal verification of phase-locked loops using reachability analysis and continuization. In: IEEE/ACM International Conference on Computer-Aided Design, Digest of Technical Papers, ICCAD. 2011. p. 659–66.
Althoff, M., et al. “Formal verification of phase-locked loops using reachability analysis and continuization.” IEEE/ACM International Conference on Computer-Aided Design, Digest of Technical Papers, ICCAD, 2011, pp. 659–66. Scopus, doi:10.1109/ICCAD.2011.6105400.
Althoff M, Yaldiz S, Rajhans A, Li X, Krogh BH, Pileggi L. Formal verification of phase-locked loops using reachability analysis and continuization. IEEE/ACM International Conference on Computer-Aided Design, Digest of Technical Papers, ICCAD. 2011. p. 659–666.

Published In

IEEE/ACM International Conference on Computer-Aided Design, Digest of Technical Papers, ICCAD

DOI

ISSN

1092-3152

ISBN

9781457713989

Publication Date

December 1, 2011

Start / End Page

659 / 666