MRS Award‎ > ‎

2013 Microsoft Research Verified Software Milestone Award Citation

The Microsoft Research Verified Software Milestone Award is made to Roope Kaivola (Intel Corporation, Oregon, USA) with regards to the Intel Core i7 verification project.  While formal methods were applied within a number of areas of the Core i7 project, the award is being given in recognition for Kaivola's role as intellectual leader of the core execution cluster as well as his leadership of the verification team.

The core execution cluster is responsible for the functional behaviour of all microinstructions. The approach taken involved symbolic simulation based formal verification techniques, encompassing full data path, control and state validation for the execution cluster. The formal verification removed the need for conventional coverage driven testing. The project established a "gold standard" for verifying arithmetic functionality across Intel, and propagated it to many other CPU and GPU projects.  The scale of the i7 project is unprecedented within the industry, and serves to show the value added that formal methods can bring to the industrial scale verification and validation challenges.  The Core i7 project represents some twenty person years of effort so Roope's award also reflects the efforts of his team, both technical and

Roope Kaivola, Rajnish Ghughal, Naren Narasimhan, Amber Telfer, Jesse Whittemore, Sudhindra Pandav, Anna Slobodova, Christopher Taylor, Vladimir Frolov, Erik Reeber, and Armaghan Naik. 2009. 
Replacing Testing with Formal Verification in Intel Core TM i7 Processor Execution Engine ValidationIn Proceedings of the 21st International Conference on Computer Aided Verification (CAV '09), Ahmed Bouajjani and Oded Maler (Eds.). Springer-Verlag, Berlin, Heidelberg, 414-429.