AutoINV：用于高层次综合设计形式验证的自动化不变量生成框架
AutoINV: Automated Invariant Generation Framework for Formal Verification on High-Level Synthesis Designs
AI总结：
本文提出利用高层次综合流程中的设计特征构建辅助断言，以引导模型检查器并加速验证过程，实验表明在高层次综合设计基准上，该方法在速度上提升了最高6.05倍，平均提升2.23倍。
摘要：
高层次综合（HLS）将硬件算法描述从更高抽象（如C/C++）转换为寄存器传输级（RTL）设计，提供减少开发时间和设计空间探索的更大灵活性。然而，由于HLS工具的限制或错误，生成的RTL设计可能包含主要功能错误或安全漏洞。形式验证，特别是模型检查，是识别这些漏洞最可靠的方法之一。然而，生成的RTL规模较大，常导致模型检查难以在合理时间内或资源限制内得出结论。本文提出利用HLS流程中的高层次设计特征构建一组辅助断言，以引导模型检查器并加速验证过程。为了确定最有效的辅助断言集，我们开发了一种证明机制，通过迭代重用证明信息来选择潜在最有用的辅助断言集。我们评估了所提出的框架在HLS设计基准集上的性能。实验结果表明，与传统的模型检查相比，我们的方法在速度上最高提升了6.05倍，平均提升了2.23倍。
英文摘要：
High-level synthesis (HLS) transforms an algorithmic description of hardware from a higher abstraction (e.g., C/C++) into a register-transfer level (RTL) design, offering reduced development time and greater flexibility in design space exploration. However, such machine-generated RTL designs may contain major functional bugs or security vulnerabilities due to limitations or errors in the HLS tools. One of the most reliable methods to identify these vulnerabilities is formal verification, particularly model checking. Nevertheless, the large size of the generated RTL often causes model checking to struggle to conclude within reasonable time or resource limits. In this study, we propose utilizing the high-level design features from the HLS flow to construct a set of helper assertions aimed at guiding the model checker and accelerating the verification process. To identify the most effective set of helpers to assist the model checker, we develop a proving mechanism that iteratively reuses proving information to select the potentially most useful set of helpers. We evaluate the proposed framework on a set of HLS design benchmarks. Experimental results demonstrate that, when compared to vanilla model checking, our approach achieves a speedup of up to 6.05x, and 2.23x on average.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
