It will be a dry run of my presentation at DCC'2004.

Title: Formal Verification of Floating-point Multiply-Add on Intel (R)
Itanium(R) Processor.

I will describe our experience of applying formal methods to the
verification of floating point unit of the next generation Itanium (R)
processor. Besides IEEE standard mandated operations, Itanium ISA
includes the fused floating-point multiply-add instruction. Two operands
are multiplied to full precision, then the third operand is added and
the result is runded to the destination precision. To my knowldege,
there have been no reports on the verification of this operation so far.
In my presentation, I will focus on the specifics of the verification in
the industrial environment and methodology that we used in our project.

Anna