The Community for Technology Leaders
Green Image
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
87 ms
(Ver 3.3 (11022016))