🚀 go-pugleaf

Where:    Hamerschlag Hall 1112
When:     3:00-4:30 Wednesday Sept. 20
Contact: Shawn Blanton x8-2987
                 Roxann Martin   x8-3336

Title:  Microprocessor Verification at Intel

Abstract 
The cost of an error once a design has gone into production is extremely
expensive, witness the Pentium� processor's FDIV bug. Therefore, validation
is an integral step towards functional silicon. However, simulation alone
is not able to keep pace with design sizes and complexities increasing in
accordance with Moore's Law. Formal verification helps alleviate specific
design concerns and reduces the burden on traditional validation.

In this talk, I will explore the state of formal verification at Intel, as
it is applied to the next generation IA32 microprocessor, the Pentium� 4.
I will begin with an introduction to model checking and theorem proving and
continue on with a few examples of how this was applied to our work.

Bio
Katherine graduated from CMU with a BS in ECE/Econ in May 1997. Since
graduation,
she has been on the formal verification team, working on the
floating point
multiplier and divider of the Pentium� 4 microprocessor.