Abstract
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.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Aziz PM, Sorensen HV, Van Der Spiegel J (1996) An overview of sigma-delta converters. IEEE Signal Process Mag, pp 61–84, January 1996
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
Biere A, Heljanko K, Junttila TA, Latvala T, Schuppan V (2006) Linear encodings of bounded ltl model checking. Log Methods Comput Sci 2(5)
Ciesinski F, Baier C (2006) Liquor: A tool for qualitative and quantitative linear time analysis of reactive systems. In: QEST, IEEE, pp 131–132
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
Courcoubetis C, Yannakakis M (1995) The complexity of probabilistic verification. J ACM 42(4):857–907
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
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
Frigo M, Johnson SG (1997) The fastest Fourier transform in the west. Technical report MIT-LCS-TR-728, Massachusetts Institute of Technology, September 1997
Gupta S, Krogh BH, Rutenbar RA (2004) Towards formal verification of analog designs. In: ICCAD, pp 210–217
Kwiatkowska MZ, Norman G, Parker D (2004) Prism 2.0: A tool for probabilistic model checking. In: QEST, IEEE, pp 322–323
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
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
Maler O, Nickovic D, Pnueli A (2008) Checking temporal properties of discrete, timed and continuous behaviors. In: Pillars of computer science, pp 475–505
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
Nickovic D, Maler O (2007) Amt: A property-based monitoring tool for analog systems. In: FORMATS, pp 304–319
Pnueli A (1977) The temporal logic of programs. In: Proc. 18th annual symposium on foundations of computer science (FOCS), pp 46–57
Schreier R (2003) The delta-sigma toolbox version 6.0, January 2003
Zakhor A, Hein S (1993) On the stability of sigma delta modulators. IEEE Trans Signal Process, 41, July 1993
Smith SW (1997) The scientist and engineer’s guide to digital signal processing. California Technical Publishing, San Diego
Schreier R, Temes GC (2005) Understanding delta-sigma data converters. Wiley/IEEE Press, Hoboken
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
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
Wald A (1945) Sequential tests of statistical hypotheses. Ann Math Stat 16(2):117–186
Younes HLS, Kwiatkowska MZ, Norman G, Parker D (2006) Numerical vs. statistical probabilistic model checking. STTT 8(3):216–228
Younes HLS (2005) Probabilistic verification for “black-box” systems. In: CAV. Lecture notes in computer science, vol 3576. Springer, Berlin, pp 253–265
Younes HLS (2005) Verification and planning for stochastic processes with asynchronous events. PhD thesis, Carnegie Mellon
Younes HLS (2005) Ymer: A statistical model checker. In: CAV. Lecture notes in computer science, vol 3576. Springer, Berlin, pp 429–433
Younes HLS (2006) Error control for probabilistic model checking. In: VMCAI. Lecture notes in computer science, vol 3855. Springer, Berlin, pp 142–156
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
Younes HLS, Simmons RG (2006) Statistical probabilistic model checking with a focus on time-bounded properties. Inf Comput 204(9):1368–1409
Author information
Authors and Affiliations
Corresponding author
Additional information
This research was sponsored by the GSRC (University of California) under contract no. SA423679952, National Science Foundation under contracts no. CCF0429120, no. CNS0411152, and no. CCF0541245, Semiconductor Research Corporation under contract no. 2005TJ1366, Air Force (University of Vanderbilt) under contract no. 18727S3, International Collaboration for Advanced Security Technology of the National Science Council, Taiwan, under contract no. 1010717, and a grant from the Belgian American Educational Foundation.
Two preliminary versions of this paper appear in the Proceedings of the 4th Haifa Verification Conference and in the Proceedings of the 2nd Workshop on Formal Verification of Analog Circuits, respectively.
Rights and permissions
About this article
Cite this article
Clarke, E., Donzé, A. & Legay, A. On simulation-based probabilistic model checking of mixed-analog circuits. Form Methods Syst Des 36, 97–113 (2010). https://doi.org/10.1007/s10703-009-0076-y
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10703-009-0076-y