More Web Proxy on the site http://driver.im/

Article

Statistical Model Checking of Mixed-Analog Circuits with an Application to a Third Order Δ – Σ Modulator

Authors:

Alexandre Donzé,

Axel LegayAuthors Info & Claims

HVC '08: Proceedings of the 4th International Haifa Verification Conference on Hardware and Software: Verification and Testing

Pages 149 - 163

https://doi.org/10.1007/978-3-642-01702-5_16

Published: 19 April 2009 Publication History

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) quantities. We follow the statistical Model Checking approach of [You05, You06] that consists of evaluating the property on a representative subset of behaviors, generated by simulation, and answering the question of whether the circuit satisfies the property with a probability greater than or equal to some value. The answer is correct up to a certain probability of error, which is pre-specified. The method automatically determines the minimal number of simulations needed to achieve the desired accuracy, thus providing a convenient way to control the trade-off between precision and computational cost. 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. Our logic is unique in that it allows us to compare the Fourier transform of two signals. We demonstrate the applicability of the method on a model of a third order <em>Δ</em> *** <em>Σ</em> modulator for which previous formal verification attempts were too conservative and required excessive computation time.

References

[1]

Aziz, P.M., Sorensen, H.V., Van Der Spiegel, J.: An overview of sigmadelta converters. IEEE Signal Processing Magazine, 61-84 (January 1996)

[2]

Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P.: Model-checking algorithms for continuous-time markov chains. IEEE Trans. Software Eng. 29(6), 524-541 (2003)

[3]

Ciesinski, F., Baier, C.: Liquor: A tool for qualitative and quantitative linear time analysis of reactive systems. In: QEST, pp. 131-132. IEEE, Los Alamitos (2006)

[4]

Ciesinski, F., Größer, M.: On probabilistic computation tree logic. In: Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P., Siegle, M. (eds.) Validation of Stochastic Systems. LNCS, vol. 2925, pp. 147-188. Springer, Heidelberg (2004)

[5]

Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification. Journal of the ACM 42(4), 857-907 (1995)

[6]

Dang, T., Donze, A., Maler, O.: Verification of analog and mixed-signal circuits using hybrid systems techniques. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol. 3312, pp. 21-36. Springer, Heidelberg (2004)

[7]

d'Amorim, M., Roşu, G.: Efficient monitoring of ω-languages. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 364-378. Springer, Heidelberg (2005)

[8]

Legay Edmund Clarke, A., Donzé, A.: Statistical model checking of mixedanalog circuits. In: Second Workshop on Formal Verification of Analog Circuits of CAV 2008 (July 2008)

[9]

Frigo, M., Johnson, S.G.: The fastest Fourier transform in the west. Technical Report MIT-LCS-TR-728, Massachusetts Institute of Technology (September 1997)

[10]

Gupta, S., Krogh, B.H., Rutenbar, R.A.: Towards formal verification of analog designs. In: ICCAD, pp. 210-217 (2004)

[11]

Hérault, T., Lassaigne, R., Magniette, F., Peyronnet, S.: Approximate probabilistic model checking. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 73-84. Springer, Heidelberg (2004)

[12]

Kwiatkowska, M.Z., Norman, G., Parker, D.: Prism 2.0: A tool for probabilistic model checking. In: QEST, pp. 322-323. IEEE, Los Alamitos (2004)

[13]

Bauer, A., Leucker, M., Schallhart, C.: Monitoring of real-time properties. In: Arun-Kumar, S., Garg, N. (eds.) FSTTCS 2006. LNCS, vol. 4337, pp. 260-272. Springer, Heidelberg (2006)

[14]

Maler, O., Nickovic, D., Pnueli, A.: Checking temporal properties of discrete, timed and continuous behaviors. In: Avron, A., Dershowitz, N., Rabinovich, A. (eds.) Pillars of Computer Science. LNCS, vol. 4800, pp. 475-505. Springer, Heidelberg (2008)

[15]

Medeiro, F., Pérez-Verdú, B., Rodríguez-Vázquez, A.: Top-Down Design of High-Performance Sigma-Delta Modulators, ch. 2. Kluwer Academic Publishers, Dordrecht (2001)

[16]

Nickovic, D., Maler, O.: Amt: A property-based monitoring tool for analog systems. In: Raskin, J.-F., Thiagarajan, P.S. (eds.) FORMATS 2007. LNCS, vol. 4763, pp. 304-319. Springer, Heidelberg (2007)

[17]

Zakhor, A., Hein, S.: On the stability of sigma delta modulators. IEEE Transactions on Signal Processing 41 (July 1993)

[18]

Smith, S.W.: The scientist and engineer's guide to digital signal processing. California Technical Publishing, San Diego (1997)

[19]

Sen, K., Viswanathan, M., Agha, G.: Statistical model checking of black-box probabilistic systems. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 202-215. Springer, Heidelberg (2004)

[20]

Sen, K., Viswanathan, M., Agha, G.: On statistical model checking of stochastic systems. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 266-280. Springer, Heidelberg (2005)

[21]

Wald, A.: Sequential tests of statistical hypotheses. Annals of Mathematical Statistics 16(2), 117-186 (1945)

[22]

Younes, H.L.S., Kwiatkowska, M.Z., Norman, G., Parker, D.: Numerical vs. statistical probabilistic model checking. STTT 8(3), 216-228 (2006)

[23]

Younes, H.L.S.: Verification and Planning for Stochastic Processes with Asynchronous Events. Ph.D thesis, Carnegie Mellon (2005)

[24]

Younes, H.L.S.: Error control for probabilistic model checking. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 142-156. Springer, Heidelberg (2005)

[25]

