Formal Methods in System Design

, Volume 36, Issue 2, pp 97–113 | Cite as

On simulation-based probabilistic model checking of mixed-analog circuits

  • Edmund Clarke
  • Alexandre Donzé
  • Axel Legay


In this paper, we consider verifying properties of mixed-signal circuits, i.e., circuits for which there is an interaction between analog (continuous) and digital (discrete) values. We use a simulation-based approach that consists of evaluating the property on a representative subset of behaviors and answering the question of whether the circuit satisfies the property with a probability greater than or equal to some threshold. We propose a logic adapted to the specification of properties of mixed-signal circuits in the temporal domain as well as in the frequency domain. We also demonstrate the applicability of the method on different models of ΔΣ modulators for which previous formal verification attempts were too conservative and required excessive computation time.


Probabilistic model-checking Simulation-based techniques Mixed-signals circuits verification Delta-sigma modulators 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Aziz PM, Sorensen HV, Van Der Spiegel J (1996) An overview of sigma-delta converters. IEEE Signal Process Mag, pp 61–84, January 1996 Google Scholar
  2. 2.
    Baier C, Haverkort BR, Hermanns H, Katoen J-P (2003) Model-checking algorithms for continuous-time Markov chains. IEEE Trans Software Eng 29(6):524–541 CrossRefGoogle Scholar
  3. 3.
    Biere A, Heljanko K, Junttila TA, Latvala T, Schuppan V (2006) Linear encodings of bounded ltl model checking. Log Methods Comput Sci 2(5) Google Scholar
  4. 4.
    Ciesinski F, Baier C (2006) Liquor: A tool for qualitative and quantitative linear time analysis of reactive systems. In: QEST, IEEE, pp 131–132 Google Scholar
  5. 5.
    Ciesinski F, Größer M (2004) On probabilistic computation tree logic. In: Validation of stochastic systems. Lecture notes in computer science, vol 2925. Springer, Berlin, pp 147–188 CrossRefGoogle Scholar
  6. 6.
    Courcoubetis C, Yannakakis M (1995) The complexity of probabilistic verification. J ACM 42(4):857–907 MATHCrossRefMathSciNetGoogle Scholar
  7. 7.
    Dang T, Donze A, Maler O (2004) Verification of analog and mixed-signal circuits using hybrid systems techniques. In: Hu AJ, Martin AK (eds) FMCAD’04–Formal methods for computer aided design. Lecture notes in computer science, vol 3312. Springer, Berlin, pp 21–36 Google Scholar
  8. 8.
    d’Amorim M, Roşu G (2005) Efficient monitoring of ω-languages. In: CAV. Lecture notes in computer science, vol 3576. Springer, Berlin, pp 364–378 Google Scholar
  9. 9.
    Frigo M, Johnson SG (1997) The fastest Fourier transform in the west. Technical report MIT-LCS-TR-728, Massachusetts Institute of Technology, September 1997 Google Scholar
  10. 10.
    Gupta S, Krogh BH, Rutenbar RA (2004) Towards formal verification of analog designs. In: ICCAD, pp 210–217 Google Scholar
  11. 11.
    Kwiatkowska MZ, Norman G, Parker D (2004) Prism 2.0: A tool for probabilistic model checking. In: QEST, IEEE, pp 322–323 Google Scholar
  12. 12.
    Bauer A, Leucker M, Schallhart C (2006) Monitoring of real-time properties. In: FSTTCS. Lecture notes in computer science, vol 4337. Springer, Berlin, pp 260–272 Google Scholar
  13. 13.
    Matsumo M, Nishimura T (2000) Dynamic creation of pseudorandom number generators. In: Monte-Carlo and Quasi-Monte Carlo methods 1998. Springer, Berlin, pp 56–69 Google Scholar
  14. 14.
    Maler O, Nickovic D, Pnueli A (2008) Checking temporal properties of discrete, timed and continuous behaviors. In: Pillars of computer science, pp 475–505 Google Scholar
  15. 15.
    Medeiro F, Pérez-Verdú B, Rodríguez-Vázquez A (2001) Top-down design of high-performance sigma-delta modulators. Kluwer, Dordrecht. Chapter 2 Google Scholar
  16. 16.
    Nickovic D, Maler O (2007) Amt: A property-based monitoring tool for analog systems. In: FORMATS, pp 304–319 Google Scholar
  17. 17.
    Pnueli A (1977) The temporal logic of programs. In: Proc. 18th annual symposium on foundations of computer science (FOCS), pp 46–57 Google Scholar
  18. 18.
    Schreier R (2003) The delta-sigma toolbox version 6.0, January 2003 Google Scholar
  19. 19.
    Zakhor A, Hein S (1993) On the stability of sigma delta modulators. IEEE Trans Signal Process, 41, July 1993 Google Scholar
  20. 20.
    Smith SW (1997) The scientist and engineer’s guide to digital signal processing. California Technical Publishing, San Diego Google Scholar
  21. 21.
    Schreier R, Temes GC (2005) Understanding delta-sigma data converters. Wiley/IEEE Press, Hoboken Google Scholar
  22. 22.
    Sen K, Viswanathan M, Agha G (2004) Statistical model checking of black-box probabilistic systems. In: CAV. Lecture notes in computer science, vol 3114. Springer, Berlin, pp 202–215 Google Scholar
  23. 23.
    Sen K, Viswanathan M, Agha G (2005) On statistical model checking of stochastic systems. In: CAV. Lecture notes in computer science, vol 3576, pp 266–280 Google Scholar
  24. 24.
    Wald A (1945) Sequential tests of statistical hypotheses. Ann Math Stat 16(2):117–186 MATHCrossRefMathSciNetGoogle Scholar
  25. 25.
    Younes HLS, Kwiatkowska MZ, Norman G, Parker D (2006) Numerical vs. statistical probabilistic model checking. STTT 8(3):216–228 CrossRefGoogle Scholar
  26. 26.
    Younes HLS (2005) Probabilistic verification for “black-box” systems. In: CAV. Lecture notes in computer science, vol 3576. Springer, Berlin, pp 253–265 Google Scholar
  27. 27.
    Younes HLS (2005) Verification and planning for stochastic processes with asynchronous events. PhD thesis, Carnegie Mellon Google Scholar
  28. 28.
    Younes HLS (2005) Ymer: A statistical model checker. In: CAV. Lecture notes in computer science, vol 3576. Springer, Berlin, pp 429–433 Google Scholar
  29. 29.
    Younes HLS (2006) Error control for probabilistic model checking. In: VMCAI. Lecture notes in computer science, vol 3855. Springer, Berlin, pp 142–156 Google Scholar
  30. 30.
    Younes HLS, Simmons RG (2002) Probabilistic verification of discrete event systems using acceptance sampling. In: CAV. Lecture notes in computer science, vol 2404. Springer, Berlin, pp 223–235 Google Scholar
  31. 31.
    Younes HLS, Simmons RG (2006) Statistical probabilistic model checking with a focus on time-bounded properties. Inf Comput 204(9):1368–1409 MATHCrossRefMathSciNetGoogle Scholar

Copyright information

© Springer Science+Business Media, LLC 2009

Authors and Affiliations

  1. 1.Carnegie Mellon UniversityComputer Science DepartmentPittsburghUSA
  2. 2.VERIMAG LaboratoryGièresFrance
  3. 3.INRIA RennesComputer Science DepartmentRennesFrance

Personalised recommendations