Formal Verification of Phase-Locked Loops Using Reachability
Analysis and Continuization
By Matthias Althoff, Akshay Rajhans, Bruce H. Krogh, Soner Yaldiz, Xin Li, and Larry Pileggi
We present a scalable and formal technique to verify locking
time and stability for charge-pump phase-locked loops
(PLLs). In contrast to the traditional simulation approach
that only validates the PLL at a given operation condition,
our proposed technique formally verified the PLL at all
possible operation conditions. The dynamics of the PLL is
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 the large number of cycles required for locking. We develop a new method
for computing effective overapproximations of the sets of
states reached on each cycle by using uncertain parameters
in a discrete-time model to represent 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.
In the standard design flow for analog mixed signal (AMS)
circuits, the complete circuit is decomposed into its principal elements or blocks, which are first analyzed and designed
using idealized low-order behavioral models. Detailed
circuit-level designs are implemented only after the performance specifications have been verified at the block level
over the required range of parameter variations and operating conditions. The goal is to create robust designs to avoid
costly redesign cycles in the downstream process.
Because of the complexity of the mixed continuous
and discrete (i.e., hybrid) AMS dynamics, there are no
analytical techniques to verify a given design satisfies
the circuit specifications, even for the simplified block-
level behavioral models. Thus, numerical simulation has
been the standard tool for evaluating the performance
of behavioral models. Simulation is not completely sat-
isfactory, however, because each simulation run repre-
sents the behavior for only one set of values for the initial
states and parameters, so many simulations are required
to assess the robustness of the design. Moreover, some
specifications can be verified only after simulations have
run for very long durations, and some specifications such
as stability cannot be confirmed with absolute certainty
because simulations cannot be run indefinitely.
This paper demonstrates an alternative to simulation
based on formal methods. Formal methods offer an attrac-
tive alternative to simulation because they can verify that
specifications for a circuit are satisfied for all possible behav-
iors over entire ranges of initial states and parameter values.
This corresponds to an infinite number of simulation runs
of unbounded duration. In their survey of the literature on
formal verification for AMS designs, Zaki et al. categorize
the methods into equivalence checking, automated state-
space exploration, run-time verification, and proof-based
11 Reachability analysis, the technique developed
in this paper, is a form of automated state-space exploration.
The basic idea of reachability analysis is to use the
dynamic equations for the circuit to propagate the trajec-
tories of entire sets of states over time, rather than just a
single state trajectory. The key issues are how to represent
sets of states numerically and how to propagate these sets
efficiently. Good techniques have been developed to repre-
sent and compute reachable sets for continuous dynamic
systems (see e.g. Althoff
1 and Girard et al.
8). All of these
techniques are based on overapproximations, since the
actual sets of reachable states are not convex in general.
These overapproximations become less accurate as time pro-
gresses, however, and for hybrid dynamic systems the over-
approximations become even less accurate and more time
consuming to compute due to the need to compute over-
approximations of intersections of reachable sets with the
surfaces representing switching conditions.
2, 6 Therefore,
current reachability analysis techniques for hybrid systems
are effective when there are only a few discrete transitions in
the time interval of interest.
To demonstrate the applicability of formal methods
and reachability analysis to AMS circuits, we consider the
verification of block-level behavioral models for a class of
phase-locked loops (PLLs). PLLs are integrated circuits that
produce high-frequency output signals that are synchronized to and in phase with low-frequency reference signals.
Originally developed in the 1930’s as a circuit for radio
receivers, millions of PLLs are now used in virtually all digital
The original version of this paper was published in the
Proceedings of the International Conference on Computer
Aided Design, 2011, pp. 659–666.