Abstract modeling has been widely used, albeit independently, for both formal verification and high-level modeling of SoC designs. In this paper we show that proper selection of modeling language and abstraction level can make the same code useful for both formal and simulation-based techniques. The abstract model enables architecture exploration and the development of verification collateral pre-RTL, and can be used as a behavioral checker in simulation against the RTL and in hardware emulation. In parallel, it enables applying formal verification techniques to verify the specification and implementation of the design. We provide examples of the successful application of abstract models developed in SystemVerilog in the course of the verification of the newest Intel® Core™ 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.

Functional coverage is a well known means of measuring verification progress. However, approaches to coverage, such as Coverage Driven and Coverage Oriented approaches, are often difficult or impractical to implement. This paper presents the coverage methodology used in the verification of Merom, Intel's first converged-core microprocessor. We describe practical methods and applied techniques which enabled a high return on a significantly reduced investment in coverage measurement and analysis.Given the tight schedule, this approach provided a clear metric for measuring verification progress and for effectively steering resources to improve the quality of the design under test.

The growing complexity of state-of-art microprocessors dictates the use of cost-effective verification methods. Functional coverage was widely applied in the verification of Banias, Intel’s new IA-32 microprocessor designed solely for the mobile computing market. In this paper, we describe the practical coverage approach as was carried out in the verification of Banias. According to this Coverage-Oriented verification approach, focus shifts gradually from basic logic cleanup using random testing, where verification follows a predefined test plan, to coverage-driven verification, where verification resources are steered to hit coverage holes. This practical approach enables reaching higher quality for lower effort under a tightened schedule, and provides a clear metric to measure the progress of verification and the quality of the design under test. As the conclusions will show, the retrospective evaluation of this approach shed light on its significant impact beyond original intentions, as well as uncovering several potential areas for refinement that will make this approach even more effective on future projects.