skip to main content
research-article

Auxiliary state machines + context-triggered properties in verification

Published: 03 October 2008 Publication History

Abstract

Formal specifications of interface protocols between a design-under-test and its environment mostly consist of two types of correctness requirements, namely (a) a set of invariants that applies throughout the protocol execution and (b) a set of context-triggered properties that applies only when the protocol state belongs to a specific set of contexts. To model such requirements, an increasingly popular design choice in the assertion IP design community has been the use of abstract context state machines and state-oriented properties. In this paper, we formalize this modeling style and present algorithms for verifying such specifications. Specifically, we present a purely formal approach and a semi-formal approach for verifying such specifications. We demonstrate the use of this design style in modeling some of the industry standard protocol descriptions and present encouraging results.

References

[1]
Börger, E. and Stärk, R. 2003. Abstract State Machines: A Method for High-Level System Design and Analysis. Springer-Verlag.
[2]
Biere, A., Cimatti, A., Clarke, E. M., and Zhu, Y. 1999. Symbolic model checking without bdds. In Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS'99). Springer-Verlag, 193--207.
[3]
Brayton, R. K., Hachtel, G. D., Sangiovanni-Vincentelli, A. L., and colleagues. 1996. Vis: A system for verification and synthesis. In Proceedings of the 8th International Conference on Computer Aided Verification (CAV'96). Springer-Verlag, 428--432.
[4]
Burch, J. R., Clarke, E. M., and Long, D. E. 1991. Representing circuits more efficiently in symbolic model checking. In Proceedings of the 28th Conference on ACM/IEEE Design Automation (DAC'91). ACM, 403--407.
[5]
Chauhan, P., Clarke, E. M., Lu, Y., and Wang, D. 1999. Verifying Ip-core based system-on-chip designs. In Proceedings of the ASIC Conference. 27--31.
[6]
Cho, H., Hachtel, G. D., Macii, E., Plessier, B., and Somenzi, F. 1993. Algorithms for approximate fsm traversal. In Proceedings of the 30th International Conference on Design Automation (DAC'93). ACM, 25--30.
[7]
Clarke, E. M., Emerson, E. A., and Sistla, A. P. 1986. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst. 8, 2, 244--263.
[8]
Dasgupta, P. 2006. A Roadmap for Formal Property Verification. Springer-Verlag.
[9]
Govindaraju, S. G. and Dill, D. L. 2000. Counterexample-guided choice of projections in approximate symbolic model checking. In Proceedings of the IEEE/ACM International Conference on Computer-Aided Design (ICCAD'00). IEEE Press, 115--119.
[10]
Kaufmann, M., Martin, A., and Pixley, C. 1998. Design constraints in symbolic model checking. In Proceedings of the 10th International Conference on Computer Aided Verification (CAV'98). Springer-Verlag, 477--487.
[11]
Nguyen, M. D., Stoffel, D., Wedler, M., and Kunz, W. 2005. Transition-by-transition fsm traversal for reachability analysis in bounded model checking. In Proceedings of the IEEE/ACM International Conference on Computer-Aided Design (ICCAD'05). IEEE Computer Society, 1068--1075.
[12]
Pnueli, A. 1977. The temporal logic of programs. In Proceedings of International Symposium on Foundations of Computer Science (FOCS'77). 46--57.
[13]
Sebastiani, R., Singerman, E., Tonetta, S., and Vardi, M. Y. 2007. GSTE is partitioned model checking. In Formal Methods in System Design. vol. 31, 177--196. Kluwar Academic Publishers.
[14]
Shimizu, K., Dill, D. L., and Chou, C.-T. 2001. A specification methodology by a collection of compact properties as applied to the intel® itaniumtm processor bus protocol. In Proceedings of the 11th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME'01). Springer-Verlag, 340--354.
[15]
Shimizu, K., Dill, D. L., and Hu, A. J. 2000. Monitor-based formal specification of pci. In Proceedings of the 3rd International Conference on Formal Methods in Computer-Aided Design (FMCAD'00). Springer-Verlag, 335--353.
[16]
Shyam, S. and Bertacco, V. 2006. Distance-guided hybrid verification with guido. In Proceedings of the Conference on Design, Automation and Test in Europe (DATE'06). European Design and Automation Association, 1211--1216.
[17]
Somenzi, F. 1998. Cudd: CU decision diagram package, release 2.3.0, User's Manual.
[18]
Yang, J. and Seger, C.-J. H. 2003. Introduction to generalized symbolic trajectory evaluation. IEEE Trans. Very Large Scale Integr. Syst. 11, 3, 345--353.

Cited By

View all
  • (2023)Analysis of Machine Learning Techniques for Time Domain Waveform Prediction in Analog and Mixed Signal Integrated Circuit Verification2023 24th International Symposium on Quality Electronic Design (ISQED)10.1109/ISQED57927.2023.10129327(1-9)Online publication date: 5-Apr-2023
  • (2019)Feature Indented Assertions for Analog and Mixed-Signal ValidationIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2016.252579835:11(1928-1941)Online publication date: 4-Jan-2019
  • (2019)Auxiliary Specifications for Context-Sensitive Monitoring of AMS AssertionsIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2011.215506530:10(1446-1457)Online publication date: 4-Jan-2019
  • Show More Cited By

Index Terms

  1. Auxiliary state machines + context-triggered properties in verification

    Recommendations

    Comments

    Information & Contributors

    Information

    Published In

    cover image ACM Transactions on Design Automation of Electronic Systems
    ACM Transactions on Design Automation of Electronic Systems  Volume 13, Issue 4
    September 2008
    328 pages
    ISSN:1084-4309
    EISSN:1557-7309
    DOI:10.1145/1391962
    Issue’s Table of Contents
    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]

    Publisher

    Association for Computing Machinery

    New York, NY, United States

    Journal Family

    Publication History

    Published: 03 October 2008
    Accepted: 01 April 2008
    Revised: 01 September 2007
    Received: 01 January 2007
    Published in TODAES Volume 13, Issue 4

    Permissions

    Request permissions for this article.

    Check for updates

    Qualifiers

    • Research-article
    • Research
    • Refereed

    Contributors

    Other Metrics

    Bibliometrics & Citations

    Bibliometrics

    Article Metrics

    • Downloads (Last 12 months)3
    • Downloads (Last 6 weeks)0
    Reflects downloads up to 15 Feb 2025

    Other Metrics

    Citations

    Cited By

    View all
    • (2023)Analysis of Machine Learning Techniques for Time Domain Waveform Prediction in Analog and Mixed Signal Integrated Circuit Verification2023 24th International Symposium on Quality Electronic Design (ISQED)10.1109/ISQED57927.2023.10129327(1-9)Online publication date: 5-Apr-2023
    • (2019)Feature Indented Assertions for Analog and Mixed-Signal ValidationIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2016.252579835:11(1928-1941)Online publication date: 4-Jan-2019
    • (2019)Auxiliary Specifications for Context-Sensitive Monitoring of AMS AssertionsIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2011.215506530:10(1446-1457)Online publication date: 4-Jan-2019
    • (2011)Auxiliary State Machines and Auxiliary FunctionsProceedings of the 2011 24th International Conference on VLSI Design10.1109/VLSID.2011.27(52-57)Online publication date: 2-Jan-2011
    • (2010)A study of modeling techniques in use in digital and mixed-signal domains for semi-formal verification2010 IEEE Students Technology Symposium (TechSym)10.1109/TECHSYM.2010.5469221(103-108)Online publication date: Apr-2010

    View Options

    Login options

    Full Access

    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