Large-scale application of formal verification: From fiction to fact

Formal verification has matured considerably as a verification discipline in the past couple of decades, becoming a mainstream technology in industrial design and verification methodologies and processes. In this paper we chronicle the evolution of formal verification at IBM from being a specialized side activity with a narrow focus, to achieving a broad-based usage as a core verification technology helping to significantly improve design and verification productivity. We 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 IBM´s POWER7™ microprocessor and systems. We touch upon the methodology and execution aspects of the unprecedented use of formal verification on the POWER7 program, and depict ways in which the technology positively impacted pre-silicon design quality and facilitated root causing of bug escapes to silicon. Furthermore, we outline where we see applied formal verification evolving towards at IBM, and the challenges thereof.