Verification Research + X = Impact

Add to your list(s) Download to your calendar using vCal

• Dr John O’Leary
• Wednesday 03 June 2015, 13:00-14:00
• FW26.

If you have a question about this talk, please contact Peter Sewell.

nonstandard room: FW26

It’s now been over twenty years since the FDIV flaw, an error in the register-transfer-level design of the Intel Pentium processor that was not detected by pre-silicon testing and that resulted in an expensive and embarrassing product recall. FDIV spurred adoption of formal datapath verification in industry, and in 2015 formal verification is in daily use at Intel and elsewhere. At Intel our CPU and graphics designs rely heavily (sometimes exclusively) on formal verification to ensure design correctness.

The industry success of formal datapath verification is due to the confluence of a pressing problem, timely academic research, and much engineering effort. This lecture will examine the path of datapath FV technology from research to “impact in the trenches”, and relate the lessons we learned.

Speaker biography:

John O’Leary is an Oliver Smithies Visiting Lecturer at Balliol College and a principal engineer at Intel Corporation, Hillsboro, USA . From 1987 to 1990, he worked in the CAD group at Bell-Northern Research, Ottawa. He received the Ph.D. degree in electrical engineering from Cornell University in 1995 and since then has held a variety of positions at Intel (most all involving the formal specification and verification of hardware).

This talk is part of the REMS lunch series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Department of Computer Science and Technology talks and seminars
• FW26
• Interested Talks
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31

Note that ex-directory lists are not shown.