Replacing Testing with Formal Verification in Intel CoreTM i7 Processor Execution Engine Validation
Replacing Testing with Formal Verification in Intel CoreTM i7 Processor Execution Engine Validation
复制标题
DOI：
10.1007/978-3-642-02658-4_32
复制
发表时间：
2009-06
期刊：
影响因子：
--
通讯作者：
Roope Kaivola;R. Ghughal;N. Narasimhan;Amber Telfer;J. Whittemore;S. Pandav;A. Slobodová;Christopher Taylor;V. Frolov;Erik Reeber;A. Naik
中科院分区：
文献类型：
--
作者：
Roope Kaivola;R. Ghughal;N. Narasimhan;Amber Telfer;J. Whittemore;S. Pandav;A. Slobodová;Christopher Taylor;V. Frolov;Erik Reeber;A. Naik
在过去几年中，算术数据路径的形式验证已成为大多数英特尔处理器设计的既定方法的一部分，通常用于补充更传统的面向覆盖率的测试活动。对于最近的英特尔$^{\tiny\circledR}$CoreTMi 7设计，我们更进一步，使用形式验证作为核心执行集群的主要验证工具，该组件负责所有微指令的功能行为。我们采用基于符号模拟的形式化验证技术对集群进行完整的数据路径、控制和状态验证，并完全放弃覆盖率驱动测试。该项目涉及约20人年的验证工作，是迄今为止硬件行业最雄心勃勃的正式验证工作之一。我们的经验表明，在适当的情况下，设计组件的完全形式化验证是一种可行的，工业上可行的和有竞争力的验证方法。
Formal verification of arithmetic datapaths has been part of the established methodology for most Intel processor designs over the last years, usually in the role of supplementing more traditional coverage oriented testing activities. For the recent Intel$^{\tiny\circledR}$ CoreTMi7 design we took a step further and used formal verification as the primary validation vehicle for the core execution cluster, the component responsible for the functional behaviour of all microinstructions. We applied symbolic simulation based formal verification techniques for full datapath, control and state validation for the cluster, and dropped coverage driven testing entirely. The project, involving some twenty person years of verification work, is one of the most ambitious formal verification efforts in the hardware industry to date. Our experiences show that under the right circumstances, full formal verification of a design component is a feasible, industrially viable and competitive validation approach.