Communications of the ACM

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)