skip to main content
10.1145/1228784.1228899acmconferencesArticle/Chapter ViewAbstractPublication PagesglsvlsiConference Proceedingsconference-collections
Article

Three-valued automated reasoning on analog properties

Published: 11 March 2007 Publication History

Abstract

We deal with the problem of designing suitable languages for the modeling and the automatic verification of properties over analog circuits. To this purpose, we suitably enrich classical temporal logics with basic formul\ae allowing to model arbitrary functions relating analog variables. We show how to automatically check the resulting CTLf formulæ on analog circuits. In particular, we rely on interval arithmetic methods and we extend to the analog context a number of techniques for the abstraction and the verification of digital systems, based on three-valued temporal logics.

References

[1]
G. Bruns et al, "Model Checking Partial State Spaces with Three Valued Temporal Logics," LNCS Proc. of the 13th Conference on Computer Aided Verification, 2001.
[2]
E. Clarke et al, "Model Checking," MIT Press, 1999.
[3]
E. Clarke et al, "Design and synthesis of synchronization skeletons using brancing time temporal logic," LNCS Proc. of Workshop on Logic of Programs, 1999.
[4]
P. Gray et al, "Analysis and Design of Analog Integrated Circuits," John Wiley & Sons Inc., 1993.
[5]
W. Hartong et al, "Model checking algorithms for analog verification," Proc. of the 39th Conference on Design Automation (DAC'02), 2002.
[6]
E. Hennig, "Symbolic Approximation and Modeling Techniques for Analysis and Design of Analog Circuits," Shaker Verlag, 2000.
[7]
T. Henzinger et al, "What's decidable about hybrid automata?," ACM Proc. of the 27th Annual Symposium on Theory of Computing, 1995.
[8]
L. Jaulin et al, "Applied Interval Analysis," Springer Verlag, 2001.
[9]
K. Schneider, "Verification of Reactive Systems," Springer Verlag, 2004.
[10]
R. Sommer et al, "A Generic Circuit Modelling Strategy Combining Symbolic and Numerical Analisys," Proc. of the 5th Int. Workshop on on Symbolic Methods and Applications to Circuit Design (SMCAD'98), 1998.
[11]
R. Sommer et al, "Analog Insydes 2 - New Features and Applications in Circuit Design," Proc. 6th Int. Workshop on Symbolic Methods and Applications in Circuit Design (SMACD 2000), 2000.

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences
GLSVLSI '07: Proceedings of the 17th ACM Great Lakes symposium on VLSI
March 2007
626 pages
ISBN:9781595936059
DOI:10.1145/1228784
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

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 11 March 2007

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. (multi valued) temporal logics & model checking
  2. analog circuits
  3. interval arithmetic

Qualifiers

  • Article

Conference

GLSVLSI07
Sponsor:
GLSVLSI07: Great Lakes Symposium on VLSI 2007
March 11 - 13, 2007
Stresa-Lago Maggiore, Italy

Acceptance Rates

Overall Acceptance Rate 312 of 1,156 submissions, 27%

Upcoming Conference

GLSVLSI '25
Great Lakes Symposium on VLSI 2025
June 30 - July 2, 2025
New Orleans , LA , USA

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • 0
    Total Citations
  • 106
    Total Downloads
  • Downloads (Last 12 months)0
  • Downloads (Last 6 weeks)0
Reflects downloads up to 27 Jan 2025

Other Metrics

Citations

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media