Complementary use of runtime validation and model checking

Ali Alphan Bayazit, Sharad Malik

Research output: Chapter in Book/Report/Conference proceedingConference contribution

32 Scopus citations

Abstract

The increasing gap between design complexity and compute power for verification necessitates radically new solutions to meet the verification challenges for future generations of hardware designs. Increasingly it will not be possible to completely validate hardware prior to fabrication. We will need to reconcile ourselves to the fact that hardware, like software, will be shipped with bugs. However, this can be acceptable with appropriate mechanisms for runtime validation that detect bugs and recover from them when needed. This paper takes a significant step in examining runtime validation as part of the verification methodology. It examines the strengths and weaknesses of runtime validation and how it may be used to complement model checking in a hybrid methodology. We consider the use of on-chip hardware for detecting bugs using hardware assertions. These assertions may be used for validating abstractions and assumptions for use in offline model checking. Hardware based assertions monitor properties at runtime and do not suffer from the state explosion problem. Offline model checking is used to validate globally distributed properties where runtime error detection has limitations in monitoring and responding to signals separated by many clock cycles. In this case the hardware based runtime validated abstractions and assumptions help in reducing the state space for model checking. Our ideas are demonstrated on a highly concurrent, yet simple to understand token sharing protocol, as well as a fairly complex cache coherence system.

Original languageEnglish (US)
Title of host publicationProceedings of theICCAD-2005
Subtitle of host publicationInternational Conference on Computer-Aided Design
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages1052-1059
Number of pages8
ISBN (Print)078039254X, 9780780392540
DOIs
StatePublished - 2005
EventICCAD-2005: IEEE/ACM International Conference on Computer-Aided Design, 2005 - San Jose, CA, United States
Duration: Nov 6 2005Nov 10 2005

Publication series

NameIEEE/ACM International Conference on Computer-Aided Design, Digest of Technical Papers, ICCAD
Volume2005
ISSN (Print)1092-3152

Other

OtherICCAD-2005: IEEE/ACM International Conference on Computer-Aided Design, 2005
CountryUnited States
CitySan Jose, CA
Period11/6/0511/10/05

All Science Journal Classification (ASJC) codes

  • Software
  • Computer Science Applications
  • Computer Graphics and Computer-Aided Design

Fingerprint Dive into the research topics of 'Complementary use of runtime validation and model checking'. Together they form a unique fingerprint.

  • Cite this

    Bayazit, A. A., & Malik, S. (2005). Complementary use of runtime validation and model checking. In Proceedings of theICCAD-2005: International Conference on Computer-Aided Design (pp. 1052-1059). [1560217] (IEEE/ACM International Conference on Computer-Aided Design, Digest of Technical Papers, ICCAD; Vol. 2005). Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1109/ICCAD.2005.1560217