Limor Fix Intel Corporation

Formal Verification in Intel – Specification, Coverage, and Engines

In the last few years, formal verification tools have become mainstream in verifying the functional correctness of hardware. In this talk, the formal temporal specification language used in Intel will be described both from the point of view of its semantics, and the expressability and methodology of using it. The talk will also cover recent research and deployment of formal coverage tools aimed at ensuring enough specifications/properties haven been developed. Finally, the talk will cover recent algorithmic development in the formal verification engines.

Bio:

Limor has a Ph.D. in Computer Science from Technion in Israel. After graduation, Limor conducted post-doc research at Cornell University and then joined Intel in Israel. During 1994-2004, Limor led a major change in Intel’s validation methodology.  She developed innovative formal verification tools and methodology that have been widely adopted by Intel’s design teams.  In 2005, Limor joined the Intel Laboratory at CMU and she is co-managing the lab in the role of Associate Director. Limor currently explores formal verification technologies in the context of multi-core and she is serving on DAC’s Executive Committee.