2002 Design, Automation and Test in Europe Conference and Exhibition (DATE'02) Formal Verification of the Pentium? 4 Floating-Point Multiplier Paris, France March 04-March 08 ISBN: 0-7695-1471-5
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 Usage of this product signifies your acceptance of the Terms of Use. | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb