Reference:

Robert B. Jones, John W. O'Leary, Carl-Johan H. Seger, Mark D. Aagaard, and Thomas F. Melham. Practical formal verification in microprocessor design. IEEE Design and Test, 18(4):18-25, July/August 2001.

Abstract:

Successful application of formal methods in the design of industrial hardware requires advanced technology and tools coupled with an appropriate methodology. We have developed a methodology for verification of datapath-dominated hardware that employs a combination of model checking and lightweight theorem proving. The methodology is realized in a framework with a general-purpose functional programming language that allows our tools to be easily customized. 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 not available
PDF

BibTeX entry:

@Article{JonesEtal01DesignAndTest,
  author    = {Robert B. Jones and 
               John W. O'Leary and
               Carl-Johan H. Seger and
               Mark D. Aagaard and
               Thomas F. Melham},
  title     = {Practical Formal Verification in Microprocessor Design},
  journal   = {IEEE Design and Test},
  volume    = 18,
  number    = 4,
  month     = {July/August},
  pages     = {18--25},
  year      = 2001,
}