NeuroAbs：用于属性检查加速的神经符号RTL抽象框架
NeuroAbs: A Neuro-Symbolic RTL Abstraction Framework for Property Checking Acceleration
- The Hong Kong University of Science and Technology (Guangzhou)（香港科技大学（广州））
- The Hong Kong University of Science and Technology（香港科技大学）
机构由 AI 辅助整理，请以论文原文为准。
AI总结：
本文提出NeuroAbs框架，结合LLM与AST实现RTL抽象，通过SMT验证抽象正确性、CEGAR迭代精化，可加速硬件属性检查，解决现有方法人工成本高或灵活性不足的问题。
AI中文摘要：
形式化验证是确保硬件设计功能正确性的关键技术。在属性检查场景中，面对日益复杂的RTL设计，高效证明用户指定属性是核心挑战。为解决该挑战，常采用抽象技术降低系统复杂度以加速验证过程，但现有RTL抽象方法要么需要大量人工投入，要么依赖规则式技术，灵活性不足。本文提出NeuroAbs，一种神经符号RTL抽象框架：NeuroAbs首先利用大语言模型（LLM）辅助的RTL分析识别适合抽象的信号，随后将基于LLM的抽象与基于抽象语法树（AST）的符号RTL表示相结合，使生成的抽象更贴合预期变换；每个抽象的正确性通过可满足性模理论（SMT）求解验证；若抽象粒度过粗无法完成证明，NeuroAbs会采用反例引导的抽象精化（CEGAR）迭代优化模型。实验结果表明，NeuroAbs在各类验证任务中显著提升了硬件属性检查的效率。
英文摘要：
Formal verification is a crucial technique for ensuring the functional correctness of hardware designs. In the context of property checking, a key challenge is how to efficiently prove a user-specified property in the face of increasingly complex RTL designs. To address this challenge, abstraction techniques are often employed to reduce system complexity and accelerate the verification process. However, prior RTL abstraction methods either require significant manual effort or rely on rule-based techniques that lack flexibility. This paper introduces NeuroAbs, a neuro-symbolic framework for RTL abstraction. NeuroAbs first uses LLM-assisted RTL analysis to identify signals suitable for abstraction. It then combines LLM-based abstraction with an AST-based symbolic RTL representation to better align the generated abstraction with the intended transformation. The soundness of each abstraction is checked using satisfiability modulo theories (SMT) solving. If the abstraction is too coarse for a successful proof, NeuroAbs applies counterexample-guided abstraction refinement (CEGAR) to iteratively refine the model. Experimental results show that NeuroAbs significantly improves the efficiency of hardware property checking across a range of verification tasks.
