ABCD: “Booleanizing” Analog
Systems for Verifying Chips
Aadithya V. Karthik,
Sayak Ray, Pierluigi Nuzzo, Alan Mishchenko,
Robert Brayton, and Jaijeet Roychowdhury
EECS Dept., The University of California, Berkeley
Feb 2014, BEARS, Berkeley
Aadithya V. Karthik <[email protected]>
Feb 2014, BEARS lightning talk, Berkeley
1/6
The Problem: Verifying a Chip
Specification
Chip designers
Chip
Aadithya V. Karthik <[email protected]>
Feb 2014, BEARS lightning talk, Berkeley
2/6
The Problem: AMS Verification
Example: SERDES
CDR
PLL
Analog
parts
I/O
Surrounded by
Digital Logic
 Want to verify complete system
>1V
o e.g., eye opening height > 1V?
 Proof or counter-example needed
Aadithya V. Karthik <[email protected]>
Feb 2014, BEARS lightning talk, Berkeley
3/6
Our approach: “Booleanize” the analog parts
AnalogBoolean
models + Digital models
ABCD:
(don't mix)
approximation
ALL
Continuous
Boolean
BOOLEAN
Best verification tools = all Boolean, no continuous
Challenge:
SAR-ADC
Boolean T/H
approximation
Analog components
Boolean
comparator
approximation
Boolean DAC
approximation
Digital components
Verification tools accept
Fast
Formal verification, high-speed simulation, test pattern generation, ...
… for the full combined system!
Aadithya V. Karthik <[email protected]>
Feb 2014, BEARS lightning talk, Berkeley
4/6
ABCD in action
Analog Circuit
ABCD
Purely Boolean
Model
Example: Channel + Equalizer
Bit Sequence
Aadithya V. Karthik <[email protected]>
Feb 2014, BEARS lightning talk, Berkeley
5/6
Circuits Successfully Booleanized
Delay line
Charge pump
Power grid
Equalizer
I/O signaling system
SAR-ADC
Aadithya V. Karthik <[email protected]>
Feb 2014, BEARS lightning talk, Berkeley
6/6