research-article

A verification system for transient response of analog circuits

Authors:

Tathagato Rai Dastidar,

P. P. ChakrabartiAuthors Info & Claims

ACM Transactions on Design Automation of Electronic Systems (TODAES), Volume 12, Issue 3

Article No.: 31, Pages 1 - 39

https://doi.org/10.1145/1255456.1255468

Published: 22 May 2008 Publication History

Abstract

We present a method for application of formal techniques like model checking and equivalence checking for validation of the transient response of nonlinear analog circuits. We propose a temporal logic called Ana CTL (computational tree logic for analog circuit verification) which is suitable for specifying properties specific to analog circuits. The application of Ana CTL for validation of transient behavior of arbitrarily nonlinear analog circuits is presented. The transient response of a circuit under all possible input waveforms is represented as a finite state machine (FSM), by bounding and discretizing the continuous state space of an analog circuit. We have developed algorithms to run Ana CTL queries on this discretized model using search-based methods which reduce the runtime considerably by avoiding creation of the whole FSM. The application of these methods on several real-life analog circuits is presented and we show that this system is a useful aid for detecting and debugging early design errors.

We also present methods for checking the equivalence of transient response of two analog circuits. The behavior of two different analog circuits can rarely be exactly similar. Hence, we introduce a notion of approximate equivalence. A query language for checking different notions of user-definable approximate equivalence is presented which extends the syntax of the Ana CTL model checking language. In its extended form, Ana CTL can be used combining model checking with equivalence checking.

References

[1]

Accellera. 2004. Verilog AMS. http://www.eda.org/verilog-ams/.

[2]

Allen, P. E. and Holberg, D. R. 1987. CMOS Analog Circuit Design. Oxford University Press.

[3]

Alur, R. and Wang, B.-Y. 1999. Next heuristic for on-the-fly model checking. In Proceedings of the 10th International Conference on Concurrency Theory (CONCUR). 98--113.

Digital Library

[4]

Alur, R., Henzinger, T. A., and Ho, P.-H. 1996. Automatic symbolic verification of embedded systems. IEEE Trans. Softw. Eng. 22, 181--201.

Digital Library

[5]

Alur, R. and Dill, D. L. 1994. A theory of timed automata. Theor. Comput. Sci. 126, 183--235.

Digital Library

[6]

Analog Insydes. 2007. Analog Insydes version 2.1. http://www.analog-inydes.de/.

[7]

Balivada, A., Hoskote, Y., and Abraham, J. A. 1995. Verification of transient response of linear analog circuits. In Proceedings of the 13th IEEE VLSI Test Symposium (VTC). 42--47.

Digital Library

[8]

Banerjee, A. and Dasgupta, P. 2005. The open family of temporal logics: Annotating temporal operators with input constraints. ACM Trans. Des. Autom. Electron. Syst. 10, 3 (Jul.), 492--522.

Digital Library

[9]

Behrmann, G., Larsen, K. G., Moller, O., David, A., and Petterson, P. 2001. UPPAL---Present and future. In Proceedings of the 40th IEEE Conference on Decision and Control. 2881--2886.

[10]

Biere, A., Cimatti, A., Clarke, E., and Zhu, Y. 1999. Symbolic model checking without BDDs. In Proceedings of the Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Springer, 193--207.

Digital Library

[11]

Burch, J. R., Clarke, E. M., Long, D. E., Mcmillan, K. L., and Dill, D. L. 1994. Symbolic model checking for sequential circuit verification. IEEE Trans. Comput. Aided Des. Integr. Circ. Syst. 13, 4 (Apr.), 401--424.

Digital Library

[12]

Chutinan, A. and Krogh, B. H. 2003. Computational techniques for hybrid system verification. IEEE Trans. Autom. Control 48, 1, 64--75.

[13]

Clarke, E. M. Jr., Grumberg, O., and Peled, D. A. 2000. Model Checking. MIT Press, Cambridge, MA.

[14]

Cormen, T. H., Leiserson, C. E., and Rivest, R. E. 1990. Introduction to Algorithms. MIT Press, Cambridge, MA.

Digital Library

[15]

Dang, T. and Maler, O. 2000. d/dt: Reachability analysis of continuous and hybrid systems. http://www-verimag.imag.fr/~tdang/ddt.html.

[16]

Dang, T., Donze, A., and Maler, O. 2004. Verification of analog and mixed-signal circuits using hybrid systems techniques. In Proceedings of the International Conference on Formal Methods in Computer-Aided Design (FMCAD) (Nov.).

[17]

Dasgupta, P., Chakrabarti, A., and Chakrabarti, P. P. 2002. Open computation tree logic for formal verification of modules. In Proceedings of the Asia and South Pacific Design Automation Conference (ASP-DAC). 735--740.

Digital Library

[18]

Dastidar, T. R. and Chakrabarti, P. P. 2005. A verification system for transient response of analog circuits using model checking. In Proceedings of the 18th International Conference on VLSI Design. 195--200.

Digital Library

[19]

Frehse, G., Krogh, B. H., and Rutenbar, R. A. 2006. Verifying analog oscillator circuits using forward/backward abstraction refinement. In Proceedings of the Conference and Exhibtion on Design, Automation and Test in Europe (DATE). 257--262.

Digital Library

[20]

Ghosh, A. and Vemuri, R. 1999. Formal verification of synthesized analog circuits. In Proceedings of the ACM/IEEE International Conference on Computer Design. 40--45.

Digital Library

[21]

Gupta, S., Krogh, B. H., and Rutenbar, R. A. 2004. Towards formal verification of analog designs. In Proceedings of the IEEE International Conference on Computer-Aided Design (ICCAD). 210--217.

Digital Library

[22]

Hartong, W., Hedrich, L., and Barke, E. 2002a. Model checking algorithms for analog verification. In Proceedings of the IEEE/ACM Design Automation Conference (DAC). 542--547.

Digital Library

[23]

Hartong, W., Hedrich, L., and Barke, E. 2002b. On discrete modeling and model checking for nonlinear analog systems. In Proceedings of the 14th International Conference on Computer-Aided Verification. 401--413.

Digital Library

[24]

Hennig, E. 2000. Symbolic Approximation and Modeling Techniques for Analysis and Design of Analog Circuits. Shaker, Aachen, Germany.

[25]

McCalla, W. J. 1988. Fundamentals of Computer-Aided Circuits Simulation. Kluwer Academic, Hingham, MA.

Digital Library

[26]

NuSMV. 2007. NuSMV: A new symbolic model checker. http://nusmv.irst.itc.it/.

[27]

PHAVer. 2006. PHAVer: Polyhedral hybrid automaton verifyer. http://www.cs.ru.nl/~goranf/.

[28]

Quarles, T., Pederson, D., Newton, R., Sangiovanni-Vincentelli, A., and Wayne, C. 2007. The Spice page. http://bwrc.eecs.berkeley.edu/Classes/IcBook/SPICE.

[29]

Quarles, T. L. 1989. The Spice3 implementation guide. Memorandum no. UCB/ERL M89/44, College of Engineering, University of California at Berkeley, Berkeley, CA.

[30]

Santone, A. 2003. Heuristic search + local model checking in selective mu-calculus. IEEE Trans. Softw. Eng. 29, 6 (Jun.).

Digital Library

[31]

Silva, B. I., Stursberg, O., Krogh, B. H., and Engell, S. 2001. An assessment of the current status of algorithmic approaches to the verification of hybrid systems. In Proceedings of the 40th IEEE Conference on Decision and Control. 2867--2874.

[32]

Tan, S. X.-D. and Shi, C.-J. R. 2001. Compact representation and efficient generation of s-expanded symbolic network functions for computer-aided analog circuit design. IEEE Trans. Comput. Aided Des. Integr. Circ. Syst. 20, 7 (Jul.), 813--827.

Cited By

Lei JChatterjee A(2022)ML-Assisted Bug Emulation Experiments for Post-Silicon Multi-Debug of AMS Circuits2022 IEEE International Test Conference (ITC)10.1109/ITC50671.2022.00035(268-277)Online publication date: Sep-2022
https://doi.org/10.1109/ITC50671.2022.00035
Fürtig AHedrich L(2017)Formal Techniques for Verification and Coverage Analysis of Analog SystemsFormal System Verification10.1007/978-3-319-57685-5_1(1-35)Online publication date: 22-Jun-2017
https://doi.org/10.1007/978-3-319-57685-5_1
Ain ABruto da Costa ADasgupta P(2016)Feature Indented Assertions for Analog and Mixed-Signal ValidationIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2016.252579835:11(1928-1941)Online publication date: 1-Nov-2016
https://dl.acm.org/doi/10.1109/TCAD.2016.2525798
Show More Cited By

Index Terms

A verification system for transient response of analog circuits
1. Hardware
  1. Hardware validation
    1. Functional verification

Recommendations

A Verification System for Transient Response of Analog Circuits Using Model Checking
VLSID '05: Proceedings of the 18th International Conference on VLSI Design held jointly with 4th International Conference on Embedded Systems Design

Conventional temporal logics like CTL, [1], used for specifying properties of digital systems are not well suited for property specification of analog systems. We present a new temporal logic for specifying properties of analog circuits. We call this ...
Verification of transient response of linear analog circuits
VTS '95: Proceedings of the 13th IEEE VLSI Test Symposium

