CPA-CSA: Verification-Aware Microarchitecture

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

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.