Advertisement

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

  • Yan PengEmail author
  • Mark Greenstreet
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, 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.

Keywords

Global Convergence Theorem Prover Proof Obligation Satisfiability Modulo Theory Reachability Analysis 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 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. 2.
    Kaufmann, M., Moore, J., Manolios, P.: Computer-Aided Reasoning: An Approach. Kluwer (2000)Google Scholar
  3. 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. 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. 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. 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. 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. 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. 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 CrossRefGoogle Scholar
  10. 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 CrossRefGoogle Scholar
  11. 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. 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) CrossRefGoogle Scholar
  13. 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. 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. 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 CrossRefGoogle Scholar
  16. 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. 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 CrossRefGoogle Scholar
  18. 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. 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. 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. 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. 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. 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. 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. 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. 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. 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. 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. 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 CrossRefMathSciNetGoogle Scholar
  30. 30.
    Gamboa, R.: Mechanically verified real-valued algorithms in ACL2. Ph.D. dissertation, University of Texas at Austin (1999)Google Scholar
  31. 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

Copyright information

© Springer International Publishing Switzerland 2015

Authors and Affiliations

  1. 1.University of British ColumbiaVancouverCanada

Personalised recommendations