Abstract: With the introduction of complex analog designs the need to verify the circuit behavior completely and efficiently cannot be overemphasized. Recognizing the limitation of circuit simulation to achieve this goal, we present a novel approach ...
Advanced methods for equivalence checking of analog circuits with strong nonlinearities

In this contribution two extensions for an analog equivalence checking method are proposed, enabling the checking of strongly nonlinear circuits with floating nodes such as digital library cells. Therefore, a structural recognition and mapping of ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Design Automation of Electronic Systems

ACM Transactions on Design Automation of Electronic Systems Volume 12, Issue 3

August 2007

427 pages

ISSN:1084-4309

EISSN:1557-7309

DOI:10.1145/1255456

Issue’s Table of Contents

Copyright © 2008 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Journal Family

ACM Journals for the Design of Smart and Connected Systems

Publication History

Published: 22 May 2008

Accepted: 01 January 2007

Revised: 01 July 2006

Received: 01 September 2005

Published in TODAES Volume 12, Issue 3

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

14
Total Citations
View Citations
449
Total Downloads

Downloads (Last 12 months)8
Downloads (Last 6 weeks)0

Reflects downloads up to 12 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Lei JChatterjee A(2022)ML-Assisted Bug Emulation Experiments for Post-Silicon Multi-Debug of AMS Circuits2022 IEEE International Test Conference (ITC)10.1109/ITC50671.2022.00035(268-277)Online publication date: Sep-2022
https://doi.org/10.1109/ITC50671.2022.00035
Fürtig AHedrich L(2017)Formal Techniques for Verification and Coverage Analysis of Analog SystemsFormal System Verification10.1007/978-3-319-57685-5_1(1-35)Online publication date: 22-Jun-2017
https://doi.org/10.1007/978-3-319-57685-5_1
Ain ABruto da Costa ADasgupta P(2016)Feature Indented Assertions for Analog and Mixed-Signal ValidationIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2016.252579835:11(1928-1941)Online publication date: 1-Nov-2016
https://dl.acm.org/doi/10.1109/TCAD.2016.2525798
Jiao FDoboli A(2016)Causal reasoning mining approach to analog circuit verificationIntegration, the VLSI Journal10.1016/j.vlsi.2016.04.00255:C(376-383)Online publication date: 1-Sep-2016
https://dl.acm.org/doi/10.1016/j.vlsi.2016.04.002
Ahmadyan SKumar JVasudevan SMacii E(2013)Runtime verification of nonlinear analog circuits using incremental time-augmented RRT algorithmProceedings of the Conference on Design, Automation and Test in Europe10.5555/2485288.2485296(21-26)Online publication date: 18-Mar-2013
https://dl.acm.org/doi/10.5555/2485288.2485296
Steinhorst SHedrich LHu A(2012)Trajectory-directed discrete state space modeling for formal verification of nonlinear analog circuitsProceedings of the International Conference on Computer-Aided Design10.1145/2429384.2429423(202-209)Online publication date: 5-Nov-2012
https://dl.acm.org/doi/10.1145/2429384.2429423
Mukherjee SDasgupta PMukhopadhyay SLittle SHavlicek JChandrasekaran S(2012)Synchronizing AMS Assertions with AMS SimulationACM Transactions on Design Automation of Electronic Systems10.1145/2348839.234884217:4(1-25)Online publication date: 1-Oct-2012
https://dl.acm.org/doi/10.1145/2348839.2348842
Steinhorst SHedrich L(2012)Equivalence checking of nonlinear analog circuits for hierarchical AMS System Verification2012 IEEE/IFIP 20th International Conference on VLSI and System-on-Chip (VLSI-SoC)10.1109/VLSI-SoC.2012.7332090(135-140)Online publication date: Oct-2012
https://doi.org/10.1109/VLSI-SoC.2012.7332090
Steinhorst SHedrich L(2012)Equivalence checking of nonlinear analog circuits for hierarchical AMS System Verification2012 IEEE/IFIP 20th International Conference on VLSI and System-on-Chip (VLSI-SoC)10.1109/VLSI-SoC.2012.6379019(135-140)Online publication date: Oct-2012
https://doi.org/10.1109/VLSI-SoC.2012.6379019
Steinhorst SHedrich L(2011)Formal Methods for Verification of Analog CircuitsSimulation and Verification of Electronic and Biological Systems10.1007/978-94-007-0149-6_9(173-192)Online publication date: 2011
https://doi.org/10.1007/978-94-007-0149-6_9
Show More Cited By

View Options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents