Computing That Serves

Efficient Modeling and Verification of Analog/Mixed-Signal Circuits


Thursday, February 7, 2008 - 11:00am


Scott Little, SRC Fellow/PhD Candidate, University of Utah

Analog circuit design is traditionally done by expert designers in an ad hoc manner heavily dependent on SPICE simulation. This method has worked successfully for many years, but recent trends are prompting design managers to explore new and innovative techniques. Process variation for modern processes is increasing which results in significant design effort by analog designers to maintain acceptable yields. The increasing popularity of larger and more complex mixed-signal circuits poses a problem to the simulation dependent validation methodology as simulation of these large circuits is possible for a very limited number of vectors. Formal methods are used successfully to aid in the complex validation problem for digital circuits.
Our research leverages the ideas of digital formal methods and applies them to the analog/mixed-signal (AMS) circuit verification problem. In this talk, I describe a formal model and analysis methods for AMS circuits as well as methods to automatically generate abstract models from common AMS modeling languages. Our analysis procedure uses difference bound matrices (DBMs), a restricted form of convex polygons, to represent the continuous state space of the model. Reachability analysis using DBMs provides very efficient analysis without a significant loss in accuracy. We demonstrate these methods on a case study of several AMS circuits from both academia and industry. The formal verification methods demonstrate the ability to find bugs missed by standard simulations. The abstract modeling methods show the promise of using automatically generated abstract models by demonstrating up to 40x speedup for some examples.


Scott R. Little received the B.S. degree in computer engineering in 2003 from the University of Utah, Salt Lake City, UT. He is currently an SRC Fellow working toward a Ph.D. in computer science at the University of Utah. His current research interests include formal and semi-formal verification of embedded systems and analog/mixed-signal circuits.