Practical formal verification in microprocessor design

Practical application of formal methods requires more than advanced technol ogy and tools; it requires an appropriate methodology, A verification metho dology for data-path-dominated hardware combines model checking and theorem proving in a customizable framework. This methodology has been effective i n large-scale industrial trials, including verification of an IEEE-complian t floating-point adder.