research-article

Analog circuit verification by statistical model checking

Authors:

Ying-Chih Wang,

Anvesh Komuravelli,

Edmund M. ClarkeAuthors Info & Claims

ASPDAC '11: Proceedings of the 16th Asia and South Pacific Design Automation Conference

Pages 1 - 6

Published: 25 January 2011 Publication History

Abstract

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 verifying stochastic systems is often difficult because of their large state space. Statistical Model Checking can be an efficient verification technique for stochastic systems. In this paper, we use sequential statistical techniques and model checking to verify properties of analog circuits in both the temporal and the frequency domain. In particular, randomly sampled system traces are sequentially generated by SPICE and passed to a trace checker to determine whether they satisfy a given specification, until the desired statistical strength is achieved.

References

[1]

E. M. Clarke, A. Donzé, and A. Legay, "Statistical model checking of mixed-analog circuits with an application to a third order delta-sigma modulator," in Haifa Verification Conference '08, ser. LNCS, vol. 5394, 2009, pp. 149--163.

Digital Library

[2]

P. Zuliani, A. Platzer, and E. M. Clarke, "Bayesian statistical model checking with application to Stateflow/Simulink verification," in HSCC, 2010, pp. 243--252.

Digital Library

[3]

H. L. S. Younes and R. G. Simmons, "Statistical probabilistic model checking with a focus on time-bounded properties," Inf. Comput., vol. 204, no. 9, pp. 1368--1409, 2006.

Digital Library

[4]

T. Hérault, R. Lassaigne, F. Magniette, and S. Peyronnet, "Approximate probabilistic model checking," in VMCAI, ser. LNCS, vol. 2937, 2004, pp. 73--84.

[5]

K. Sen, M. Viswanathan, and G. Agha, "Statistical model checking of black-box probabilistic systems," in CAV, ser. LNCS, vol. 3114, 2004, pp. 202--215.

[6]

C. Baier, E. M. Clarke, V. Hartonas-Garmhausen, M. Z. Kwiatkowska, and M. Ryan, "Symbolic model checking for probabilistic processes," in ICALP, ser. LNCS, vol. 1256, 1997, pp. 430--440.

Digital Library

[7]

C. Baier, B. R. Haverkort, H. Hermanns, and J.-P. Katoen, "Model-checking algorithms for continuous-time Markov chains," IEEE Trans. Software Eng., vol. 29, no. 6, pp. 524--541, 2003.

Digital Library

[8]

A. Pnueli, "The temporal logic of programs," in FOCS. IEEE, 1977, pp. 46--57.

Digital Library

[9]

R. Grosu and S. Smolka, "Monte Carlo Model Checking," in TACAS, ser. LNCS, vol. 3440, 2005, pp. 271--286.

Digital Library

[10]

A. Chutinan and B. H. Krogh, "Verification of polyhedral-invariant hybrid automata using polygonal flow pipe approximations," in HSCC, 1999, pp. 76--90.

Digital Library

[11]

S. Gupta, B. H. Krogh, and R. A. Rutenbar, "Towards formal verification of analog designs," in ICCAD, 2004, pp. 210--217.

Digital Library

[12]

S. Little, N. Seegmiller, D. Walter, C. J. Myers, and T. Yoneda, "Verification of analog/mixed-signal circuits using labeled hybrid petri nets," in ICCAD, 2006, pp. 275--282.

Digital Library

[13]

W. Denman, B. Akbarpour, S. Tahar, M. H. Zaki, and L. C. Paulson, "Formal verification of analog designs using metitarski," in FMCAD, 2009, pp. 93--100.

[14]

S. Little, D. Walter, K. Jones, and C. J. Myers, "Analog/mixed-signal circuit verification using models generated from simulation traces," in ATVA, 2007, pp. 114--128.

Digital Library

[15]

R. Narayanan, B. Akbarpour, M. H. Zaki, S. Tahar, and L. C. Paulson, "Formal verification of analog circuits in the presence of noise and process variation," in DATE, 2010, pp. 1309--1312.

Digital Library

Cited By

Song JJung YCho CJee EBae DHong JBures MPark JCerny T(2022)Statistical verification using learned usages for evaluating energy-efficient mobile device designProceedings of the 37th ACM/SIGAPP Symposium on Applied Computing10.1145/3477314.3507167(960-963)Online publication date: 25-Apr-2022
https://dl.acm.org/doi/10.1145/3477314.3507167
Zhang YSankaranarayanan SSomenzi FChen XÁbraham EHenkel J(2013)From statistical model checking to statistical model inferenceProceedings of the International Conference on Computer-Aided Design10.5555/2561828.2561958(662-669)Online publication date: 18-Nov-2013
https://dl.acm.org/doi/10.5555/2561828.2561958

Index Terms

Analog circuit verification by statistical model checking
1. Hardware

Recommendations

Sequential circuit verification using symbolic model checking
DAC '90: Proceedings of the 27th ACM/IEEE Design Automation Conference

The temporal logic model checking algorithm developed by Clarke, Emerson, and Sistla [9] is modified to represent a state graph using binary decision diagrams (BDD's) [4]. Because this representation captures some of the regularity in the state space of ...
Statistical model checking of Timed Rebeca models

The actor-based language, Timed Rebeca, was introduced to model distributed and asynchronous systems with timing constraints and message passing communication. A toolset was developed for automated translation of Timed Rebeca models to Erlang. The ...
Symbolic model checking for sequential circuit verification

The temporal logic model checking algorithm of Clarke, Emerson, and Sistla (1986) is modified to represent state graphs using binary decision diagrams (BDD's) and partitioned transition relations. Because this representation captures some of the ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ASPDAC '11: Proceedings of the 16th Asia and South Pacific Design Automation Conference

January 2011

841 pages

ISBN:9781424475162

Sponsors

IEEE
IPSJ
SIGDA: ACM Special Interest Group on Design Automation
IEICE ESS: Institute of Electronics, Information and Communication Engineers, Engineering Sciences Society
IEICE

Publisher

IEEE Press

Publication History

Published: 25 January 2011

Check for updates

Qualifiers

Research-article

Conference

ASPDAC '11

Sponsor:

SIGDA
IEICE ESS

ASPDAC '11: 16th Asia and South Pacific Design Automation Conference

January 25 - 28, 2011

Yokohama, Japan

Acceptance Rates

Overall Acceptance Rate 466 of 1,454 submissions, 32%

Upcoming Conference

ASPDAC '25

Sponsor:
sigda

30th Asia and South Pacific Design Automation Conference

January 20 - 23, 2025

Tokyo , Japan

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
251
Total Downloads

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

Reflects downloads up to 17 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Song JJung YCho CJee EBae DHong JBures MPark JCerny T(2022)Statistical verification using learned usages for evaluating energy-efficient mobile device designProceedings of the 37th ACM/SIGAPP Symposium on Applied Computing10.1145/3477314.3507167(960-963)Online publication date: 25-Apr-2022
https://dl.acm.org/doi/10.1145/3477314.3507167
Zhang YSankaranarayanan SSomenzi FChen XÁbraham EHenkel J(2013)From statistical model checking to statistical model inferenceProceedings of the International Conference on Computer-Aided Design10.5555/2561828.2561958(662-669)Online publication date: 18-Nov-2013
https://dl.acm.org/doi/10.5555/2561828.2561958

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

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents