The Community for Technology Leaders
Green Image
ABSTRACT
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.
INDEX TERMS
CITATION

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.
doi:10.1109/54.936245
90 ms
(Ver 3.3 (11022016))