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.
T. F. Melham, M. D. Aagaard, C. H. Seger, R. B. Jones and J. W. O'Leary, "Practical Formal Verification in Microprocessor Design," in IEEE Design & Test of Computers, vol. 18, no. , pp. 16-25, 2001.