Title :
Formal verification of the PentiumLt;4 floating-point multiplier
Author :
Kaivola, Roope ; Narasimhan, Naren
Author_Institution :
Intel Corp., Hillsboro, OR, USA
Abstract :
We present the formal verification of the floating-point multiplier in the Intel IA-32 PentiumLt; 4 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
Keywords :
binary decision diagrams; floating point arithmetic; formal verification; microprocessor chips; multiplying circuits; theorem proving; BDD based model-checking tasks; Intel IA-32 microprocessor; Pentium4 floating-point multiplier; complete verification; formal verification; multiplier hardware; rounder logic; theorem proving; unified hardware verification environment; Binary decision diagrams; Boolean functions; Circuit faults; Circuit testing; Data structures; Design automation; Formal verification; Hardware; Logic; Microprocessors;
Conference_Titel :
Design, Automation and Test in Europe Conference and Exhibition, 2002. Proceedings
Conference_Location :
Paris
Print_ISBN :
0-7695-1471-5
DOI :
10.1109/DATE.2002.998245
