An industrially effective environment for formal hardware verification

Carl Johan H Seger, Robert B. Jones, John W. O'Leary, Tom Melham, Mark D. Aagaard, Clark Barrett, Don Syme

Research output: Contribution to journalArticle

Abstract

The Forte formal verification environment for datapath-dominated hardware is described. Forte has proven to be effective in large-scale industrial trials and combines an efficient linear-time logic model-checking algorithm, namely the symbolic trajectory evaluation (STE), with lightweight theorem proving in higher-order logic. These are tightly integrated in a general-purpose functional programming language, which both allows the system to be easily customized and at the same time serves as a specification language. The design philosophy behind Forte is presented and the elements of the verification methodology that make it effective in practice are also described.

Original languageEnglish (US)
Pages (from-to)1381-1404
Number of pages24
JournalIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems
Volume24
Issue number9
DOIs
StatePublished - Sep 2005

Keywords

  • BDDs
  • Formal verification
  • Model checking
  • Symbolic trajectory evaluation
  • Theorem proving

ASJC Scopus subject areas

  • Software
  • Computer Graphics and Computer-Aided Design
  • Electrical and Electronic Engineering

Fingerprint Dive into the research topics of 'An industrially effective environment for formal hardware verification'. Together they form a unique fingerprint.

  • Cite this

    Seger, C. J. H., Jones, R. B., O'Leary, J. W., Melham, T., Aagaard, M. D., Barrett, C., & Syme, D. (2005). An industrially effective environment for formal hardware verification. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 24(9), 1381-1404. https://doi.org/10.1109/TCAD.2005.850814