Analog/Mixed-signal (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

performance-limiting components in larger sub-systems, but they also now

account for a disproportionately high share of design bugs (and associated

designer-time and debugging costs). CAD tools for the accurate modelling,

analysis, high-speed 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, bug-free 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

differential-algebraic 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 over-simplified

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,

bug-free AMS design. We call this approach "Booleanization", which involves

approximating the continuous-domain 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

performance-limiting analog traits and characteristics), (2) ABCD-L, a technique

based on eigen-analysis that works well for Booleanizing Linear Time Invariant

(LTI) continuous systems, and (3) ABCD-NL, 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 non-linear AMS

designs. These three approaches together form the ABCD (Accurate Booleanization

of Continuous Dynamics) suite of Booleanization techniques.

Starting from SPICE-level netlists, we apply the techniques above to Booleanize

a variety of AMS circuits including latches and flip-flops, 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 state-of-the-art Boolean verification and

model-checking 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 discrete-time, in the logical domain) than

SPICE-level models; so, in many situations, ABCD-generated models may be usable

as much faster, almost-as-accurate, drop-in replacements for SPICE. Thirdly, by

virtue of being all-Boolean, ABCD-generated 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 co-analysis procedure (called the Berkeley

Eye Estimator, or BEE) for carrying out highly accurate worst case and

stochastic eye diagram analysis of modern high-speed communication sub-systems

that use correlated bitstreams and coding strategies to minimize bit error

rates.