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