Practical Formal Verification in Microprocessor Design

	This Article
	Subscribers, please Login Purchase article: $19 PDF HTML IEEE Xplore Subscribers RSS feed
	Share
	Email this Article to a friend
	Bibliographic References
	ASCII Text BibTex RefWorks Procite/RefMan/Endnote
	Add to:
	Digg Furl Spurl Blink Simpy Google Del.icio.us Y!MyWeb
	Search
	Similar Articles Articles by Robert B. Jones Articles by John W. O'Leary Articles by Carl-Johan H. Seger Articles by Mark D. Aagaard Articles by Thomas F. Melham

July/August 2001 (vol. 18 no. 4)

pp. 16-25

	ASCII Text	x
	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 and Test of Computers, vol. 18, no. 4, pp. 16-25, July/August, 2001.

	BibTex	x
	@article{ 10.1109/54.936245, author = {Robert B. Jones and John W. O'Leary and Carl-Johan H. Seger and Mark D. Aagaard and Thomas F. Melham}, title = {Practical Formal Verification in Microprocessor Design}, journal ={IEEE Design and Test of Computers}, volume = {18}, number = {4}, issn = {0740-7475}, year = {2001}, pages = {16-25}, doi = {http://doi.ieeecomputersociety.org/10.1109/54.936245}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }

	RefWorks Procite/RefMan/Endnote	x
	TY - MGZN JO - IEEE Design and Test of Computers TI - Practical Formal Verification in Microprocessor Design IS - 4 SN - 0740-7475 SP16 EP25 EPD - 16-25 A1 - Robert B. Jones, A1 - John W. O'Leary, A1 - Carl-Johan H. Seger, A1 - Mark D. Aagaard, A1 - Thomas F. Melham, PY - 2001 VL - 18 JA - IEEE Design and Test of Computers ER -

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.

Citation:

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 and Test of Computers, vol. 18, no. 4, pp. 16-25, July/Aug. 2001, doi:10.1109/54.936245

Peer Review Notice | Give Us Feedback

Usage of this product signifies your acceptance of the Terms of Use.