Skip to main content
SpringerLink
Log in
Book cover

NASA Formal Methods Symposium

NFM 2015: NASA Formal Methods pp 310–326Cite as

Integrating SMT with Theorem Proving for Analog/Mixed-Signal Circuit Verification

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 9058))

Abstract

We present our integration of the Z3 SMT solver into the ACL2 theorem prover and its application to formal verification of analog-mixed signal circuits by proving global convergence for a state-of-the-art digital phase-locked loop (PLL). SMT (satisfiability modulo theory) solvers eliminate much of the tedium associated with detailed proofs by providing automatic reasoning about propositional formulas including equalities and inequalities of polynomial functions. A theorem prover complements the SMT solver by providing a proof structuring and proof by induction. We use this combined tool to show global convergence (i.e. correct start-up and mode-switching) of a digital PLL. The PLL is an example of a second-order hybrid control system; its verification demonstrates how these methods can address challenges that arise when verifying such designs.

This research was supported by grants from NSERC Canada and Intel.

This is a preview of subscription content, 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 PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight 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

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. de Moura, L., Bjørner, N.S.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). http://dx.doi.org/10.1007/978-3-540-78800-3_24

  2. Kaufmann, M., Moore, J., Manolios, P.: Computer-Aided Reasoning: An Approach. Kluwer (2000)

    Google Scholar 

  3. Kundert, K.S.: Introduction to RF simulation and its application. IEEE J. Solid-State Circuits 34(9), 1298–1319 (1999). http://dx.doi.org/10.1109/4.782091

  4. Kim, J., Jeeradit, M., Lim, B., Horowitz, M.A.: Leveraging designer’s intent: a path toward simpler analog CAD tools. In: Custom Integrated Circuits Conf., pp. 613–620, September 2009. http://dx.doi.org/10.1109/CICC.2009.5280741

  5. McLaughlin, S., Barrett, C., Ge, Y.: Cooperating theorem provers: A case study combining HOL-Light and CVC Lite. In: 3rd Workshop on Pragmatics of Decision Procedures in Automated Reasoning, pp. 43–51. http://dx.doi.org/10.1016/j.entcs.2005.12.005

  6. Fontaine, P., Marion, J.-Y., Merz, S., Nieto, L.P., Tiu, A.F.: Expressiveness + automation + soundness: towards combining SMT solvers and interactive proof assistants. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 167–181. Springer, Heidelberg (2006). http://dx.doi.org/10.1007/11691372_11

  7. Besson, F.: Fast reflexive arithmetic tactics the linear case and beyond. In: Altenkirch, T., McBride, C. (eds.) TYPES 2006. LNCS, vol. 4502, pp. 48–62. Springer, Heidelberg (2007). http://dx.doi.org/10.1007/978-3-540-74464-1_4

  8. Armand, M., Faure, G., Grégoire, B., Keller, C., Théry, L., Werner, B.: A modular integration of SAT/SMT solvers to Coq through proof witnesses. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol. 7086, pp. 135–150. Springer, Heidelberg (2011). http://dx.doi.org/10.1007/978-3-642-25379-9_12

  9. Merz, S., Vanzetto, H.: Automatic verification of TLA\({^ + }\) proof obligations with SMT solvers. In: Bjørner, N., Voronkov, A. (eds.) LPAR-18 2012. LNCS, vol. 7180, pp. 289–303. Springer, Heidelberg (2012). https://hal.inria.fr/hal-00760570/document

    Chapter  Google Scholar 

  10. Blanchette, J.C., Böhme, S., Paulson, L.C.: Extending Sledgehammer with SMT solvers. J. of Automated Reasoning 51(1), 109–128 (2013). http://dx.doi.org/10.1007/s10817-013-9278-5

    Article  Google Scholar 

  11. Déharbe, D., Fontaine, P., Guyof, Y., Voisin, L.: Integrating SMT solvers in Rodin. Science of Computer Programming 94(pt. 2), 130–143 (2014). http://www.sciencedirect.com/science/article/pii/S016764231400183X

  12. Barrett, C.W., Berezin, S.: CVC lite: A new implementation of the cooperating validity checker category B. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 515–518. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  13. Abrial, J.-R., Butler, M., Hallerstede, S., Voisin, L.: An open extensible tool environment for Event-B. In: Liu, Z., Kleinberg, R.D. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 588–605. Springer, Heidelberg (2006). http://dx.doi.org/10.1007/11901433_32

  14. Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB standard version 2.0. In: 8th SMT Workshop (2010). http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.0-r10.12.21.pdf

  15. Immler, F.: Formally verified computation of enclosures of solutions of ordinary differential equations. In: Badger, J.M., Rozier, K.Y. (eds.) NFM 2014. LNCS, vol. 8430, pp. 113–127. Springer, Heidelberg (2014). http://home.in.tum.de/ immler/documents/immler2014enclosures.pdf

    Chapter  Google Scholar 

  16. Harutunian, S.: Formal verification of computer controlled systems. Ph.D. dissertation, University of Texas, Austin, May 2007. http://www.lib.utexas.edu/etd/d/2007/harutunians68792/harutunians68792.pdf

  17. Kurshan, R., McMillan, K.: Analysis of digital circuits through symbolic reduction. IEEE Trans. CAD 10(11), 1356–1371 (1991). http://dx.doi.org/10.1109/43.97615

    Article  Google Scholar 

  18. Hedrich, L., Barke, E.: A formal approach to nonlinear analog circuit verification. In: ICCAD, pp. 123–127 (1995). http://dl.acm.org/citation.cfm?id=224841.224870

  19. Greenstreet, M. R.: Verifying safety properties of differential equations. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 277–287. Springer, Heidelberg (1996). http://dx.doi.org/10.1007/3-540-61474-5_76

  20. Hartong, W., Hedrich, L., Barke, E.: Model checking algorithms for analog verification. In: 39th DAC, pp. 542–547, June 2002. http://dx.doi.org/10.1109/DAC.2002.1012684

  21. Dang, T., Donzé, A., Maler, O.: Verification of analog and mixed-signal circuits using hybrid system techniques. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol. 3312, pp. 21–36. Springer, Heidelberg (2004). http://dx.doi.org/10.1007/978-3-540-30494-4_3

  22. Dong, Z.J., Zaki, M.H., Al-Sammane, G., Tahar, S., Bois, G.: Checking properties of PLL designs using run-time verification. In: Int’l. Conf. Microelectronics, pp. 125–128 (2007). http://dx.doi.org/10.1109/ICM.2007.4497676

  23. Jesser, A., Hedrich, L.: A symbolic approach for mixed-signal model checking. In: ASPDAC, pp. 404–409 (2008). http://dl.acm.org/citation.cfm?id=1356802.1356903

  24. Althoff, M., Rajhans, A., et al.: Formal verification of phase-locked loops using reachability analysis and continuization. Comm. ACM 56(10), 97–104 (2013). http://doi.acm.org/10.1145/2507771.2507783

  25. Lin, H., Li, P., Myers, C. J.: Verification of digitally-intensive analog circuits via kernel ridge regression and hybrid reachability analysis. In: 50th DAC, pp. 66:1–66:6 (2013). http://doi.acm.org/10.1145/2463209.2488814

  26. Lin, H., Li, P.: Parallel hierarchical reachability analysis for analog verification. In: 51st DAC, pp. 150:1–150:6 (2014). http://doi.acm.org/10.1145/2593069.2593178

  27. Frehse, G., et al.: SpaceEx: scalable verification of hybrid systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 379–395. Springer, Heidelberg (2011). http://dx.doi.org/10.1007/978-3-642-22110-1_30

  28. Wei, J., Peng, Y., Yu, G., Greenstreet, M.: Verifying global convergence for a digital phase-locked loop. In: 13th FMCAD, pp. 113–120, October 2013. http://dx.doi.org/10.1109/FMCAD.2013.6679399

  29. Marques-Silva, J., Sakallah, K.: GRASP: a search algorithm for propositional satisfiability. IEEE Trans. Computers 48(5), 506–521 (1999). http://dx.doi.org/10.1109/12.769433

    Article  MathSciNet  Google Scholar 

  30. Gamboa, R.: Mechanically verified real-valued algorithms in ACL2. Ph.D. dissertation, University of Texas at Austin (1999)

    Google Scholar 

  31. Crossley, J., Naviasky, E., Alon, E.: An energy-efficient ring-oscillator digital PLL. In: Custom Integrated Circuits Conf. (September 2010). http://dx.doi.org/10.1109/CICC.2010.5617417

Download references

Author information

Authors and Affiliations

  1. University of British Columbia, Vancouver, British Columbia, Canada

    Yan Peng & Mark Greenstreet

Authors
  1. Yan Peng
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Mark Greenstreet
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Yan Peng .

Editor information

Editors and Affiliations

  1. Jet Propulsion Laboratory, Pasadena, California, USA

    Klaus Havelund

  2. Jet Propulsion Laboratory, Pasadena, California, USA

    Gerard Holzmann

  3. Jet Propulsion Laboratory, Pasadena, California, USA

    Rajeev Joshi

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Peng, Y., Greenstreet, M. (2015). Integrating SMT with Theorem Proving for Analog/Mixed-Signal Circuit Verification. In: Havelund, K., Holzmann, G., Joshi, R. (eds) NASA Formal Methods. NFM 2015. Lecture Notes in Computer Science(), vol 9058. Springer, Cham. https://doi.org/10.1007/978-3-319-17524-9_22

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-17524-9_22

  • Published:

  • Publisher Name: Springer, Cham

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

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

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation