Collaborative Research: Integrated Verification, Built-in Self-Test and Tuning for Digitally-Intensive Analog Systems PIs: Peng Li (Texas A&M), Chris J. Myers (University of Utah) Sponsor: National Science Foundation (NSF) Directorate for Computer & Information Science & Engineering (CSE) Division of Computer and Communication Foundations (CCF) NSF Award #: 1117660 (TAMU) / 1117515 (Utah) Duration: August 1, 2011 – July 31, 2015

[Participants] [Overview] [Research Highlights] [Publications] [Software]

Principle investigators:

Prof. Peng Li (TAMU), Prof. Chris J. Myers (Utah)

Students:

Yingyezhe Jin, Ph. D. (TAMU)

Honghuang Lin, Ph.D. (TAMU)

Myung Seok Shim, Ph.D. (TAMU)

Qian Wang, Ph. D. (TAMU)

Ya Wang, Ph. D. (TAMU)

Alumni:

Leyi Yin, Ph.D. graduated in June, 2012 (TAMU), now with Cirrus Logic, Austin, Texas

Yue Deng, M.S., graduated in May, 2012 (TAMU), now with Zipalog, Plano, Texas

Dhanashree Kulkarni, M.S., graduated in 2013 (Utah), now with Intel Corporation, Hillsboro, Oregon

Parijat Mukherjee, Ph.D., graduated in December 2014 (TAMU), now with the Intel Strategic CAD Lab, Hillsboro, Oregon

Andrew Fisher, Ph.D., graduated in May 2015 (Utah), now with Sandia National Laboratories.

Designing analog integrated circuits is more of an art than a science. Their continuous nature makes them difficult to both verify to be correct before fabrication as well as difficult to test to be free of faults after fabrication. This fact leads to design errors forcing costly re-spins (repetitions of the design and fabrication process) and even worse faulty parts being shipped to customers. In an attempt to address this problem, engineers are exploring the use of digitally-intensive analog circuits. In these circuits, designers use the simpler 0-1 binary digital assumption for the majority of the implementation, and they only use analog components when absolutely essentially. While this has some advantages, it creates new challenges as traditional verification and test methodologies for digital and analog design are extremely different. The project is attempting to address these challenges. In particular, the project is exploring the integration of both design-time verification as well as new built-in self-test and tuning techniques. This integration will allow not only joint enhancement of design correctness and robustness, hence a holistic guarantee of design quality, but also verification of self healing analog systems with built-in digitally-assisted test and tuning.

The broader impact of this work is that it will enable the design of nanoscale robust computing systems vital to a wide range of applications. Also, interdisciplinary explorations will provide new opportunities for solving research problems of practical significance and offer educational opportunities to make students well grounded in both theory and application. The PIs will promote the research participation from undergraduate students and students from underrepresented groups. The research outcomes of this work will be integrated into undergraduate and graduate curriculum and widely disseminated in the research community. The developed software computer-aided design tools will be released in the public domain.

Some of our recent activities have been placed on the following key aspects:

1)    Our functional analog/mixed-signal circuit testing work allows us to maximize the probability of observing post-silicon failures even when dealing with limited measurement budgets and large circuits with highly non-linear dynamics. More importantly, it does so in a manner that ensures we aren’t testing around a single failure mechanism. This work will be presented at the FAC Workshop in November 2015.

2)    Our SVM based performance modeling technique has been demonstrated to be rather efficient for a number of analog-like circuit examples. Our IEEE TCAD paper on this topic has been published.

3)     Publication of a new theory for piecewise linear analysis of ranges of rates for continuous variables that eliminates false positives from our zone-based model checker at the 7th Nasa Symposium on Formal Methods.

4)     New model checking algorithm for AMS circuits that uses octagons to improve the accuracy and reduce the chances of false negative results.  This work was implemented in our LEMA tool and described in Andrew Fisher's PhD dissertation.

5)    A new workflow for mixed asynchronous/analog circuit optimization.  This workflow is leveraging formal verification to find timing information that can be leveraged to reduce the asynchronous logic complexity.

Dissertations

Andrew Fisher, “Efficient, Sound Formal Verification for Analog/Mixed-Signal Circuits,” Ph. D. dissertation, University of Utah, May 2015.

