To: seminaire@pauillac.inria.fr From: Francois.Pottier@inria.fr Subject: SEM - INRIA : Gallium - 22/03/06 - Paris - FR Vous pouvez vous abonner à nos annonces de séminaires http://pauillac.inria.fr/seminaires/subscribe.html S E M I N A I R E __ / _` _ / / o /| /| __ __ __ __ _ _ / ) __) / / / / / /\/| ----- / |/ | / )(_ / / ) ) ) __) (___/ (_/ (_ (_ / (__/ / | / | (__/ __)(_ (__/ (_/ (_/ I N R I A - Rocquencourt Amphi Turing du bâtiment 1 MERCREDI 22 mars, 10h30 ------------ John O'Leary ------------ Intel Corporation ========================================== Using a reflective functional language for hardware verification and theorem proving ========================================== In the last ten years formal methods have seen substantial use at Intel. Among our success stories is the formal verification of floating-point operations implemented in x86 hardware. Our tools and methods have been applied in a number of design projects, including the Pentium (R) 4 processor. In the Pentium 4 design we were able to capture several extremely subtle bugs that eluded simulation-based validation efforts - any of these bugs could have resulted in an expensive and embarrassing recall. Formal verification is now viewed as an essential component of any CPU design project. This talk will give an overview of our approach to formal hardware verification, which uses a combination of model checking (symbolic trajectory evaluation) and higher-order logic theorem proving. I will then focus on two key supporting tools. reFLect is a functional programming language that we use for writing specifications, building tools, and scripting. reFLect is strongly typed and similar to ML, but has quotation and antiquotation constructs that may be used to construct and decompose expressions in the reFLect language itself. Goaled is a higher order logic theorem prover we built for reasoning about reFLect programs. Using reFLect as both object language and meta language gives us the capability to perform "proof by evaluation" and we use this to advantage in rewriting and decision procedures.