Skip to main content
SpringerLink
Log in

Framework for Formally Verifying Analog and Mixed-Signal Designs

  • Chapter
  • First Online:
Computational Intelligence in Analog and Mixed-Signal (AMS) and Radio-Frequency (RF) Circuit Design

Abstract

This chapter proposes a complementary formal-based solution to the verification of analog and mixed-signal (AMS) designs. The authors use symbolic computation to model and verify AMS designs through the application of induction-based model checking. They also propose the use of higher order logic theorem proving to formally verify continuous models of analog circuits. To test and validate the proposed approaches, they developed prototype implementations in Mathematica and HOL and target analog and mixed-signal systems such as delta-sigma modulators.

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 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Hardcover Book
USD 54.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

References

  1. Gielen, G.G., Rutenbar, R.A.: Computer-aided design of analog and mixed-signal integrated circuits. Proc. IEEE 88(12), 1825–1852 (2000)

    Article  Google Scholar 

  2. Shi, G., Tan, S.X.-D., Tlelo-Cuautle, E.: Advanced Symbolic Analysis for VLSI Systems. Springer, Berlin (2014) (ISBN 978-1-4939-1102-8)

    Google Scholar 

  3. Fakhfakh, M., Tlelo-Cuautle, E., Fernandez, F.V.: Design of Analog Circuits through Symbolic Analysis, 491 pages. Bentham Sciences Publishers Ltd., Sharjah (2012) (ISBN: 978-1-60805-425-1)

    Google Scholar 

  4. Johns, D., Martin, K.: Analog Integrated Circuit Design. Wiley, New York City (1997)

    Google Scholar 

  5. Biere, A., Cimatti, A., Clarke, E., Strichman, O., Zhu, Y.: Bounded model checking. Adv. Comput. 58, 118–149 (2003)

    Google Scholar 

  6. Moore, R.E.: Methods and Applications of Interval Analysis. Society for Industrial and Applied Mathematics, Philadelphia (1979)

    Google Scholar 

  7. Zaki, M.H., Tahar, S., Bois, G.: Formal verification of analog and mixed signal designs: a survey. Microelectron. J. 39(12):1395–1404 (2008)

    Google Scholar 

  8. Kurshan, R.P., McMillan, K.L.: Analysis of digital circuits through symbolic reduction. IEEE Trans. Comput. Aided Des. 10(11), 1356–1371 (1991)

    Article  Google Scholar 

  9. Hartong, W., Klausen, R., Hedrich, L.: Formal verification for nonlinear analog systems: approaches to model and equivalence checking. In: Advanced Formal Verification, pp. 205–245. Kluwer, The Netherlands (2004)

    Google Scholar 

  10. Greenstreet, M.R., Mitchell, I.: Reachability analysis using polygonal projections. In: Hybrid Systems: Computation and Control, LNCS, vol. 1569, pp. 103–116, Springer, Berlin (1999)

    Google Scholar 

  11. Yan, C., Greenstreet, M.R.: Verifying an arbiter circuit. IEEE Form. Methods Comput. Aided Des. 1–9 (2008)

    Google Scholar 

  12. Zaki, M.H., Al Sammane, G., Tahar, S., Bois, G.: Combining symbolic simulation and interval arithmetic for the verification of AMS designs. IEEE Form. Methods Comput. Aided Des. 207–215 (2007)

    Google Scholar 

  13. Walter, D., Little, S., Myers, C.: Bounded model checking of analog and mixed-signal circuits using an SMT solver. In: Automated Technology for Verification and Analysis, LNCS, vol. 4762, pp. 66–81. Springer, Berlin (2007)

    Google Scholar 

  14. Dang, T., Donze, A., Maler, O.: Verification of analog and mixed-signal circuits using hybrid system techniques. In: Formal Methods in Computer-Aided Design, LNCS, vol. 3312, pp. 14–17. Springer, Berlin (2004)

    Google Scholar 

  15. Gupta, S., Krogh, B.H., Rutenbar, R.A.: Towards formal verification of analog designs. In: IEEE/ACM International Conference on Computer Aided Design, pp. 210–217 (2004)

    Google Scholar 

  16. G. Frehse, B.H. Krogh, R.A. Rutenbar. Verifying analog oscillator circuits using forward/backward abstraction refinement. IEEE/ACM Des. Autom. Test Eur. pp. 257–262 (2006)

    Google Scholar 

  17. Lata, K., Roy, S.K.: Formal verification of analog and mixed signal designs using SPICE circuit simulation traces. J. Electron. Test. 29(5), 715–740 (2013)

    Google Scholar 

  18. Al-Sammane, G.: Simulation Symbolique des Circuits Decrits au Niveau Algorithmique. PhD thesis, Université Joseph Fourier, Grenoble, France (2005)

    Google Scholar 

  19. Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2000)

    Google Scholar 

  20. Al Sammane, G., Zaki, M., Tahar,S.: A symbolic methodology for the verification of analog and mixed signal designs. IEEE/ACM Des. Autom. Test Eur. 249–254 (2007)

    Google Scholar 

  21. Moore, J.S.: Introduction to the OBDD algorithm for the ATP community. J. Autom. Reason. 12(1):33–45 (1994)

    Google Scholar 

  22. Amla, N., Du, X., Kuehlmann, A., Kurshan, R.P., McMillan, K.L.: An analysis of SAT-based model checking techniques in an industrial environment. In: Correct Hardware Design and Verification Methods, LNCS, vol. 3725, pp. 254–268. Springer, Berlin (2005)

    Google Scholar 

  23. Wolfram, S.: Mathematica: A System for Doing Mathematics by Computer. Addison Wesley Longman Publishing, USA (1991)

    Google Scholar 

  24. Frehse, G., Le Guernic, C., Donzé, A., Cotton, S., Ray, R., Lebeltel, O., Ripado, R., Girard, A., Dang, T., Maler, O.: Spaceex: scalable verification of hybrid systems. In: Computer Aided Verification, LNCS, vol. 6806, pp. 379–395. Springer, Berlin (2011)

    Google Scholar 

  25. Denman, W., Akbarpour, B., Tahar, S., Zaki, M., Paulson, L.C.P: Formal verification of analog designs using MetiTarski. In: Formal Methods in Computer Aided Design, pp. 93–100. IEEE, New York (2009)

    Google Scholar 

  26. Hanna, K.: Reasoning about Real Circuits, vol. 859, pp. 235–253. Springer, Berlin (1994)

    Google Scholar 

  27. Ghosh, A., Vemuri, R.: Formal verification of synthesized analog circuits. In: ACM/IEE International Conference on Computer Design, vol. 31, pp. 40–45 (1999)

    Google Scholar 

  28. Hanna, K.: Reasoning about analog level implementation of digital systems. Form. Methods Syst. Des. 16(2), 127–158 (2000)

    Article  MathSciNet  Google Scholar 

  29. Taqdees, S.H., Hasan, O.: Formal verification of continuous models of analog circuits. In: Frontiers in Analog CAD, Poster Paper (2013)

    Google Scholar 

  30. Harrison, J.: Theorem Proving with the Real Numbers. Springer, Berlin (1998)

    Google Scholar 

  31. Usman, M., Hasan, O.: Formal verification of cyber-physical systems: coping with continuous elements. In: Computational Science and Its Applications, LNCS-Part 1, vol. 7971, pp. 358–371. Springer, Berlin (2013)

    Google Scholar 

  32. Harrison, J.: A HOL theory of Euclidean space. In: Theorem Proving in Higher Order Logics, LNCS, vol. 3603, pp. 114–129. Springer, Berlin (2005)

    Google Scholar 

  33. Taqdees, S.H., Hasan, O.: Formalization of Laplace transform using the multivariate calculus theory of HOL-light. In: Logic for Programing Artificial Intelligence and Reasoning, LNCS, vol. 8312, pp. 744–758. Springer, Berlin (2013)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Concordia University, Montreal, Québec, Canada

    Mohamed H. Zaki, Sofiène Tahar & Ghiath Al-Sammane

  2. National University of Sciences and Technology, Islamabad, Pakistan

    Osman Hasan

Authors
  1. Mohamed H. Zaki
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Osman Hasan
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Sofiène Tahar
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Ghiath Al-Sammane
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Mohamed H. Zaki .

Editor information

Editors and Affiliations

  1. Department of Electronics, ENET'Com, University of Sfax, Sfax, Tunisia

    Mourad Fakhfakh

  2. Dept. of Electronics, INAOE, Tonantzintla, Puebla, Mexico

    Esteban Tlelo-Cuautle

  3. Laboratory LiSSi (EA 3956), Université Paris-Est Créteil, Vitry-sur-Seine, France

    Patrick Siarry

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this chapter

Cite this chapter

Zaki, M.H., Hasan, O., Tahar, S., Al-Sammane, G. (2015). Framework for Formally Verifying Analog and Mixed-Signal Designs. In: Fakhfakh, M., Tlelo-Cuautle, E., Siarry, P. (eds) Computational Intelligence in Analog and Mixed-Signal (AMS) and Radio-Frequency (RF) Circuit Design. Springer, Cham. https://doi.org/10.1007/978-3-319-19872-9_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-19872-9_5

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-19871-2

  • Online ISBN: 978-3-319-19872-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation