Invited Talk

Viresh Paruthi (IBM Austin) - Large-scale Formal Application: From Fiction to Fact

Formal verification has matured as a verification discipline in the past decade and half becoming mainstream in industrial design and verification methodologies and processes. In this talk we will chronicle evolution of formal verification at IBM over the years from being a specialized side activity with a narrow focus, to a broad-based use as a core verification technology helping to significantly improve overall design and verification productivity. We will showcase what is possible in the application of formal verification in a commercial/industrial setting by highlighting the success we had in leveraging the technology extensively on the POWER7 program. We will touch upon the methodology and execution aspects of the unprecedented use of formal verification on POWER7, and depict ways in which the technology positively impacted pre-silicon design quality and facilitated root causing of bug escapes to silicon. Furthermore, we will outline where we see formal verification evolving towards at IBM, and the challenges thereof.