Title :
Practical formal verification in microprocessor design
Author :
Jones, Robert B. ; O´leary, John W. ; Seger, Carl-Johan H. ; Aagaard, Mark D. ; Melham, Thomas F.
Author_Institution :
Intel Corp., Hillsboro, OR, USA
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
Keywords :
formal verification; logic design; microprocessor chips; theorem proving; IEEE-compliant floating-point adder; customizable framework; data-path-dominated hardware; formal methods; formal verification; large-scale industrial trials; microprocessor design; model checking; theorem proving; verification methodology; Acoustical engineering; Adders; Circuit simulation; Circuit testing; Debugging; Design engineering; Documentation; Formal verification; Large-scale systems; Microprocessors;
Journal_Title :
Design & Test of Computers, IEEE