Younes, H.L.S., Simmons, R.G.: Statistical probabilistic model checking with a focus on time-bounded properties. Information and Computation 204(9), 1368-1409 (2006)

Cited By

Chakarov ASankaranarayanan S(2013)Probabilistic Program Analysis with MartingalesProceedings of the 25th International Conference on Computer Aided Verification - Volume 804410.5555/2958031.2958114(511-526)Online publication date: 13-Jul-2013
https://dl.acm.org/doi/10.5555/2958031.2958114
Sankaranarayanan SChakarov AGulwani S(2013)Static analysis for probabilistic programsACM SIGPLAN Notices10.1145/2499370.246217948:6(447-458)Online publication date: 16-Jun-2013
https://dl.acm.org/doi/10.1145/2499370.2462179
Sankaranarayanan SChakarov AGulwani SBoehm HFlanagan C(2013)Static analysis for probabilistic programsProceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/2491956.2462179(447-458)Online publication date: 16-Jun-2013
https://dl.acm.org/doi/10.1145/2491956.2462179
Show More Cited By

Statistical Model Checking of Mixed-Analog Circuits with an Application to a Third Order Δ – Σ Modulator
1. Theory of computation

Recommendations

Analog circuit verification by statistical model checking
ASPDAC '11: Proceedings of the 16th Asia and South Pacific Design Automation Conference

We show how statistical Model Checking can be used for verifying properties of analog circuits. As integrated circuit technologies scale down, manufacturing variations in devices make analog designs behave like stochastic systems. The problem of ...
On simulation-based probabilistic model checking of mixed-analog circuits

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 ...
Symbolic Model Checking of Analog/Mixed-Signal Circuits
ASP-DAC '07: Proceedings of the 2007 Asia and South Pacific Design Automation Conference

This paper presents a Boolean based symbolic model checking algorithm for the verification of analog/mixed-signal (AMS) circuits. The systems are modeled in VHDL-AMS, a hardware description language for AMS circuits. The VHDL-AMS description is compiled ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

HVC '08: Proceedings of the 4th International Haifa Verification Conference on Hardware and Software: Verification and Testing

April 2009

214 pages

ISBN:9783642017018

Editors:
Hana Chockler
IBM Haifa Labs, Haifa University Campus, Mount Carmel, Haifa, Israel 31905
,
Alan J. Hu
Department of Computer Science, University of British Columbia, Vancouver, Canada

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 19 April 2009

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

12
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 10 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Chakarov ASankaranarayanan S(2013)Probabilistic Program Analysis with MartingalesProceedings of the 25th International Conference on Computer Aided Verification - Volume 804410.5555/2958031.2958114(511-526)Online publication date: 13-Jul-2013
https://dl.acm.org/doi/10.5555/2958031.2958114
Sankaranarayanan SChakarov AGulwani S(2013)Static analysis for probabilistic programsACM SIGPLAN Notices10.1145/2499370.246217948:6(447-458)Online publication date: 16-Jun-2013
https://dl.acm.org/doi/10.1145/2499370.2462179
Sankaranarayanan SChakarov AGulwani SBoehm HFlanagan C(2013)Static analysis for probabilistic programsProceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/2491956.2462179(447-458)Online publication date: 16-Jun-2013
https://dl.acm.org/doi/10.1145/2491956.2462179
Gui LSun JLiu YSi YDong JWang XPezzè MHarman M(2013)Combining model checking and testing with an application to reliability prediction and distributionProceedings of the 2013 International Symposium on Software Testing and Analysis10.1145/2483760.2483779(101-111)Online publication date: 15-Jul-2013
https://dl.acm.org/doi/10.1145/2483760.2483779
Abbas HFainekos GSankaranarayanan SIvančić FGupta A(2013)Probabilistic Temporal Logic Falsification of Cyber-Physical SystemsACM Transactions on Embedded Computing Systems10.1145/2465787.246579712:2s(1-30)Online publication date: 1-May-2013
https://dl.acm.org/doi/10.1145/2465787.2465797
Sankaranarayanan SFainekos GDang TMitchell I(2012)Falsification of temporal properties of hybrid systems using the cross-entropy methodProceedings of the 15th ACM international conference on Hybrid Systems: Computation and Control10.1145/2185632.2185653(125-134)Online publication date: 17-Apr-2012
https://dl.acm.org/doi/10.1145/2185632.2185653
Kim YKim MKim T(2012)Statistical model checking for safety critical hybrid systemsProceedings of the 8th international conference on Hardware and Software: verification and testing10.1007/978-3-642-39611-3_18(162-177)Online publication date: 6-Nov-2012
https://dl.acm.org/doi/10.1007/978-3-642-39611-3_18
Wang YKomuravelli AZuliani PClarke E(2011)Analog circuit verification by statistical model checkingProceedings of the 16th Asia and South Pacific Design Automation Conference10.5555/1950815.1950816(1-6)Online publication date: 25-Jan-2011
https://dl.acm.org/doi/10.5555/1950815.1950816
Legay ADelahaye BBensalem S(2010)Statistical model checkingProceedings of the First international conference on Runtime verification10.5555/1939399.1939412(122-135)Online publication date: 1-Nov-2010
https://dl.acm.org/doi/10.5555/1939399.1939412
Narayanan RAkbarpour BZaki MTahar SPaulson LDe Micheli GAl-Hashimi BMueller WMacii E(2010)Formal verification of analog circuits in the presence of noise and process variationProceedings of the Conference on Design, Automation and Test in Europe10.5555/1870926.1871240(1309-1312)Online publication date: 8-Mar-2010
https://dl.acm.org/doi/10.5555/1870926.1871240
Show More Cited By

View Options

View options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents