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

Fingerprint

Functional programming
Theorem proving
Specification languages
Model checking
Computer programming languages
Trajectories
Hardware
Formal verification

Keywords

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

ASJC Scopus subject areas

  • Electrical and Electronic Engineering
  • Hardware and Architecture
  • Computer Science Applications
  • Computational Theory and Mathematics

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

An industrially effective environment for formal hardware verification. / Seger, Carl Johan H; Jones, Robert B.; O'Leary, John W.; Melham, Tom; Aagaard, Mark D.; Barrett, Clark; Syme, Don.

In: IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, Vol. 24, No. 9, 09.2005, p. 1381-1404.

Research output: Contribution to journalArticle

Seger, Carl Johan H ; Jones, Robert B. ; O'Leary, John W. ; Melham, Tom ; Aagaard, Mark D. ; Barrett, Clark ; Syme, Don. / An industrially effective environment for formal hardware verification. In: IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems. 2005 ; Vol. 24, No. 9. pp. 1381-1404.
@article{bf47a1e65e504992aad0781e7efc68e9,
title = "An industrially effective environment for formal hardware verification",
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.",
keywords = "BDDs, Formal verification, Model checking, Symbolic trajectory evaluation, Theorem proving",
author = "Seger, {Carl Johan H} and Jones, {Robert B.} and O'Leary, {John W.} and Tom Melham and Aagaard, {Mark D.} and Clark Barrett and Don Syme",
year = "2005",
month = "9",
doi = "10.1109/TCAD.2005.850814",
language = "English (US)",
volume = "24",
pages = "1381--1404",
journal = "IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems",
issn = "0278-0070",
publisher = "Institute of Electrical and Electronics Engineers Inc.",
number = "9",

}

TY - JOUR

T1 - An industrially effective environment for formal hardware verification

AU - Seger, Carl Johan H

AU - Jones, Robert B.

AU - O'Leary, John W.

AU - Melham, Tom

AU - Aagaard, Mark D.

AU - Barrett, Clark

AU - Syme, Don

PY - 2005/9

Y1 - 2005/9

N2 - 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.

AB - 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.

KW - BDDs

KW - Formal verification

KW - Model checking

KW - Symbolic trajectory evaluation

KW - Theorem proving

UR - http://www.scopus.com/inward/record.url?scp=27644588866&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=27644588866&partnerID=8YFLogxK

U2 - 10.1109/TCAD.2005.850814

DO - 10.1109/TCAD.2005.850814

M3 - Article

AN - SCOPUS:27644588866

VL - 24

SP - 1381

EP - 1404

JO - IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems

JF - IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems

SN - 0278-0070

IS - 9

ER -