Automated Formal Verification for Domain-Specific Hardware Acceleration

计算机芯片、计算机系统和计算机软件是人类有史以来设计的最复杂的东西。例如，即使是我们的学生在第一门计算机科学课程中编写的简单程序，其可能的行为也远远超过宇宙中的光子！毫不奇怪，很难把所有的细节都做对。事实上，公司现在花费最多的精力不是在设计上，而是在验证上--确定系统是否正确运行的任务。形式验证是使用数学逻辑来辅助验证过程。我的研究强调自动形式验证，其中计算机程序分析正在设计的系统，自动查找错误或证明设计的属性，除了指定所需的内容外，还需要最少的人力。从20世纪90年代开始的研究突破（一直持续到今天）使得形式验证对于验证计算机硬件是必不可少的-所有主要的计算机和电子公司都在他们的计算机芯片上使用形式验证。这是学术研究的一个重大成功故事，为社会带来了巨大的进步。从21世纪初开始，随着计算机硬件形式验证的成功，学术研究界将重点转移到软件上。这一关注为软件的自动化验证带来了非凡的进步，Facebook、亚马逊、微软和谷歌等领先的软件公司都在正式验证方面进行了大量投资。然而，软件并不存在于真空中--它需要在计算机硬件上运行。并且特别地，要求新的软件任务（例如，机器学习、机器视觉、自动翻译等）已经催生了对加速特定问题计算任务的全新硬件设计的需求。该提案的重点是开发理论和实践工具，用于验证新兴的新硬件设计以及依赖于它们的硬件/软件系统。拟议的研究将建立在硬件和软件的自动化形式验证的先前成功的基础上，但该提案也呼吁在正式的硬件验证复兴：我们需要革命性的新技术（规范形式主义，抽象，算法）和工具，以帮助开发革命性的新硬件架构。如果成功，这项研究将有助于计算机和电子行业的持续进步和成功。

Computer chips, computer systems, and computer software are the most complex things ever designed by humans. For example, even the simple programs written by our students in their first computer science course have far more possible behaviors than there are photons in the universe! Not surprisingly, it's hard to get all the details right. In fact, companies now spend the most effort not on design, but on verification -- the task of determining if the system behaves correctly. Formal verification is the use of mathematical logic to aid the verification process. My research emphasizes automatic formal verification, in which a computer program analyzes the system being designed, automatically finding bugs or proving properties about the design, with minimal human effort beyond specifying what is desired. Research breakthroughs starting in the 1990s (and continuing today) made formal verification indispensable for verifying computer hardware -- all major computer and electronics companies use formal verification on their computer chips. This has been a major success story of academic research enabling enormous progress for society. Starting in the early 2000s, as the success of formal verification for computer hardware became established, the academic research community shifted its focus to software. This focus has generated extraordinary progress for automated verification of software, and leading software companies like Facebook, Amazon, Microsoft, and Google all have substantial investments in formal verification. However, software doesn't exist in a vacuum -- it needs to run on computer hardware. And in particular, demanding new software tasks (e.g., machine learning, machine vision, automated translation, etc.) have spawned demand for radical new hardware designs that accelerate problem-specific computational tasks. This proposal focuses on developing theoretical and practical tools for verifying the emerging new hardware designs as well as the hardware/software systems that rely on them. The proposed research will build upon the prior successes of automated formal verification for both hardware and software, but the proposal is also calling for a renaissance in formal hardware verification: we need revolutionary new techniques (specification formalisms, abstractions, algorithms) and tools to help develop the revolutionary new hardware architectures. If successful, the research will help enable the continued progress and success of the computer and electronics industries.