Skip to main content
SpringerLink
Log in

Approaches to Formal Verification of Analog Circuits

  • Chapter
Low-Power Design Techniques and CAD Tools for Analog and RF Integrated Circuits

8.5 Conclusions

In this chapter, algorithms for formal verification of analog systems circuits are presented. The algorithms compare two system descriptions on different levels of abstraction. They prove/disprove, that the systems have functionally similar inputoutput behavior. Additionally, in case of nonlinear dynamic circuits, an algorithm for generating transient stimuli is outlined to help the designer finding the design flaws with well known transient simulations. Some examples show the feasibility of the approaches.

All methods try to prove in a more or less graphical way the similarity of two system descriptions. Due to the large effort to do a mathematical proof, it is currently not possible to handle nonlinear dynamic circuits with tolerances. An other important step in the development of the formal verification methodology could be to restrict the proof to special properties of a system. For example: to prove that the gain of a system is always greater than a given value. This could be understood as model checking for analog circuits.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 129.00
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 169.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 169.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Mentor Graphics: http://www.mentor.com/formalpro/

  2. Verplex Systems: http://www.verplex.com/product.html

  3. Avant! Corporation: http://www.avanticorp.com/product/1,1172,50,00.html

  4. P. Nussbaum, M. Hinners, L. Menevaut, “SimBoy: An Analog Simulator Interface for Automated Datasheet Generation”, Proceedings of the European Design Automation Conference, pp. 37–41, Nov 1994.

    Google Scholar 

  5. St. W. Director, P. Feldmann, K. Krishna, “Optimization of Parametric Yield: A Tutorial”, Proceedings of the Custom Integrated Circuits Conference, pp. 3.1.1–3.1.8, Jan 1992.

    Google Scholar 

  6. K. J. Antreich, H. E. Graeb, C. U. Wieser, “Circuit Analysis and Optimization Driven by Worst-Case Distances”, IEEE Transactions on Computer-Aided Design, Vol. 13,No. 1, pp. 57–71, Jan 1994.

    Article  Google Scholar 

  7. Th. A. Henzinger, P.-H. Ho, “Algorithmic Analysis of Nonlinear Hybrid Systems”, International Conference on Computer Aided Verification, pp. 225–238, June 1995.

    Google Scholar 

  8. A. Puri, P. Varaiya, “Decidability of Hybrid Systems with Rectangular Differential Inclusions”, International Conference on Computer Aided Verification, pp. 95–104, June 1994.

    Google Scholar 

  9. St.W. Director, P. Feldmann, K. Krishna, “Optimization of Parametric Yield: A Tutorial”, Proc. Custom Integrated Circuits Conference, pp. 3.1.1–3.1.8, 1992.

    Google Scholar 

  10. A. Dharchoudhury, S.M. Kang, “Worst-Case Analysis and Optimization of VLSI Circuit Performances”, IEEE Trans. on Computer-Aided Design, Vol. 14,No. 4, pp 481–192, 1993.

    Google Scholar 

  11. K.J. Antreich, H.E. Graeb, C.U. Wieser, “Circuit Analysis and Optimization Driven by Worst-Case Distances”, IEEE Trans. on Computer-Aided Design, Vol. 13,No. 1, pp. 57–71, 1994.

    Google Scholar 

  12. G.E. Mller-L., “Limit Parameters: The General Solution of the Worst-Case Problem of the Linearized Case”, IEEE Intern. Symp. on Circuits and Systems, Vol. 3, pp. 2256–2259, 1990.

    Google Scholar 

  13. St.W. Director, G.D. Hachtel, “The Simplical Approximation Approach to Design Centering”, IEEE Trans. on Circuits and Systems, Vol. 24,No. 7, pp. 363–372, 1977.

    Article  MathSciNet  Google Scholar 

  14. A. Levkovich, E. Zeheb, N. Cohen, “Frequency Response Envelopes of a Family of Uncertain Continuous-Time Systems”, IEEE Trans. on Circuits and Systems, Vol. 42,No. 3, pp. 156–16, May 1995.

    MathSciNet  Google Scholar 

  15. S.P. Bhattacharyya, H. Chapellat, L.H. Keel, “Robust Control: The Parametric Approach”, Prentice Hall, London, 1995.

    Google Scholar 

  16. P.-O. Gutman; C. Baril, L. Neumann, “An Algorithm for Computing Value Sets of Uncertain Transfer Functions in Factored Real Form”, IEEE Trans. on Automatic Control, Vol. 39,No. 6, pp. 1269–73, 1994.

    Article  MathSciNet  Google Scholar 

  17. G. Gielen, W. Sansen, “Symbolic Analysis for Automated Design of Analog Integrated Circuits”, Kluwer Academic Publishers, Boston, 1991.

    Google Scholar 

  18. R.E. Moore, “Interval analysis”, Prentice Hall, Englewood Cliffs, 1966.

    Google Scholar 

  19. G. Alefeld, J. Herzberger, “Introduction to interval computations”, Academic Press, New York, 1983.

    Google Scholar 

  20. E.P. Oppenheimer, A.N. Michel, “Application of Interval Analysis Techniques to Linear Systems: Part I-III”, IEEE Trans. on Circuits and Systems, Vol. 35,No. 9–10, 1988.

    Google Scholar 

  21. E.G. Eszter, R.S. Sanchez Pena, “Value set boundary computation of uncertainty structures”, Proc. of the American Control Conference, pp. 2210–13, 1992.

    Google Scholar 

  22. J. O’Rourke, “Computational Geometry in C”, Cambridge University Press, New York, 1993.

    Google Scholar 

  23. D. Python, Ch. C. Enz, “An Antialiasing Filter Using Complementary MOS Transconductors Biased in the Tiode Region” Deliverable 5.2.5, ESD-LPD Project “Alpins”, Proc. IEEE Int. Symp. Circuits Syst., Vol. 2, pp. 184–187, June 1999.

    Google Scholar 

  24. D. Python, Ch. C. Enz, “A 40μW,75dB Dynamic Range, 70kHz Bandwidth Biquad based on complementary MOS Transconductors” Deliverable 5.2.6, ESD-LPD Project “Alpins”, Proc. European Solid-State Circuits Conference in Duisburg, Sept. 1999.

    Google Scholar 

  25. R. Krawczyk, “Interval Iteration for Including a Set of Solutions”, Computing 32, pp. 13–31, 1984.

    Article  MATH  MathSciNet  Google Scholar 

  26. R. Krawczyk, A. Neumaier, “Interval Newton operators for Function Strips”, Journal of Mathematical Analysis and Applications, No. 124, pp. 52–72, 1987.

    Article  MathSciNet  Google Scholar 

  27. R Krawczyk, “Properties of Interval Operators”, Computing 37, pp.227–245, 1986.

    MATH  MathSciNet  Google Scholar 

  28. D. Oelschlgel, “Intervallmathematische Lösung nichtlinearer Gleichungssysteme”, Wissenschaftliche Zeitschrift TH Leuna-Merseburg 26, PP.298–307, 1984 in German.

    Google Scholar 

  29. L. Hedrich, E. Barke, “A Formal Approach to Nonlinear Analog Circuit Verification”, International Conference on Computer-Aided Design, pp. 123–127, Nov 1995.

    Google Scholar 

  30. F. H. Bursal, B. H. Tongue, “A New Method of Nonlinear System Identification Using Interpolated Cell Mapping”, Proc. of the American Control Conf., Vol. 4, pp. 3160–4, Jan 1992.

    Google Scholar 

  31. S. Natarajan, “A systematic method for obtaining state equations using MNA”, IEE Proceedings-G, Vol. 138,No. 3, pp. 341–345, Mar 1991.

    MathSciNet  Google Scholar 

  32. L. Fortuna, G. Nunnari and A. Gallo, “Model Order Reduction Techniques with Applications in Electrical Engineering”, Springer-Verlag London, 1992.

    Google Scholar 

  33. P. Feldmann, R.W. Freund, “Efficient Linear Circuits Analysis by Pade Approximation via the Lanczos Process”, IEEE Transactions on Computer Aided Design, Vol. 14,No. 5, pp. 639–649, May 1995.

    Google Scholar 

  34. P.E. Gill, W. Murray, M.H. Wright, “Practical Optimization”, Academic Press Inc, London, 1981.

    Google Scholar 

  35. M. Punzenberger, C. Enz, “A 1.2-V Low-Power BiCMOS Class AB Log-Domain Filter”, IEEE Journal of Solid-State Circuits, Vol. 32,No. 12, 1997.

    Google Scholar 

  36. M. Punzenberger, C. Enz, “A Compact Low-Power BiCMOS Log-Domain Filter”, IEEE Journal of Solid-State Circuits, Vol. 33,No. 7, 1998.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute of Microelectronic Circuits and Systems, University of Hannover, Germany

    Lars Hedrich & Walter Hartong

Authors
  1. Lars Hedrich
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Walter Hartong
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. IMEC, Belgium

    Piet Wambacq

  2. Katholieke Universiteit Leuven, Belgium

    Georges Gielen

  3. CSEM System Engineering, Switzerland

    John Gerrits

  4. TU Delft/DIMES, Delft, The Netherlands

    Rene van Leuken , Alexander de Graaf  & Reinder Nouta ,  & 

Rights and permissions

Reprints and permissions

Copyright information

© 2001 Kluwer Academic Publishers

About this chapter

Cite this chapter

Hedrich, L., Hartong, W. (2001). Approaches to Formal Verification of Analog Circuits. In: Wambacq, P., Gielen, G., Gerrits, J., van Leuken, R., de Graaf, A., Nouta, R. (eds) Low-Power Design Techniques and CAD Tools for Analog and RF Integrated Circuits. Springer, Boston, MA. https://doi.org/10.1007/0-306-48089-1_8

Download citation

  • DOI: https://doi.org/10.1007/0-306-48089-1_8

  • Publisher Name: Springer, Boston, MA

  • Print ISBN: 978-0-7923-7432-9

  • Online ISBN: 978-0-306-48089-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation