Practical formal verification in microprocessor design
Robert B. Jones, John W. O’Leary, C.-J.H. Seger, Mark D. Aagaard, Tom Melham · IEEE Design & Test of Computers · 2001
Practical application of formal methods requires more than advanced technology and tools; it requires an appropriate methodology. A verification methodology for data-path-dominated hardware combines model checking and theorem proving in a customizable framework. This methodology has been effective in large-scale industrial trials, including verification of an IEEE-compliant floating-point adder.