CPA-CSA: Verification-Aware Microarchitecture

CPA-CSA：验证感知微架构

• 批准号: 0811290
• 负责人: Daniel Sorin
• 金额: $ 22万
• 依托单位: Duke University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2008
• 资助国家: 美国
• 起止时间: 2008-09-01 至 2012-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0811290&HistoricalAwards=false
• 关键词: CPA; CSA; Verification; Aware; Microarchitecture

Microprocessor verification is a critical challenge for the computing industry. A design bug in a shipped processor chip can lead to failures and data corruptions, which can be catastrophic in many applications, such as medical equipment, avionics, and automotive control. Microprocessor design bugs can also be financially disastrous; the recall of Intel's Pentium, due to its notorious division bug, cost Intel approximately 420 million dollars. Society relies upon microprocessors, and thus the possibility of a flawedmicroprocessor is an enormous concern. Unfortunately, verifying a complex, modern microprocessor is extremely difficult. Due to both its difficulty and importance, verification consumes a large fraction (60-70%) of the resources--engineers, time, and money--devoted to the creation of a new microprocessor. Despite this effort, the most recent processors from Intel, AMD, and IBM have been shipped with dozens of documented design bugs.This research project addresses both society's need for correct microprocessor designs and industry's desire to improve product quality and shorten the design cycle, both of which can be achieved through a reduction in verification effort. The project's goal is to design microprocessors such that they can be more easily verified. To achieve this goal, this project will pursue three complementary research thrusts. The first thrust will analyze existing designs to identify features that require more verification effort than is merited by their benefits. The second thrust will re-design the waysin which microprocessor components interact, in order to reduce design complexity. The third thrust will develop sets of invariants that facilitate verification; there are often many ways to specify the correctness of a system, some of which are far easier to verify than others. The benefits of the proposed research are broader than its technical results, because of the importance of the verification problem to national infrastructure and industry. This project will also support training of undergraduate and minority students.

微处理器验证是计算行业面临的严峻挑战。发货的处理器芯片中的设计错误可能会导致故障和数据损坏，这在许多应用中可能是灾难性的，例如医疗设备、航空电子设备和汽车控制。微处理器设计缺陷也可能造成经济灾难。由于臭名昭著的除法错误，英特尔奔腾的召回使英特尔损失了大约 4.2 亿美元。社会依赖微处理器，因此微处理器存在缺陷的可能性是一个巨大的问题。不幸的是，验证复杂的现代微处理器极其困难。由于其难度和重要性，验证消耗了用于创建新微处理器的大部分资源（60-70%）——工程师、时间和金钱。尽管做出了这些努力，英特尔、AMD 和 IBM 的最新处理器在出厂时仍存在数十个记录在案的设计错误。该研究项目既满足了社会对正确微处理器设计的需求，也满足了业界提高产品质量和缩短设计周期的愿望。这可以通过减少核查工作来实现。该项目的目标是设计微处理器，使其更易于验证。 为了实现这一目标，该项目将追求三个互补的研究主旨。 第一个重点将分析现有设计，以确定需要比其优点更多的验证工作的功能。 第二个推动力将重新设计微处理器组件交互的方式，以降低设计复杂性。 第三个重点将开发一组有助于验证的不变量；通常有很多方法可以指定系统的正确性，其中一些方法比其他方法更容易验证。 由于验证问题对国家基础设施和工业的重要性，拟议研究的好处比其技术成果更广泛。 该项目还将支持本科生和少数民族学生的培训。