AutoSVA：使RTL模块交互的形式化验证民主化
AutoSVA: Democratizing Formal Verification of RTL Module Interactions
摘要：
现代SoC设计依赖于独立验证IP块相对于其自身规格的能力。基于SystemVerilog断言（SVA）的形式化验证（FV）是一种在单元级对模块进行穷举验证的有效方法。不幸的是，FV有一个陡峭的学习曲线，需要工程努力，阻止硬件设计人员在RTL模块开发过程中使用它。我们提出AutoSVA，一个框架，自动生成FV测试台，验证模块交互中涉及的控制逻辑的活性和安全性。我们证明了AutoSVA的有效性和效率的死锁关键模块的广泛使用的开源硬件项目。
英文摘要：
Modern SoC design relies on the ability to separately verify IP blocks relative to their own specifications. Formal verification (FV) using SystemVerilog Assertions (SVA) is an effective method to exhaustively verify blocks at unit-level. Unfortunately, FV has a steep learning curve and requires engineering effort that discourages hardware designers from using it during RTL module development. We propose AutoSVA, a framework to automatically generate FV testbenches that verify liveness and safety of control logic involved in module interactions. We demonstrate AutoSVA's effectiveness and efficiency on deadlock-critical modules of widely-used open-source hardware projects.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