Parijat Mukherjee, “Detection and Diagnosis of Out-of-Specification Failures in Mixed-Signal Circuits”, Ph. D. dissertation, Texas A&M University, December 2014.

Dhanashree Kulkarni, “Formal verification of digitally-intensive analog/mixed-signal circuits,” M.S. thesis, University of Utah, 2013.

Leyi Yin, “Formal verification and in-situ test of analog and mixed-signal circuits,” Ph.D. dissertation, Dept. of Electrical and Computer Engineering, Texas A&M University, December 2012.

Yue Deng, “SAT-based Verification for Analog and Mixed-Signal Circuits”, M.S. dissertation, Dept. of Electrical and Computer Engineering, Texas A&M University, May 2012.

Amandeep Singh, “Behavioral model equivalence checking for large analog/mixed signal systems”, M.S. dissertation, Dept. of Electrical and Computer Engineering, Texas A&M University, May 2011.

Book Chapters

A. Fisher, D. Kulkarni, and C. Myers (2015). A new assertion property language for analog/mixed- signal circuits. Languages, Design Methods, and Tools for Electronic System Design - Selected Contributions from FDL 2013.

Journals

Honghuang Lin and Peng Li, “Circuit performance classification with active learning guided sampling for support vector machines,” in IEEE Trans. on Computer-Aided Design of Integrated Circuits and Systems (in press), 2015.

Leyi Yin, Yue Deng and Peng Li, “Simulation-Assisted Formal Verification of Nonlinear Mixed-Signal Circuits with Bayesian Inference Guidance,” IEEE Trans. on Computer-Aided Design of Integrated Circuits and Systems, pp. 977-990, July 2013.

S. Little, D. Walter, C. Myers, R. Thacker, S. Batchu, and T. Yoneda, “Verification of analog/mixed-signal circuits using labeled hybrid Petri nets,'” in IEEE Transactions on CAD, 30(4): 617-630, April, 2011.

S. Little, D. Walter, K. Jones, C. Myers, and A. Sen, “Analog/mixed-signal circuit verification using models generated from simulation traces,” in The International Journal of Foundations of Computer Science, 21(2): 191-210, 2010.

Guo Yu and Peng Li, “Exploring circuit adaptation for yield optimization of low-power all-digital PLLs,” Journal of Low Power Electronics, vol. 6, no. 1, Apr. 2010.

D. Walter, S. Little, C. Myers, N. Seegmiller, and T. Yoneda, “Verification of analog/mixed-signal circuits using symbolic methods,” in IEEE Transactions on CAD}, 27(12): 2223-2235, December, 2008.

Conference Proceedings and Workshops

P. Mukherjee and P. Li, “Functional testing of large mixed-signal circuits with non-linear dynamics using pre-silicon knowledge,” FAC Workshop, Nov.  2015.

V. Dubikhin, A. Fisher, D. Sokolov, C. Myers, A. Yakovlev, “A Workflow for the Design of Mixed-signal Systems with Asynchronous Control,”  FAC Workshop, Nov.  2015.

A. Fisher, C. Myers, P. Li,  “Reachability analysis using extremal rates,” 7th Nasa Formal Methods Symposium. Pasadena, CA, 2015.

A. Fisher, S. Batchu, K. Jones, D. Kulkarni, S. Little, D. Walter, and C. Myers, “LEMA: a tool for the formal verification of digitally-intensive analog/mixed-signal circuits,”  Midwest Symposium on Circuits and Systems, August, 2014.

Parijat Mukherjee, Chirayu Amin and Peng Li, “Approximate property checking of mixed-signal circuits,” in Proc. of IEEE/ACM Design Automation Conference, pp. 1-6, June 2014  and also in Proc. of ACM Int. Workshop on Timing Issues in the Specification and Synthesis of Digital Systems, March 2014.

Honghuang Lin and Peng Li, “Parallel hierarchical reachability analysis for analog verification,” in Proc. of IEEE/ACM Design Automation Conference, pp. 1-6, June 2014.

Parijat Mukherjee and Peng Li, “Leveraging pre-silicon data to diagnose out-of-specification failures in mixed-signal circuits,” in Proc. of IEEE/ACM Design Automation Conference, pp. 1-6, June 2014.

D. Kulkarni, A. Fisher, and C. Myers, “A new assertion property language for analog/mixed-signal circuits,'” Forum on Design Languages, September 2013 (best paper candidate).

