“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.
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.)