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.

翻译：高层次综合（HLS）将硬件的算法描述从较高抽象层次（如C/C++）转换为寄存器传输级（RTL）设计，从而缩短开发时间并提高设计空间探索的灵活性。然而，由于HLS工具的局限性或错误，这类机器生成的RTL设计可能包含重大功能缺陷或安全漏洞。识别这些漏洞最可靠的方法之一是形式化验证，尤其是模型检验。然而，生成的RTL规模庞大常导致模型检验在合理的时间或资源限制内难以得出结论。本研究提出利用HLS流程中的高层次设计特征，构建一组辅助断言，旨在引导模型检验器并加速验证过程。为确定最有效的辅助断言集以协助模型检验器，我们开发了一种证明机制，通过迭代重用证明信息来选择潜在最有用的辅助断言集。我们在多组HLS设计基准上评估了所提出的框架。实验结果表明，与原生模型检验相比，本方法实现了最高6.05倍、平均2.23倍的加速比。