BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Verification Research + X = Impact - Dr John O’Leary
DTSTART:20150603T120000Z
DTEND:20150603T130000Z
UID:TALK56533@talks.cam.ac.uk
CONTACT:Peter Sewell
DESCRIPTION:\nIt’s now been over twenty years since the FDIV flaw\, an e
 rror in the register-transfer-level design of the Intel Pentium processor 
 that was not detected by pre-silicon testing and that resulted in an expen
 sive and embarrassing product recall. FDIV spurred adoption of formal data
 path verification in industry\, and in 2015 formal verification is in dail
 y use at Intel and elsewhere. At Intel our CPU and graphics designs rely h
 eavily (sometimes exclusively) on formal verification to ensure design cor
 rectness.\n\nThe industry success of formal datapath verification is due t
 o the confluence of a pressing problem\, timely academic research\, and mu
 ch engineering effort. This lecture will examine the path of datapath FV t
 echnology from research to “impact  in the trenches”\, and relate the 
 lessons we learned.\n\nSpeaker biography:\n\nJohn O’Leary is an Oliver S
 mithies Visiting Lecturer at Balliol College and a principal engineer at I
 ntel Corporation\, Hillsboro\, USA. From 1987 to 1990\, he worked in the C
 AD group at Bell-Northern Research\, Ottawa. He received the Ph.D. degree 
 in electrical engineering from Cornell University in 1995 and since then h
 as held a variety of positions at Intel (most all involving the formal spe
 cification and verification of hardware).
LOCATION:FW26
END:VEVENT
END:VCALENDAR