Article

Verification of analog/mixed-signal circuits using labeled hybrid petri nets

Authors:

Nicholas Seegmiller,

Tomohiro YonedaAuthors Info & Claims

ICCAD '06: Proceedings of the 2006 IEEE/ACM international conference on Computer-aided design

Pages 275 - 282

https://doi.org/10.1145/1233501.1233556

Published: 05 November 2006 Publication History

Abstract

System on a chip design results in the integration of digital, analog, and mixed-signal circuits on the same substrate which further complicates the already difficult validation problem. This paper presents a new model, labeled hybrid Petri nets (LHPNs), that is developed to be capable of modeling such a heterogeneous set of components. This paper also describes a compiler from VHDL-AMS to LHPNs. To support formal verification, this paper presents an efficient zone-based state space exploration algorithm for LHPNs. This algorithm uses a process known as warping to allow zones to describe continuous variables that may be changing at variable rates. Finally, this paper describes the application of this algorithm to a couple of analog/mixed-signal circuit examples.

References

[1]

R. Alur, C. Courcoubetis, T. A. Henzinger, and P.-H. Ho. Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems. In R. L. Grossman, A. Nerode, A. P. Ravn, and H. Rischel, editors, Hybrid Systems, volume 736 of LNCS, pages 209--229. Springer, 1992.

Digital Library

[2]

W. Belluomini and C. J. Myers. Timed state space exploration using posets. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 19(5):501--520, May 2000.

Digital Library

[3]

W. Belluomini and C. J. Myers. Timed circuit verification using tel structures. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 20(1):129--146, Jan. 2001.

Digital Library

[4]

E. M. Clarke and R. P. Kurshan. Computer-aided verification. IEEE Spectrum, 33(6):61--67, June 1996.

Digital Library

[5]

T. Dang, A. Donze, and O. Maler. Verification of analog and mixed-signal circuits using hybrid systems techniques. In Formal Methods for Computer Aided Design, 2004.

[6]

R. David and H. Alla. On hybrid petri nets. Discrete Event Dynamic Systems: Theory and Applications, 11(1-2):9--40, Jan. 2001.

Digital Library

[7]

D. L. Dill. Timing assumptions and verification of finite-state concurrent systems. In J. Sifakis, editor, Proc. Automatic Verification Methods for Finite-State Systems, volume 407 of LNCS, pages 197--212. Springer, 1989.

Digital Library

[8]

G. Frehse. PHAVer: Algorithmic verification of hybrid systems past hytech. In M. Morari and L. Thiele, editors, Hybrid Systems: Computation and Control (HSCC), volume 3414 of LNCS, pages 258--273. Springer, 2005.

Digital Library

[9]

G. Frehse, B. H. Krogh, and R. A. Rutenbar. Verifying analog oscillator circuits using forward/backward refinement. In Proc. Design, Automation and Test in Europe (DATE), pages 257--262. IEEE Computer Society Press, 2006.

Digital Library

[10]

A. Ghosh and R. Vemuri. Formal verification of synthesized analog designs. In Proc. International Conf. on Computer Design (ICCD), pages 40--45. IEEE Computer Society Press, 1999.

Digital Library

[11]

S. Gupta, B. H. Krogh, and R. A. Rutenbar. Towards formal verification of analog designs. In Proc. International Conf. on Computer Aided Design (ICCAD), pages 210--217. IEEE Computer Society Press, 2004.

Digital Library

[12]

W. Hartong, L. Hedrich, and E. Barke. Model checking algorithms for analog verification. In Proc. Design Automation Conference (DAC), pages 542--547. ACM Press, 2002.

Digital Library

[13]

W. Hartong, L. Hedrich, and E. Barke. On discrete modeling and model checking for nonlinear analog systems. In E. Brinksma and K. G. Larsen, editors, Proc. International Conference on Computer Aided Verification (CAV), volume 2404 of LNCS, pages 401--413. Springer, 2002.

Digital Library

[14]

L. Hedrich and E. Barke. A formal approach to nonlinear analog circuit verification. In Proc. International Conf. on Computer Aided Design (ICCAD), pages 123--127. IEEE Computer Society Press, Nov. 1995.

Digital Library

[15]

L. Hedrich and E. Barke. A formal approach to verification of linear analog circuits with parameter tolerances. In Proc. Design, Automation and Test in Europe (DATE), pages 649--654. IEEE Computer Society Press, Feb. 1998.

Digital Library

[16]

S. Hendricx and L. Claesen. A symbolic core approach to the formal verification of integrated mixed-mode applications. In Proc. European Design and Test Conference, pages 432--436. IEEE Computer Society Press, 1997.

Digital Library

[17]

T. A. Henzinger, P.-H. Ho, and H. Wong-Toi. HYTECH: A model checker for hybrid systems. International Journal on Software Tools for Technology Transfer, 1(1-2):110--122, 1997.

Digital Library

[18]

S. Little, D. Walter, N. Seegmiller, C. Myers, and T. Yoneda. Verification of analog and mixed-signal circuits using timed hybrid petri nets. In Automated Technology for Verification and Analysis, volume 3299 of LNCS, pages 426--440. Springer, Nov. 2004.

[19]

C. Myers. Asynchronous Circuit Design. 2001.

[20]

C. J. Myers, R. R. Harrison, D. Walter, N. Seegmiller, and S. Little. The case for analog circuit verification. Electronic Notes Theoretical Computer Science., 153(3):53--63, 2006.

Digital Library

[21]

A. Salem. Semi-formal verification of VHDL-AMS descriptions. In Proc. International Symposium on Circuits and Systems (ISCAS), pages 123--127. IEEE Computer Society Press, 2002.

