 Main
Accurate Booleanization of Continuous Dynamics for Analog/MixedSignal Design
 Aadithya, Karthik Venkatraman
 Advisor(s): Roychowdhury, Jaijeet S
Abstract
Analog/Mixedsignal (AMS) systems (e.g., ADCs and DACs, charge pumps,
comparators, SERDES systems and PLLs, etc.) are playing an increasingly
important role in modern chip design: they have not only become key
performancelimiting components in larger subsystems, but they also now
account for a disproportionately high share of design bugs (and associated
designertime and debugging costs). CAD tools for the accurate modelling,
analysis, highspeed simulation, formal verification, and debugging of AMS
systems have not been able to keep pace with the rapid growth in complexity of
these designs. Therefore, effective, bugfree AMS design remains a largely
unsolved problem today.
At the heart of this problem lies the fact that the analog components in AMS
systems are modelled in a very different way from the digital components. While
analog components are typically modelled as continuous dynamical systems using
differentialalgebraic equations (DAEs), the digital components are usually
modelled using clean Boolean abstractions such as truth tables and finite state
machines (FSMs). The formal analysis and verification of AMS systems,
therefore, typically involves having to simultaneously reason about both
continuous quantities and discrete quantities, which is inherently a very
difficult mathematical problem.
A variety of "hybrid system" methods and frameworks have been developed to
formally verify AMS designs. However, these methods tend to scale very poorly in
the number of continuous (analog) variables involved, often being able to handle
no more than 5 to 10 continuous variables. The enormous computational cost of
adding extra continuous variables in turn forces the adoption of highly
simplified behavioural macromodels for AMS components; these oversimplified
models do not capture the behaviour of the underlying AMS components accurately.
In this dissertation, we propose a new approach to the problem of effective,
bugfree AMS design. We call this approach "Booleanization", which involves
approximating the continuousdomain behaviour of AMS components using
purely Boolean models (such as FSMs). Booleanization works by first
discretizing the voltages and currents in the given AMS design, and then
encoding the analog dynamics of the given design in purely Boolean form using
FSM state transitions. The finer the discretization of the circuit's voltages
and currents, the greater the accuracy with which the resulting Boolean model
captures the circuit's continuous dynamics.
We propose three automated techniques for Booleanizing a wide variety of AMS
systems and components: (1) DAE2FSM, which is based on an adaptation of
Angluin's algorithm from computational learning theory, which works well for
Booleanizing "digitalish" designs (i.e., circuits whose intended functionality
is purely digital, but which nevertheless exhibit significant
performancelimiting analog traits and characteristics), (2) ABCDL, a technique
based on eigenanalysis that works well for Booleanizing Linear Time Invariant
(LTI) continuous systems, and (3) ABCDNL, a technique based on separating the
underlying circuit's dynamics into DC and transient components, which works well
for Booleanizing a large class of genuinely analog, genuinely nonlinear AMS
designs. These three approaches together form the ABCD (Accurate Booleanization
of Continuous Dynamics) suite of Booleanization techniques.
Starting from SPICElevel netlists, we apply the techniques above to Booleanize
a variety of AMS circuits including latches and flipflops, digital logic blocks
such as counters, charge pumps, delay lines, equalizers, filters, I/O links,
ADCs and DACs, comparators, power grid networks, etc. In each of these cases,
we show that the Boolean models generated by ABCD are indeed able to capture
the underlying analog dynamics of these systems with high accuracy.
We believe that Booleanization offers several compelling features. Firstly,
since the generated models are all purely Boolean, they can be used in
conjunction with existing stateoftheart Boolean verification and
modelchecking engines (such as ABC) to formally verify AMS designs in a
scalable way. Secondly, the Boolean models produced by ABCD can be simulated
much more efficiently (in discretetime, in the logical domain) than
SPICElevel models; so, in many situations, ABCDgenerated models may be usable
as much faster, almostasaccurate, dropin replacements for SPICE. Thirdly, by
virtue of being allBoolean, ABCDgenerated models enable one to accurately
represent analog dynamics without incurring the severe penalty of adding
continuous variables; so ABCD models may be usable in conjunction with existing
hybrid system methodologies, frameworks, and verification flows  thereby
helping these approaches scale to much larger problem sizes than they can do so
at present. Finally, ABCD models can also be used in a variety of niche
algorithms and "custom" analysis procedures aimed at solving targeted AMS
design problems for specific systems and applications; for example, we have
developed an efficient Boolean/LTI coanalysis procedure (called the Berkeley
Eye Estimator, or BEE) for carrying out highly accurate worst case and
stochastic eye diagram analysis of modern highspeed communication subsystems
that use correlated bitstreams and coding strategies to minimize bit error
rates.
Main Content
Enter the password to open this PDF file:













