Automated Formal Verification for Domain-Specific Hardware Acceleration

点击翻译按钮获取中文摘要

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.