results on computing reachable sets for linear systems with
bounded uncertain parameters. Using the equations that govern the continuous dynamics of the PLL, we create a discrete-time model that generates tight overapproximations of the
reachable sets at the beginning of each continuous-time
cycle. Since the actual times at which the discrete transitions
occur can vary, we introduce bounded uncertain parameters
in the linear discrete-time model that account for the variations in the actual transition times. We call this process of
mapping variations in time into parameter uncertainties
continuizaton.
3 Finally, we show that satisfaction of the PLL
specifications for the discrete-time model guarantees the
specifications are satisfied at all points in time. The reachable sets for the discrete time model can be computed very
fast, and the time reduced further by taking advantage of
certain symmetries in the PLL dynamics. Our approach illustrates how the successful use of formal methods to solve real
problems often requires extensions and insights that exploit
the particular structure and features of the target application. It is an enabling technique that facilitates us to efficiently verify a PLL at all possible operation conditions.
We begin in the next section by showing how a class of
charge-pump PLLs can be modeled at the behavioral level
using hybrid automata with uncertain parameters. Section
3 presents a conversion of the continuous-time behavioral
model to a discrete-time model, which provides the solution of the original model after each cycle. Variations in
switching times of the PLL are abstracted away in Section 4
using the new concept of continuization. This makes it possible to abstract the hybrid dynamics of the PLL by a linear
system with uncertain parameters. Using the model resulting from continuization, Section 5 presents the application
of reachability analysis for formal verification of the PLL
specifications, and Section 6 presents a comparison of the
verification results using reachability to the classical simulation approach. The concluding section summarizes the
contributions of this paper.
2. PLL BehAVioRAL moDeL
We consider the dual path, type II, third-order charge-pump PLL shown in Figure 2, consisting of a reference signal generator (Ref), a voltage-controlled oscillator (VCO), a
phase frequency detector (PFD), and charge pumps (CPs),
along with RC circuits to implement a PI controller for the
research highlights
communication systems, from satellites to mobile phones,
as well as in many other applications such as clock generation for microprocessors. The charge-pump PLL is one of the
popular PLL architectures.
7 It is an AMS circuit: the error signal driving the analog feedback is generated by digital logic.
7
The primary requirements to be verified for a PLL are
the circuit’s locking time and stability. These specifications are illustrated in Figure 1. Locking time is a transient
specification: the PLL state must reach the invariant region
within a specified number of cycles. Stability is an invariant
specification: from some set of initial states, the magnitude
of the phase difference must remain within a given bound
indefinitely. Both of these specifications must be achieved
robustly, that is, from an arbitrary initial state and over a
range of parameter values that reflect the target operating conditions (e.g., a given temperature range) as well as
the inherent uncertainties that will arise from the detailed
design and manufacturing processes. Verifying the behavioral model of a PLL using simulation is time consuming and
ultimately inconclusive because: (i) locking can take a few
thousand cycles, so very long simulation runs are required;
(ii) each simulation run represents 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; and (iii) invariance can only be inferred, but not
guaranteed, because simulations cannot be run indefinitely.
We present a method for verifying both the transient and
invariant specifications for a PLL over entire ranges of initial
states and parameter values using reachable set computations that can be performed in the same amount of time currently required to simulate the circuit models for just a few
selected points in the design space. Our approach relies on
some new techniques tailored to the PLL problem because
locking can require thousands of cycles, which implies
there will be thousands of discrete transitions in the switching logic. Experiments with existing methods implemented
in tools such as PHAVer5 or SpaceEx6 show that the overapproximations using existing methods become inaccurate
so quickly that it is impossible to demonstrate that locking
occurs, even for simple cases where locking can be demonstrated analytically.
The main technical contribution of this paper is a new
method for computing accurate overapproximations of reachable sets for hybrid systems when there are a large number of
discrete state transitions. This approach leverages previous
figure 1. transient (locking time) and invariant (stability)
specifications for a PLL.
0 500 1000 1500
–0.3
–0.2
–0.1
0
Cycle number
P
h
a
se
di
ff
er
en
ce
∆
Φ
Ci
Cp1
CP
Rp2
Rp3
frequency
divider
1/N
Cp3
vi
vp1 vp ip
ii
Φref
Φv
phase
frequency
detector
(PFD)
Ref
UP VCO
DN
figure 2. Dual-path charge-pump PLL.