Accurate Booleanization of Continuous Dynamics for Analog/Mixed-Signal Design

Karthik Aadithya

EECS Department
University of California, Berkeley
Technical Report No. UCB/EECS-2016-146
August 12, 2016

http://www2.eecs.berkeley.edu/Pubs/TechRpts/2016/EECS-2016-146.pdf

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 the 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.

Advisor: Jaijeet Roychowdhury


BibTeX citation:

@phdthesis{Aadithya:EECS-2016-146,
    Author = {Aadithya, Karthik},
    Title = {Accurate Booleanization of Continuous Dynamics for Analog/Mixed-Signal Design},
    School = {EECS Department, University of California, Berkeley},
    Year = {2016},
    Month = {Aug},
    URL = {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2016/EECS-2016-146.html},
    Number = {UCB/EECS-2016-146},
    Abstract = {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
the 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.}
}

EndNote citation:

%0 Thesis
%A Aadithya, Karthik
%T Accurate Booleanization of Continuous Dynamics for Analog/Mixed-Signal Design
%I EECS Department, University of California, Berkeley
%D 2016
%8 August 12
%@ UCB/EECS-2016-146
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2016/EECS-2016-146.html
%F Aadithya:EECS-2016-146