Case study: Integrating FV and DV in the Verification of the Intel® Core^{TM} 2 Duo Microprocessor

The ever-growing complexity of Intel® CPUs, together with shortened time-to-market requirements, poses significant challenges for pre-silicon logic verification. To address the increasing verification gap, major improvements to verification practices are required. In Merom, the Intel® Core^{TM} 2 Duo microprocessor, we integrated Formal Verification (FV) with Dynamic Verification (DV) such that FV was also practiced by non-FV experts and replaced some traditional, simulation-based verification activities. This led to both higher productivity and better quality compared to previous projects. In this paper we report on the integration we used, including two examples, results, and future directions.