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

Effective heuristics for counterexample-guided abstraction refinement

Published: 11 March 2007 Publication History

Abstract

Verification of complex system-on-a-chip (SoC) designs becomes a critical problem in practice. We consider using model checking to verify the correctness of such systems. We study the state separation problem in the framework of counterexample-guided abstraction refinement. We present two fast heuristics to solve this problem. To the best of our knowledge, our work is the first study on the effectiveness of greedy heuristics for this problem. In comparison with the latest work using the decision tree learning (DTL) solver, the proposed method performs about three orders of magnitude faster and the size of the separation set is 70% smaller on average.

References

[1]
E. Clarke, A. Gupta, and O. Strichman. SAT based counterexample-guided abstraction-refinement. IEEE Transactions on Computer Aided Design, 23(7):1113--1123, July 2004.
[2]
E. M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement. In Computer Aided Verification, pages 154--169, 2000.
[3]
M. Glusman, G. Kamhi, S. Mador-Haim, R. Fraer, and M. Y. Vardi. Multiple-counterexample guided iterative abstraction refinement: an industrial evaluation. In TACAS, pages 176--191, 2003.
[4]
S. G. Govindaraju and D. L. Dill. Counterexample-guided choice of projections in approximate symbolic model checking. In ICCAD, pages 115--119, 2000.
[5]
A. Gupta, M. K. Ganai, Z. Yang, and P. Ashar. Iterative abstraction using SAT-based BMC with proof analysis. In ICCAD, pages 416--423, 2003.
[6]
A. Gupta and O. Strichman. Abstraction refinement for bounded model checking. In Computer Aided Verification, pages 112--124, 2005.
[7]
T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Lazy abstraction. In Symposium on Principles of Programming Languages, pages 58--70, 2002.
[8]
R. P. Kurshan. Compter Aided Verification of coordinating Processes. Princeton University Press, 1994.
[9]
K. L. McMillan and N. Amla. Automatic abstraction without counterexamples. In TACAS, pages 2--17, 2003.
[10]
C. Wang, H. Jin, G. D. Hachtel, and F. Somenzi. Refining the SAT decision ordering for bounded model checking. In DAC, pages 535--538, 2004.

Cited By

View all
  • (2010)Integrating Evolutionary Computation with Abstraction Refinement for Model CheckingIEEE Transactions on Computers10.1109/TC.2009.10559:1(116-126)Online publication date: 1-Jan-2010

Index Terms

  1. Effective heuristics for counterexample-guided abstraction refinement

    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. SoC
    2. abstraction
    3. heuristics
    4. model checking
    5. verification

    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

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

    Other Metrics

    Citations

    Cited By

    View all
    • (2010)Integrating Evolutionary Computation with Abstraction Refinement for Model CheckingIEEE Transactions on Computers10.1109/TC.2009.10559:1(116-126)Online publication date: 1-Jan-2010

    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