Formal Techniques for Verification and Coverage Analysis of Analog Systems



Formal verification for analog circuits has grown and is attracting more attention due to the introduction of cyber-physical systems in many technical areas including demanding concepts like autonomous driving. In this chapter, we give an overview of the state of the art including different concepts, and present some new ideas, especially coverage metrics for analog circuit verification. Putting all these concepts together, a methodology is introduced partially answering the question, how a whole system can be formally verified in parallel to the top-down design spanning from system to transistor level. Some results for analog circuits and continuous system-level descriptions are presented, demonstrating the feasibility of the approaches and giving an impression of their capabilities.


  1. 1.
    A. Vachoux, C. Grimm, K. Einwich, A. Vachoux, C. Grimm, K. Einwich, Analog and mixed-signal modeling with SystemC-AMS, in Proceedings of the 2003 International Symposium on Circuits and Systems, 2003, ISCAS’03, vol. 3 (2003), pp. III–914Google Scholar
  2. 2.
    R. Telichevesky, K. Kundert, J. White, SpectreRF; New Frontiers in Circuit Simulation (1995), pp. 3–24Google Scholar
  3. 3.
    D. Zaum, S. Hoelldampf, M. Olbrich, E. Barke, I. Neumann, S. Schmidt, The PRAISE approach for accelerated transient analysis applied to wire models, in Behavioral Modeling and Simulation Workshop, BMAS 2009 (IEEE, 2009), pp. 120–125Google Scholar
  4. 4.
    G. Gielen, E. Maricau, in Analog IC Reliability in Nanometer CMOS (Springer, Heidelberg, 2013)Google Scholar
  5. 5.
    T. Henzinger, P.-H. Ho, H. Wong-Toi, HyTech: a model checker for hybrid systems. Lecture Notes in Computer Science (Springer, 1997), pp. 460–463Google Scholar
  6. 6.
    E. Asarin, T. Dang, O. Maler, d/dt: a tool for reachability analysis of continuous and hybrid systems (2001)Google Scholar
  7. 7.
    A. Eggers, N. Ramdani, N.S. Nedialkov, M. Fränzle, Improving the SAT modulo ODE approach to hybrid systems analysis by combining different enclosure methods. Softw. Syst. Model. 14(1), 121–148 (2012)CrossRefzbMATHGoogle Scholar
  8. 8.
    T.A. Henzinger, P.-H. Ho, H. Wong-Toi, Algorithmic analysis of nonlinear hybrid systems. IEEE Trans. Autom. Control 43(4), 540–554 (1998)MathSciNetCrossRefzbMATHGoogle Scholar
  9. 9.
    G. Frehse, PHAVer: algorithmic verification of hybrid systems past HyTech, in Proceedings of Hybrid Systems: Computation and Control (HSCC 2005). Lecture Notes in Computer Science, vol. 3414 (2005), pp. 258–273Google Scholar
  10. 10.
    T. Dang, A. Donzé, O. Maler, Verification of analog and mixed-signal circuits using hybrid system techniques, in Formal Methods in Computer-Aided Design (Springer, 2004), pp. 21–36Google Scholar
  11. 11.
    Z.J.D. Ghiath Al Sammane, Mohamed H. Zaki, S. Tahar, Towards assertion based verification of analog and mixed signal designs using PSL, in Forum on Design Languages (FDL) (2007)Google Scholar
  12. 12.
    S. Little, D. Walter, N. Seegmiller, C. Myers, T. Yoneda, Verication of analog and mixed-signal circuits using timed hybrid petri nets, in ATVA (2004), pp. 426–440Google Scholar
  13. 13.
    L. Hedrich, E. Barke, A formal approach to verification of linear analog circuits with parameter tolerances, in Proceedings of the Design, Automation and Test in Europe (1998), pp. 649–654Google Scholar
  14. 14.
    D. Grabowski, M. Olbrich, C. Grimm, E. Barke, Analog circuit simulation using range arithmetics, in ASPDAC (2008), pp. 762–767Google Scholar
  15. 15.
    M. Althoff, A. Rajhans, B.H. Krogh, S. Yaldiz, X. Li, L. Pileggi, Formal verification of phase-locked loops using reachability analysis and continuization. Commun. ACM 56(10), 97–104 (2013)CrossRefGoogle Scholar
  16. 16.
    G. Frehse, C. Le Guernic, A. Donzé, S. Cotton, R. Ray, O. Lebeltel, R. Ripado, A. Girard, T. Dang, O. Maler, SpaceEx: scalable verification of hybrid systems. in Computer Aided Verification (Springer, 2011), pp. 379–395Google Scholar
  17. 17.
    M. Freisfeld, M. Olbrich, E. Barke, Circuit simulations with uncertainties using affine arithmetic and piecewise affine statemodels, in 9th International Conference on Solid-State and Integrated-Circuit Technology, 2008 ICSICT (2008), pp. 496–499Google Scholar
  18. 18.
    T.R. Dastidar, P.P. Chakrabarti, A verification system for transient response of analog circuits. ACM Trans. Des. Autom. Electron. Syst. 12(3), 31:1–31:39 (2008)Google Scholar
  19. 19.
    L. Hedrich, E. Barke, A formal approach to nonlinear analog circuit verification, in Proceedings of the IEEE/ACM International Conference on Computer-Aided Design ICCAD-95. Digest of Technical Papers (1995), pp. 123–127Google Scholar
  20. 20.
    A.V. Karthik, S. Ray, P. Nuzzo, A. Mishchenko, R. K. Brayton, J. Roychowdhury, ABCD-NL: approximating continuous non-linear dynamical systems using purely Boolean models for analog/mixed-signal verification. in ASP-DAC (2004), pp. 250–255Google Scholar
  21. 21.
    S. Steinhorst, L. Hedrich, Improving verification coverage of analog circuit blocks by state space-guided transient simulation, in IEEE International Symposium on Circuits and Systems (2010)Google Scholar
  22. 22.
    D. Grabowski, D. Platte, L. Hedrich, E.A. Barke, Time constrained verification of analog circuits using model-checking algorithms, in ENCTS: Workshop on Formal Verification of Analog Circuits (2005)Google Scholar
  23. 23.
    O. Maler, A. Pnueli, Extending PSL for Analog Circuits, in Research Report:PROSYD: Property-Based System Design FP6-IST-507219 (2005)Google Scholar
  24. 24.
    S. Steinhorst, L. Hedrich, Analog assertion-based verification on partial state space representations using ASL. In 2012 Forum on Specification and Design Languages (FDL) (2012), pp. 98–104Google Scholar
  25. 25.
    J. Eckmüller, M. Gröpl, H. Gräb, Hierarchical characterization of analog integrated circuits, in DATE ’98: Design, Automation and Test in Europe (1998)Google Scholar
  26. 26.
    M. Ma, L. Hedrich, C. Sporrer, ASDeX: a formal specification for analog circuit enabling a full automated design validation. in Design Automation for Embedded Systems (2012), pp. 1–20Google Scholar
  27. 27.
    S. Fine, A. Ziv, Coverage directed test generation for functional verification using Bayesian networks, in Proceedings of the Design Automation Conference (2003), pp. 286–291Google Scholar
  28. 28.
    F. Haedicke, D. Große, R. Drechsler, A guiding coverage metric for formal verification, in Design, Automation and Test in Europe Conference and Exhibition (DATE) (IEEE, 2012), pp. 617–622Google Scholar
  29. 29.
    J.-Y. Jou, C. Liu, Coverage analysis techniques for hdl design validation. in Proceedings of the Asia Pacific CHip Design Languages (1999), pp. 48–55Google Scholar
  30. 30.
    K. Arabi, B. Kaminska, Parametric and catastrophic fault coverage of analog circuits in oscillation-test methodology, in 15th IEEE VLSI Test Symposium (1997), pp. 166–171Google Scholar
  31. 31.
    J. Parky, S. Madhavapeddiz, A. Paglieri, C. Barrz, J. Abraham, Defect-based analog fault coverage analysis using mixed-mode fault simulation. in IEEE 15th International Mixed-Signals, Sensors, and Systems Test Workshop, 2009, IMS3TW ’09 (2009), pp. 1–6Google Scholar
  32. 32.
    M. Horowitz, M. Jeeradit, F. Lau, S. Liao, B. Lim, J. Mao, Fortifying analog models with equivalence checking and coverage analysis, in Proceedings of the 47th Design Automation Conference, DAC ’10, NY, USA, New York (2010), pp. 425–430Google Scholar
  33. 33.
    A. Julius, G. Fainekos, M. Anand, I. Lee, G. Pappas, Robust test generation and coverage for hybrid systems, in Proceedings of the 10th International Conference on Hybrid Systems: Computation and Control (HSCC) (2007), pp. 329–342Google Scholar
  34. 34.
    T. Nahhal, T. Dang, Test coverage for continuous and hybrid systems. in Computer Aided Verification (Springer, 2007), pp. 449–462Google Scholar
  35. 35.
    L. Pillage, C. Wolff, R. Rohrer, Dominant Pole(s)/Zero(s) analysis for analog circuit, in CICC (1989), pp. 21.3.1–21.3.4Google Scholar
  36. 36.
    R. Freund, P. Feldmann, Reduction-order modeling of large linear passive multi-terminal circuits using matrix-pade approximation, in Review (1988), pp. 1–19Google Scholar
  37. 37.
    S. Steinhorst, L. Hedrich, Advanced methods for equivalence checking of analog circuits with strong nonlinearities. Form. Methods Syst. Des. 36(2), 131–147 (2010)CrossRefzbMATHGoogle Scholar
  38. 38.
    S. Steinhorst, L. Hedrich, Trajectory-directed discrete state space modeling for formal verification of nonlinear analog circuits, in Proceedings of the International Conference on Computer-Aided Design (ACM, 2012), pp. 202–209Google Scholar
  39. 39.
    W. Hartong, R. Klausen, L. Hedrich, Formal verification for nonlinear analog systems: approaches to model and equivalence checking, in Advanced Formal Verification, ed. by R. Drechsler (Kluwer Academic Publishers, Boston, 2004), pp. 205–245Google Scholar
  40. 40.
    A.T. Davis, An overview of algorithms in Gnucap, in University/Government/Industry Microelectronics Symposium (2003), pp. 360–361Google Scholar
  41. 41.
    D. Nickovic, O. Maler, AMT: a property-based monitoring tool for analog systems, in Formal Modeling and Analysis of Timed Systems, vol. 4763, Lecture Notes in Computer Science, ed. by J.-F. Raskin, P. Thiagarajan (Springer, Heidelberg, 2007), pp. 304–319CrossRefGoogle Scholar
  42. 42.
    R. Alur, C. Courcoubetis, D. Dill, Model-checking in dense real-time. Inf. Comput. 104, 2–34 (1993)MathSciNetCrossRefzbMATHGoogle Scholar
  43. 43.
    S. Steinhorst, L. Hedrich, Model checking of analog systems using an analog specification language, in Proceedings of the Design, Automation and Test in Europe DATE ’08 (2008), pp. 324–329Google Scholar
  44. 44.
    J.L. Bentley, Multidimensional binary search trees used for associative searching. Commun. ACM 18(9), 509–517 (1975)CrossRefzbMATHGoogle Scholar
  45. 45.
    B. Chazelle, An optimal convex hull algorithm in any fixed dimension. Discret. Comput. Geom. 10, 377–409 (1993)MathSciNetCrossRefzbMATHGoogle Scholar
  46. 46.
    M. Althoff, S. Yaldiz, A. Rajhans, X. Li, B. Krogh, L. Pileggi, Formal verification of phase-locked loops using reachability analysis and continuization, in 2011 IEEE/ACM International Conference on Computer-Aided Design (ICCAD) (IEEE, 2011), pp. 659–666Google Scholar

Copyright information

© Springer International Publishing AG 2018

Authors and Affiliations

  1. 1.University of FrankfurtFrankfurt/MainGermany

Personalised recommendations