Issue No. 04 - July/August (2001 vol. 18)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/54.936245
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.
Thomas F. Melham, Mark D. Aagaard, Carl-Johan H. Seger, Robert B. Jones, John W. O'Leary, "Practical Formal Verification in Microprocessor Design", IEEE Design & Test of Computers, vol. 18, no. , pp. 16-25, July/August 2001, doi:10.1109/54.936245