Formal verification at Intel

Abstract

As designs become more complex, formal verificationtechniques are becoming increasingly important in thehardware industry. Many different methods are used, rangingfrom propositional tautology checking up to the use ofinteractive higher-order theorem provers. Our own work ismainly concerned with the formal verification of floating-pointmathematical functions. As this paper aims to illustrate,such applications require a rather general mathematicalframework and the ability to automate special-purposeproof algorithms in a reliable way. Our work uses thepublic-domain interactive theorem prover HOL Light, andwe claim that this and similar LCF-style' theorem proversare a good choice for such applications.