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.
