Verification Research + X = Impact

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 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 his PhD 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).