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 journalArticlepeer-review

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