CPA-CSA: Verification-Aware Microarchitecture

微处理器验证是计算机行业的一个关键挑战。处理器芯片中的设计缺陷可能导致故障和数据损坏，这在许多应用中可能是灾难性的，例如医疗设备，航空电子设备和汽车控制。微处理器的设计缺陷也可能造成经济上的灾难;英特尔的奔腾因其臭名昭著的分部缺陷而被召回，使英特尔损失了大约4.2亿美元。社会依赖于微处理器，因此微处理器出现缺陷的可能性是一个巨大的问题。不幸的是，验证一个复杂的现代微处理器是非常困难的。由于其难度和重要性，验证消耗了大量（60-70%）的资源-工程师，时间和金钱-致力于创建一个新的微处理器。尽管如此，英特尔、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.