Unlocking the Power of Formal Hardware Verification with CoSA and Symbolic QED: Invited Paper
Unlocking the Power of Formal Hardware Verification with CoSA and Symbolic QED: Invited Paper
复制标题
使用 CoSA 和符号 QED 释放正式硬件验证的力量：特邀论文
DOI：
--
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
Clark W. Barrett
中科院分区：
文献类型：
--
作者：
Florian Lonsing;K. Ganesan;Makai Mann;Srinivasa Shashank Nuthakki;Eshan Singh;Mario Srouji;Yahan Yang;S. Mitra;Clark W. Barrett
随着设计规模和复杂性的增长，设计验证成为设计团队面临的最困难和最昂贵的任务之一。形式化验证技术提供了巨大的希望，因为它们能够详尽地探索设计行为。然而，形式化技术也有劳动密集型和局限于小块的声誉。形式化技术在设计规模上的成功应用有希望吗？我们通过深入挖掘来了解真实的技术问题和机会是什么，从而肯定地回答了这个问题。首先，我们看看可满足性求解器，引擎的形式化技术，如模型检查。鉴于最近的创新，在可满足性解决，我们认为，有很多理由是乐观的，形式化的技术将规模的实际利益的设计。我们使用我们的CoSA模型检查器作为演示平台来说明求解器的进步如何提高可扩展性。然而，即使求解器变得非常快，应用它们仍然是劳动密集型的。这是因为形式化工具的有用程度取决于它们被赋予证明的属性，而这些属性在传统上需要付出巨大的努力来开发。符号快速错误检测（SQED）通过使用自动检查设计的单个通用属性来解决这个问题。我们演示了SQED如何自动发现各种设计中的逻辑和安全错误，并报告在学术和行业设计中发现的错误和实现的效率提升。我们还提出了一个发电机的改进SQED模块，进一步减少了大量的手动工作，必须花费的设计师。
As designs grow in size and complexity, design verification becomes one of the most difficult and costly tasks facing design teams. Formal verification techniques offer great promise because of their ability to exhaustively explore design behaviors. However, formal techniques also have a reputation for being labor-intensive and limited to small blocks. Is there any hope for successful application of formal techniques at design scale? We answer this question affirmatively by digging deeper to understand what the real technological issues and opportunities are. First, we look at satisfiability solvers, the engines underlying formal techniques such as model checking. Given the recent innovations in satisfiability solving, we argue that there are many reasons to be optimistic that formal techniques will scale to designs of practical interest. We use our CoSA model checker as a demonstration platform to illustrate how advances in solvers can improve scalability. However, even if solvers become blazingly fast, applying them well is still labor-intensive. This is because formal tools are only as useful as the properties they are given to prove, which traditionally have required great effort to develop. Symbolic quick error detection (SQED) addresses this issue by using a single, universal property that checks designs automatically. We demonstrate how SQED can automatically find logic and security bugs in a variety of designs and report on bugs found and efficiency gains realized in academic and industry designs. We also present a generator for an improved SQED module that further reduces the amount of manual effort that has to be spent by the designer.