Honghuang Lin, Peng Li, and Chris J. Myers, “Verification of digitally-intensive analog circuits via kernel ridge regression and hybrid reachability analysis,” IEEE/ACM Design Automation Conference, June 2013, Austin, TX.

Parijat Mukherjee, Chirayu Amin and Peng Li, “A formal approach to DC operating point analysis for large mixed signal circuits: challenges and opportunities,” in Proc. of ACM Int. Workshop on Timing Issues in the Specification and Synthesis of Digital Systems, March 2013.

Dhanashree Kulkarni, Andrew Fisher, Chris J. Myers, “A New Assertion Property Language for Analog/Mixed-Signal Circuits,” Frontiers in Analog CAD, Feb. 2013, Berkeley, CA.

Leyi Yin, Yue Deng and Peng Li, “Verifying dynamic properties of nonlinear mixed-signal circuits via efficient SMT-based techniques,” IEEE/ACM Conf. on Computer-Aided Design, pp. 436-442, November 2012.

Honghuang Lin and Peng Li, “Classifying circuit Performance using active-learning guided support vector machines,” IEEE/ACM Conf. on Computer-Aided Design, pp. 187-194, November 2012.

D. Kulkarni, S. Batchu, and C. Myers, “Improved model generation of AMS circuits for formal verification,'' in 2011 Virtual Worldwide Forum for PhD Researchers in Electronic Design Automation, November, 2011.

Leyi Yin and Peng Li, “RF BIST for ADPLL-based polar transmitters with wide-band DCO gain calibration,” in Proc. of IEEE Int. Symp. on Quality Electronic Design, pp. 303-340, March 2011.

Amandeep Singh and Peng Li, “On behavioral model equivalence checking for large analog/mixed signal systems,” in Proc. of IEEE/ACM Int. Conf. on Computer-Aided Design, pp. 55-61, November 2010.

Leyi Yin and Peng Li, “In-situ jitter test and diagnosis of digital PLLs using digital reconfiguration,” SRC TECHCON, 4 pages, September 2010.

Leyi Yin and Peng Li, “Exploiting reconfigurability for low-cost in-situ test and monitoring of digital PLLs,” in Proc. of ACM/IEEE Design Automation Conf., pp. 929-934, June 2010.

S. Little and C. Myers, “Abstract modeling and simulation aided verification of analog/mixed-signal circuits,'' in Workshop on Formal Verification of Analog Circuits, July, 2008.

S. Little, A. Sen, and C. Myers, “Application of automated model generation techniques to analog/mixed-signal circuits,'' in 8th International Workshop on Microprocessor Test and Verification, December, 2007.

S. Little, D. Walter, K. Jones, and C. Myers, “Analog/mixed-signal circuit verification using models generated from simulation traces,'' in Automated Technology for Verification and Analysis, October, 2007.

D. Walter, S. Little, and C. Myers, “Bounded model checking of analog and mixed-signal circuits using an SMT solver,'' in Automated Tech. for Verif. and Analysis,  October, 2007.

Guo Yu and Peng Li, “A methodology for systematic built-in self-test of phase-locked loops targeting at parametric failures,” pp. 1-10, in Proc. of IEEE Int. Test Conference, October 2007.

D. Walter, S. Little, N. Seegmiller, C. Myers, and T. Yoneda, “Symbolic model checking of analog/mixed-signal circuits'', in Asia and South Pacific Design Automation Conference 2007, January, 2007.

S. Little, N. Seegmiller, D. Walter, C. Myers, and T. Yoneda, Verification of analog/mixed-signal circuits using labeled hybrid Petri nets'', in {\em 2006 International Conference on Computer-Aided Design}, November, 2006.}

C. Myers, R. Harrison, D. Walter, N. Seegmiller, and S. Little, `”The case for analog circuit verification,'' in Workshop on Formal Verification of Analog Circuits, April, 2005.

S. Little, D. Walter, N. Seegmiller, C. Myers, and T. Yoneda, “Verification of analog and mixed-signal circuits using timed hybrid Petri nets,'' in Automated Technology for Verification and Analysis, pages 426-440, November, 2004.

 Acknowledgement and Disclaimer

This material is based upon work supported by the National Science Foundation under Grants No. 1117660 and No. 1117515.

Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the National Science Foundation.

 Copyright by Peng Li and Chris J. Myers.