Automatic generation of invariants in processor verification

Jeffrey X. Su, David L. Dill, Clark W. Barrett

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

Abstract

A central task in formal verification is the definition of invariants, which characterize the reachable states of the system. When a system is finites state, invariants can be discovered automatically. Our experience in verifying microprocessors using symbolic logic is that finding adequate invariants is extremely time-consuming. We present three techniques for automating the discovery of some of these invariants. All of them are essentially syntactic transformations on a logical formula derived from the state transition function. The goal is to eliminate quantifiers and extract small clauses implied by the larger formula. We have implemented the method and exercised it on a description of the FLASH Protocol Processor (PP), a microprocessor designed at Stanford for handling communications in a multiprocessor. We had previously verified the PP by manually deriving invariants. Although the method is simple, it discovered 6 out of 7 of the invariants needed for verification of the CPU of the processor design, and 28 out of 72 invariants needed for verification of the memory system of the processor. We believe that, in the future, the discovery of invariants can be largely automated by a combination of different methods, including this one.

Original languageEnglish (US)
Title of host publicationFormal Methods in Computer-Aided Design - 1st International Conference, FMCAD 1996, Proceedings
EditorsAlbert Camilleri, Mandayam Srivas
PublisherSpringer Verlag
Pages377-388
Number of pages12
ISBN (Print)3540619372, 9783540619376
DOIs
StatePublished - 1996
Event1st International Conference on Formal Methods in Computer-Aided Design, FMCAD 1996 - Palo Alto, United States
Duration: Nov 6 1996Nov 8 1996

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume1166
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other1st International Conference on Formal Methods in Computer-Aided Design, FMCAD 1996
CountryUnited States
CityPalo Alto
Period11/6/9611/8/96

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Automatic generation of invariants in processor verification'. Together they form a unique fingerprint.

  • Cite this

    Su, J. X., Dill, D. L., & Barrett, C. W. (1996). Automatic generation of invariants in processor verification. In A. Camilleri, & M. Srivas (Eds.), Formal Methods in Computer-Aided Design - 1st International Conference, FMCAD 1996, Proceedings (pp. 377-388). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1166). Springer Verlag. https://doi.org/10.1007/BFb0031822