Doi: 10.1145/2507771.2507783

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

Abstract

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.

1. intRoDuCtion

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
methods. 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.