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)


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.


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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  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).
  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).
  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.
  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.
  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).
  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).
  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).
  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). 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). 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).
  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).
  14. 14.
    Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB standard version 2.0. In: 8th SMT Workshop (2010).
  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). 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.
  17. 17.
    Kurshan, R., McMillan, K.: Analysis of digital circuits through symbolic reduction. IEEE Trans. CAD 10(11), 1356–1371 (1991). CrossRefGoogle Scholar
  18. 18.
    Hedrich, L., Barke, E.: A formal approach to nonlinear analog circuit verification. In: ICCAD, pp. 123–127 (1995).
  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).
  20. 20.
    Hartong, W., Hedrich, L., Barke, E.: Model checking algorithms for analog verification. In: 39th DAC, pp. 542–547, June 2002.
  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).
  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).
  23. 23.
    Jesser, A., Hedrich, L.: A symbolic approach for mixed-signal model checking. In: ASPDAC, pp. 404–409 (2008).
  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).
  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).
  26. 26.
    Lin, H., Li, P.: Parallel hierarchical reachability analysis for analog verification. In: 51st DAC, pp. 150:1–150:6 (2014).
  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).
  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.
  29. 29.
    Marques-Silva, J., Sakallah, K.: GRASP: a search algorithm for propositional satisfiability. IEEE Trans. Computers 48(5), 506–521 (1999). 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).

Copyright information

© Springer International Publishing Switzerland 2015

Authors and Affiliations

  1. 1.University of British ColumbiaVancouverCanada

Personalised recommendations