SystemVerilog Assertions (SVA) are essential for formal verification of digital hardware, yet their manual creation demands significant expertise in both the design under verification and temporal logic. Recent studies have explored using large language models (LLMs) to automate SVA generation, but existing approaches suffer from incorrect signal references, missing timing constraints, and lack of formal correctness guarantees. This paper presents ProofLoop, a tool-augmented ReAct agent that generates SVA from natural-language specifications using a solver-in-the-loop approach. The agent operates in two phases: Phase A autonomously gathers design context by invoking EDA and formal tools, including semantic search over an AST-indexed vector database and JasperGold structural queries, while Phase B generates SVA and iteratively refines it using JasperGold formal proof feedback over up to fixed (here 3) verification rounds. We evaluate ProofLoop on FVEval Design2SVA design benchmarks and demonstrate that this framework can achieve 93.7% syntax correctness and 82.0% functional correctness. An ablation study confirms that each component, i.e., retrieval-augmented generation (RAG), JasperGold tools, and the verification loop contributes significantly (and orthogonally).

翻译：SystemVerilog断言（SVA）对于数字硬件的形式验证至关重要，但其手动创建需要对被验证设计和时序逻辑具备深厚的专业知识。近期研究探索了利用大型语言模型（LLM）自动生成SVA，但现有方法存在信号引用错误、缺乏时序约束以及缺少形式正确性保证等问题。本文提出ProofLoop——一种经过工具增强的ReAct智能体，它采用求解器在环（solver-in-the-loop）方法，从自然语言规范中生成SVA。该智能体分两阶段运作：阶段A通过调用EDA和形式工具自主收集设计上下文，包括基于AST索引向量数据库的语义搜索以及JasperGold结构查询；阶段B生成SVA，并利用JasperGold形式验证反馈，在最多固定次数（此处为3次）的验证轮次中迭代优化。我们在FVEval Design2SVA设计基准上评估ProofLoop，结果表明该框架可达到93.7%的语法正确性和82.0%的功能正确性。消融研究证实，每个组件（即检索增强生成（RAG）、JasperGold工具以及验证循环）均对性能有显著且正交的贡献。