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.

Advisors: 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.},
}

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