[22]

H. Zheng. Specification and compilation of timed systems. Master's thesis, University of Utah, 1998.

Cited By

Kaergel MOlbrich MBarke EDavid EOrdonez Mde Azevedo RKinget P(2014)Simulation Based Verification with Range Based Signal Representations for Mixed-Signal SystemsProceedings of the 27th Symposium on Integrated Circuits and Systems Design10.1145/2660540.2661010(1-7)Online publication date: 1-Sep-2014
https://dl.acm.org/doi/10.1145/2660540.2661010
Miller MBrewer FMacii E(2013)Formal verification of analog circuit parameters across variation utilizing SATProceedings of the Conference on Design, Automation and Test in Europe10.5555/2485288.2485631(1442-1447)Online publication date: 18-Mar-2013
https://dl.acm.org/doi/10.5555/2485288.2485631
Karthik ARoychowdhury J(2013)ABCD-LProceedings of the 50th Annual Design Automation Conference10.1145/2463209.2488811(1-9)Online publication date: 29-May-2013
https://dl.acm.org/doi/10.1145/2463209.2488811
Show More Cited By

Index Terms

Verification of analog/mixed-signal circuits using labeled hybrid petri nets
1. Hardware
  1. Hardware validation
    1. Functional verification

Recommendations

Verification of Analog/Mixed-Signal Circuits Using Labeled Hybrid Petri Nets

Mixed-signal designs integrate digital and analog circuits which complicates the already difficult verification problem. This paper presents a model, labeled hybrid Petri nets (LHPNs), that is developed to model this heterogeneous set of components. To ...
Efficient modeling and verification of analog/mixed-signal circuits using labeled hybrid petri nets
Verification of Analog/Mixed-Signal Circuits Using Symbolic Methods

This paper presents two symbolic model checking algorithms for the verification of analog/mixed-signal circuits. The first model checker utilizes binary decision diagrams while the second is a bounded model checker that uses a satisfiability modulo ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ICCAD '06: Proceedings of the 2006 IEEE/ACM international conference on Computer-aided design

November 2006

147 pages

ISBN:1595933891

DOI:10.1145/1233501

General Chair:
Soha Hassoun
Tufts Univ., Medford, MA

Copyright © 2006 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGDA: ACM Special Interest Group on Design Automation
IEEE-CAS: Circuits & Systems
IEEE-CS: Computer Society

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 05 November 2006

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

ICCAD06

Sponsor:

SIGDA
IEEE-CAS
IEEE-CS

ICCAD06: The International Conference on Computer-Aided Design 2006

November 5 - 9, 2006

California, San Jose

Acceptance Rates

Overall Acceptance Rate 457 of 1,762 submissions, 26%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

19
Total Citations
View Citations
303
Total Downloads

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

Reflects downloads up to 13 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Kaergel MOlbrich MBarke EDavid EOrdonez Mde Azevedo RKinget P(2014)Simulation Based Verification with Range Based Signal Representations for Mixed-Signal SystemsProceedings of the 27th Symposium on Integrated Circuits and Systems Design10.1145/2660540.2661010(1-7)Online publication date: 1-Sep-2014
https://dl.acm.org/doi/10.1145/2660540.2661010
Miller MBrewer FMacii E(2013)Formal verification of analog circuit parameters across variation utilizing SATProceedings of the Conference on Design, Automation and Test in Europe10.5555/2485288.2485631(1442-1447)Online publication date: 18-Mar-2013
https://dl.acm.org/doi/10.5555/2485288.2485631
Karthik ARoychowdhury J(2013)ABCD-LProceedings of the 50th Annual Design Automation Conference10.1145/2463209.2488811(1-9)Online publication date: 29-May-2013
https://dl.acm.org/doi/10.1145/2463209.2488811
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
Little SWalter DMyers CThacker RBatchu SYoneda T(2011)Verification of Analog/Mixed-Signal Circuits Using Labeled Hybrid Petri NetsIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2010.209745030:4(617-630)Online publication date: 1-Apr-2011
https://dl.acm.org/doi/10.1109/TCAD.2010.2097450
Ye QMacgregor M(2011)Using simulation to test formally verified protocols in complex environmentsMathematical and Computer Modelling: An International Journal10.1016/j.mcm.2010.03.03953:3-4(538-551)Online publication date: 1-Feb-2011
https://dl.acm.org/doi/10.1016/j.mcm.2010.03.039
Steinhorst SHedrich L(2011)Formal Methods for Verification of Analog CircuitsSimulation and Verification of Electronic and Biological Systems10.1007/978-94-007-0149-6_9(173-192)Online publication date: 2011
https://doi.org/10.1007/978-94-007-0149-6_9
Thacker RJones KMyers CZheng HSztipanovits JRajkumar R(2010)Automatic abstraction for verification of cyber-physical systemsProceedings of the 1st ACM/IEEE International Conference on Cyber-Physical Systems10.1145/1795194.1795197(12-21)Online publication date: 13-Apr-2010
https://dl.acm.org/doi/10.1145/1795194.1795197
Jones KKonrad VNičković D(2010)Analog property checkersFormal Methods in System Design10.1007/s10703-009-0085-x36:2(114-130)Online publication date: 1-Jun-2010
https://dl.acm.org/doi/10.1007/s10703-009-0085-x
Tiwary SGupta APhillips JPinello CZlatanovici RRoychowdhury J(2009)First steps towards SAT-based formal analog verificationProceedings of the 2009 International Conference on Computer-Aided Design10.1145/1687399.1687401(1-8)Online publication date: 2-Nov-2009
https://dl.acm.org/doi/10.1145/1687399.1687401
Show More Cited By

View Options

Get Access

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