Skip to main content
SpringerLink
Log in

Formal Techniques for Verification and Coverage Analysis of Analog Systems

  • Chapter
  • First Online:
Formal System Verification

Abstract

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
eBook
USD 16.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 129.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 129.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

Notes

  1. 1.

    A low weight (\(w_{\sigma } = 0)\) indicates an interesting state inside the ATS. The weight is set to zero, because this can be directly be used as the initial value for the labeling function \(\omega \), which indicates how often this state was covered before or not, which is used by the path planning algorithm presented in Sect. 1.5.3.

References

  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–914

    Google Scholar 

  2. R. Telichevesky, K. Kundert, J. White, SpectreRF; New Frontiers in Circuit Simulation (1995), pp. 3–24

    Google Scholar 

  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–125

    Google Scholar 

  4. G. Gielen, E. Maricau, in Analog IC Reliability in Nanometer CMOS (Springer, Heidelberg, 2013)

    Google Scholar 

  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–463

    Google Scholar 

  6. E. Asarin, T. Dang, O. Maler, d/dt: a tool for reachability analysis of continuous and hybrid systems (2001)

    Google Scholar 

  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)

    Article  MATH  Google Scholar 

  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)

    Article  MathSciNet  MATH  Google Scholar 

  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–273

    Google Scholar 

  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–36

    Google Scholar 

  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. 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–440

    Google Scholar 

  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–654

    Google Scholar 

  14. D. Grabowski, M. Olbrich, C. Grimm, E. Barke, Analog circuit simulation using range arithmetics, in ASPDAC (2008), pp. 762–767

    Google Scholar 

  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)

    Article  Google Scholar 

  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–395

    Google Scholar 

  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–499

    Google Scholar 

  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. 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–127

    Google Scholar 

  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–255

    Google Scholar 

  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. 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. O. Maler, A. Pnueli, Extending PSL for Analog Circuits, in Research Report:PROSYD: Property-Based System Design FP6-IST-507219 (2005)

    Google Scholar 

  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–104

    Google Scholar 

  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. 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–20

    Google Scholar 

  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–291

    Google Scholar 

  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–622

    Google Scholar 

  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–55

    Google Scholar 

  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–171

    Google Scholar 

  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–6

    Google Scholar 

  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–430

    Google Scholar 

  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–342

    Google Scholar 

  34. T. Nahhal, T. Dang, Test coverage for continuous and hybrid systems. in Computer Aided Verification (Springer, 2007), pp. 449–462

    Google Scholar 

  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.4

    Google Scholar 

  36. R. Freund, P. Feldmann, Reduction-order modeling of large linear passive multi-terminal circuits using matrix-pade approximation, in Review (1988), pp. 1–19

    Google Scholar 

  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)

    Article  MATH  Google Scholar 

  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–209

    Google Scholar 

  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–245

    Google Scholar 

  40. A.T. Davis, An overview of algorithms in Gnucap, in University/Government/Industry Microelectronics Symposium (2003), pp. 360–361

    Google Scholar 

  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–319

    Chapter  Google Scholar 

  42. R. Alur, C. Courcoubetis, D. Dill, Model-checking in dense real-time. Inf. Comput. 104, 2–34 (1993)

    Article  MathSciNet  MATH  Google Scholar 

  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–329

    Google Scholar 

  44. J.L. Bentley, Multidimensional binary search trees used for associative searching. Commun. ACM 18(9), 509–517 (1975)

    Article  MATH  Google Scholar 

  45. B. Chazelle, An optimal convex hull algorithm in any fixed dimension. Discret. Comput. Geom. 10, 377–409 (1993)

    Article  MathSciNet  MATH  Google Scholar 

  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–666

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Frankfurt, Frankfurt/Main, Germany

    Andreas Fürtig & Lars Hedrich

Authors
  1. Andreas Fürtig
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Lars Hedrich
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Andreas Fürtig .

Editor information

Editors and Affiliations

  1. DFKI, University of Bremen, Bremen, Germany

    Rolf Drechsler

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG

About this chapter

Cite this chapter

Fürtig, A., Hedrich, L. (2018). Formal Techniques for Verification and Coverage Analysis of Analog Systems. In: Drechsler, R. (eds) Formal System Verification. Springer, Cham. https://doi.org/10.1007/978-3-319-57685-5_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-57685-5_1

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-57683-1

  • Online ISBN: 978-3-319-57685-5

  • eBook Packages: EngineeringEngineering (R0)

Publish with us

Policies and ethics

Search

Navigation