Reference:

Mark D. Aagaard, Robert B. Jones, Thomas F. Melham, John W. O'Leary, and Carl-Johan H. Seger. A methodology for large-scale hardware verification. In Warren A. Hunt Jr. and Steven D. Johnson, editors, Formal Methods in Computer-Aided Design (FMCAD), volume 1954 of Lecture Notes in Computer Science, pages 263-282. Springer-Verlag, November 2000.

Abstract:

We present a formal verification methodology for datapath-dominated hardware. This provides a systematic but flexible framework within which to organize the activities undertaken in large-scale verification efforts and to structure the associated code and proof-script artifacts. The methodology deploys a combination of model checking and lightweight theorem proving in higher-order logic, tightly integrated within a general-purpose functional programming language that allows the framework to be easily customized and also serves as a specification language. We illustrate the methodology--which has has proved highly effective in large-scale industrial trials--with the verification of an IEEE-compliant, extended precision floating-point adder.

Download (please read copyright notice):

PostScript (gzipped)
PDF (auto-translated from PS, may have problems)

BibTeX entry:

@InProceedings{AagaardEtal00FMCAD,
  author    = {Mark D. Aagaard and
               Robert B. Jones and 
               Thomas F. Melham and
               John W. O'Leary and
               Carl-Johan H. Seger},
  title     = {A Methodology for Large-Scale Hardware Verification},
  pages     = {263--282},
  booktitle = {Formal Methods in Computer-Aided Design (FMCAD)},
  editor    = {Warren A. Hunt~Jr. and Steven D. Johnson},
  volume    = 1954,
  series    = {Lecture Notes in Computer Science},
  publisher = {Springer-Verlag},
  month     = {November},
  year      = 2000,
}