A Methodology for Large-Scale Hardware Verification

Mark Aagaard, Robert B Jones, Thomas F Melham, John W O'Leary and Carl-Johan H Seger

To appear at Formal Methods in Computer Aided Design (FMCAD00), Austin, Texas, November 1-3, 2000


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.

Server START Conference Manager
Update Time 26 Jun 2000 at 16:35:38
Maintainer sjohnson@cs.indiana.edu.
Start Conference Manager
Conference Systems