Formal Verification of the Pentium? 4 Floating-Point Multiplier

	This Article
	Subscribers, please Login Purchase article: $19 PDF 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 R. Kaivola Articles by N. Narasimhan

2002 Design, Automation and Test in Europe Conference and Exhibition (DATE'02)

Paris, France

March 04-March 08

ISBN: 0-7695-1471-5

	ASCII Text	x
	R. Kaivola, N. Narasimhan, "Formal Verification of the Pentium? 4 Floating-Point Multiplier," Design, Automation and Test in Europe Conference and Exhibition, pp. 0020, 2002 Design, Automation and Test in Europe Conference and Exhibition (DATE'02), 2002.

	BibTex	x
	@article{ 10.1109/DATE.2002.998245, author = {R. Kaivola and N. Narasimhan}, title = {Formal Verification of the Pentium? 4 Floating-Point Multiplier}, journal ={Design, Automation and Test in Europe Conference and Exhibition}, volume = {0}, year = {2002}, isbn = {0-7695-1471-5}, pages = {0020}, doi = {http://doi.ieeecomputersociety.org/10.1109/DATE.2002.998245}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }

	RefWorks Procite/RefMan/Endnote	x
	TY - CONF JO - Design, Automation and Test in Europe Conference and Exhibition TI - Formal Verification of the Pentium? 4 Floating-Point Multiplier SN - 0-7695-1471-5 SP EP A1 - R. Kaivola, A1 - N. Narasimhan, PY - 2002 VL - 0 JA - Design, Automation and Test in Europe Conference and Exhibition ER -

R. Kaivola

N. Narasimhan

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/DATE.2002.998245

We present the formal verification of the floating-point multiplier in the Intel IA-32 Pentium ® microprocessor. The verification is based on a combination of theorem-proving and BDD based model-checking tasks performed in a unified hardware verification environment. The tasks are tightly integrated to accomplish complete verification of the multiplier hardware coupled with the rounder logic. The approach does not rely on specialized representations like Binary Moment Diagrams or its variants.

Citation:

R. Kaivola, N. Narasimhan, "Formal Verification of the Pentium? 4 Floating-Point Multiplier," date, pp.0020, 2002 Design, Automation and Test in Europe Conference and Exhibition (DATE'02), 2002

Peer Review Notice | Give Us Feedback

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