An Industrially Effective Environment for Formal Hardware Verification

“An Industrially Effective Environment for Formal Hardware Verification” by Carl-Johan H. Seger, Robert B. Jones, John W. O'Leary, Tom Melham, Mark D. Aagaard, Clark Barrett, and Don Syme. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 24, no. 9, Sep. 2005, pp. 1381-1405.

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.

BibTeX entry:

@article{SJO+05,
   author = {Carl-Johan H. Seger and Robert B. Jones and John W. O'Leary
	and Tom Melham and Mark D. Aagaard and Clark Barrett and Don
	Syme},
   title = {An Industrially Effective Environment for Formal Hardware
	Verification},
   journal = {IEEE Transactions on Computer-Aided Design of Integrated
	Circuits and Systems},
   volume = {24},
   number = {9},
   pages = {1381--1405},
   month = sep,
   year = {2005},
   issn = {0278-0070},
   doi = {10.1109/TCAD.2005.850814},
   url = {http://theory.stanford.edu/~barrett/pubs/SJO+05.pdf}
}

(This webpage was created with bibtex2web.)