A Methodology for Large-Scale Hardware Verification

Abstract. We present a formal verification methodology for datapathdominated 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 IEEEcompliant, extended precision floating-point adder.

• Type: Conference
• Year: 2000
• Where: FMCAD
• Authors: Mark Aagaard, Robert B. Jones, Thomas F. Melham, John W. O'Leary, Carl-Johan H. Seger
• Keywords: FMCAD 2000, Formal Methods, Formal Verification Methodology, Large-scale Verification Efforts, Precision Floating-point Adder