OCTObER2013 | vOl. 56 | nO. 10 | CommuniCAtions of the ACm 99
where the resistor and capacitor values are given in Figure 2
and the values Ki, Kp, and f0 determine the frequency of the
VCO: . Input values u vary depend-
ing on the signals leaving the PFD according to
The output signals of the PFD are determined by threshold
crossings of phase signals. The switching logic is described
by the automaton shown in Figure 3, where the states are
labeled as up_active, dn_active, both_active, and both_off.
Starting in both_off, the next discrete state of the hybrid
automaton is up_active if the reference signal leads by first
reaching Φref =2p, and dn_active when Φv =2p is reached
first. As shown in Figure 4, in order to use the same phase
crossings for the next cycle, the phase values are reset to
Φref : = Φref − 2p, Φv : = Φv − 2p upon continuing in up_active and
dn_active. Once the lagging signal has a zero-crossing, the
discrete state both_active is entered which models a time
delay td for switching off both charge pumps. After the delay,
Locking of the PLL is achieved by the PFD by comparing
the phases of the reference signal and the VCO signal and set-
ting the signals UP = 1 if the reference signal leads, and DN = 1
if it lags. These signals pump charge into or out of the capaci-
tors, changing voltages vp and vi, which serve as proportional
and integral (PI) control inputs to the VCO. For instance, if
the reference signal leads, it means that the reference signal
is faster than the VCO signal (when divided by N). In this case,
UP is set to 1 and the “up” current will charge the capacitors
so that the voltage values vi and vp increase. As a result, the
VCO frequency increases in order to catch the reference signal.
We do not consider adaptation of PLL parameters such as the
frequency divider, resistor, or capacitor values.
As one can see from Figure 2, different components of the
PLL system operate at different frequencies. For instance,
the reference signal is at low frequency, while the VCO signal
may be at extremely high frequency if the frequency divider
ratio N is large. The large difference in frequency makes PLL
simulation extremely challenging, since a traditional simulation tool must adopt a very small time step to numerically
solve the PLL response in time domain. It, in turn, results in
a very long simulation time.
The behavioral model of the charge-pump PLL is a hybrid
automaton4 with linear continuous dynamics and uncertain
parameters. Appropriate bounds on the uncertain parameters can be determined by equivalence checking with
detailed circuit models.
9, 10 These bounds should be chosen
to assure that the behavioral model represents all possible
behaviors of a detailed circuit model. If the more detailed
model is at the transistor level, the approach is also able to
catch issues at the transistor level. However, current equivalence checking techniques are typically semi-formal such
that a complete enclosure cannot yet be guaranteed.
The continuous state vector in the behavioral model is
x = [vi vp1 vp Φv Φref] T with input vector u = [ii ip]T (see Figure 2).
The dynamics are
( 1)
with
both_off
UP = 0,
DN = 0
dn_active
UP = 0,
DN = 1
up_active
UP = 1,
DN = 0
both_active
UP = 1,
DN = 1
guard: Φref == 2p
reset: Φv := Φv − 2p
Φref := 0
guard: Φv == 2p
reset: Φref := Φref − 2p
guard: Φref == 0
reset: t := 0
guard: Φv == 0
reset: t := 0
Φv := 0
guard: t == td
figure 3. hybrid automaton.
figure 4. typical charge pump activity.
IiUP
ton td
Φref
Φv
ii
t
t
t
2p
2p
0
0
0