Communications of the ACM

100 CommuniCAtions of the ACm | OCTObER 2013 | vOl. 56 | nO. 10 the system is in both_off again, which completes one cycle. Locking is achieved when the phase difference reaches and remains within the locked condition given by the interval [−0.1°, 0.1°].

3. time DisCRetizAtion

Given the hybrid automaton behavioral model of the PLL,
we first derive a discrete-time linear model with bounded
uncertain parameters based on the phase of the reference
signal, assuming the reference signal leads the VCO
signal, that is, for the discrete state sequence up_active →
both_active → both_off. The time for a cycle of the reference
signal is given by tcycle = 1/fref . Since the continuous dynamics
of the PLL is linear, we can take advantage of the superposi-
tion principle and obtain the initial state solution and the
input solution separately. The initial state solution for one
cycle is given by xh(t + tcycle)= e Atcycle x(t). The input solution
for constant input u over the time interval [0, r], where r is
the time the charge pump is active, can be written using the
Taylor series of e At as
( 2)

where A ⊕ B = {a + b|a ∈ A, b ∈ B} is a Minkowski addition
and A ⊗ B={ab|a ∈ A, b ∈ B} a set-based multiplication.
Note that sets can be sets of scalars, vectors, or matrices, and
sets may also contain just a single (certain) element. The
set multiplication sign is sometimes dropped when the
context makes it clear that uncertain matrices are involved.
The standard operator precedence rules apply. The set of
remainders E p(r) is overapproximated by an interval matrix,
that is, a matrix with lower and upper bounds on each ele-
ment, as presented in Althoff et al. 3 Since there is no input
for the rest of the cycle, the input solution after one cycle is
xp(tcycle) ∈ e A(tcycle–r) Γ(r)u. Let ton denote the time the system
is in location up_active and recall that td is the time it is in
both_active. Also, let u denote the input in up_active and ud
denote the input in both_active. Finally, defining xk = x(k tcycle),
the combination of the initial state solution and all input
solutions can be written as
( 3)

The above formula is a discrete-time overapproximation of the continuous-time evolution after one cycle.

4. ContinuizAtion

The model derived above computes the state of the system after one cycle when the switching time of the charge pumps is known. In this section, we develop a model that computes the range of state values that can occur at each cycle, for the entire range of possible switching times ton (while td is a given constant). A closed form solution does not exist for ton, which research highlights

depends on the state of the system. Simulation techniques obtain ton by detecting a zero-crossing which corresponds to crossing the guard condition Φv ==0. Here we propose a more efficient method based on overapproximating the interval of possible values for ton. Since ton depends only on

Φv = x4, it is sufficient to consider (see ( 1) )

( 4)

We assume user-defined bounds ,
which are monitored during the verification process. Viola-
tion of these bounds would require to restart the verification
with larger intervals. Applying interval arithmetic to ( 4)
results in the bound . We further extract the bound
on x4 from the reachable set at the beginning of each
cycle. We obtain
using the fact that the reference signal is leading
resulting in
( 5)

Using bounds on the switching times derived above, we
use the concept of continuization to compute the set of
reachable states resulting from uncertain switching times.
To compute the reachable set under uncertain switching
times (see Figure 5), we modify ( 3) and compute the solution
successively, first of k at times tk + on, then of k+ 1 at times
tk+ 1. This makes it possible to reset the uncertain switching
time to values in the interval [0, ∆ton], ∆ton = on − on com-
pared to [ on, on], which has computational benefits when
evaluating Taylor series since higher order terms can be
tightly bounded. The new equations are:
( 6)