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