发表机构
The Hong Kong University of Science and Technology (Guangzhou); The Hong Kong University of Science and Technology（香港科技大学（广州）; 香港科技大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
该研究提出NeuroAssertion框架，结合形式化迹生成、SyGuS与智能体启发优化，实现覆盖率驱动的RTL断言生成，断言数量与突变覆盖率均约为传统方法的2倍。
AI 中文摘要
硬件功能验证依赖高质量断言来暴露设计缺陷并建立对寄存器传输级（RTL）设计的置信度。然而现有断言挖掘方法仍难以生成完整可靠的断言集：随机或有限的迹无法覆盖难以到达的行为，一次性生成几乎无法提供关于仍未验证内容或应如何改进断言集的反馈。因此，即使生成了大量断言，关键设计行为仍可能未被覆盖。我们提出NeuroAssertion，一种覆盖率驱动的断言生成框架，该框架在统一框架内结合了形式化迹生成、语法引导综合（SyGuS）和智能体启发的优化过程。我们的框架首先将难以到达的控制流条件转换为形式化可达性目标，使用模型检查生成行为多样化的迹，并通过SyGuS从这些迹中挖掘初始断言。随后在验证反馈下执行有针对性的智能体启发优化：一个大语言模型（LLM）首先为未覆盖区域提出候选断言，若候选断言未通过形式化检查，第二个LLM会生成修复语法，指导神经符号修复过程中的受限符号综合。实验结果表明，该框架生成的断言数量约为传统断言挖掘方法的2倍，突变覆盖率也约为传统方法的2倍。
英文摘要
Hardware functional verification relies on high-quality assertions to expose design bugs and establish confidence in Register Transfer Level (RTL) designs. Yet existing assertion mining methods still struggle to produce complete and reliable assertion sets: random or limited traces fail to cover hard-to-reach behaviors, and one-shot generation provides little feedback about what remains unverified or how the assertion set should be improved. As a result, critical design behaviors can remain uncovered even when many assertions are generated. We present NeuroAssertion, a coverage-driven assertion generation framework that combines formal trace generation, syntax-guided synthesis (SyGuS), and an agent-inspired refinement process within a unified framework. Our framework first converts hard-to-reach control-flow conditions into formal reachability objectives, uses model checking to generate behaviorally diverse traces, and mines initial assertions from these traces with SyGuS. It then performs targeted agent-inspired refinement under verification feedback: one LLM first proposes candidate assertions for uncovered regions, and if a candidate fails formal checking, a second LLM generates a repair grammar that guides constrained symbolic synthesis in a neuro-symbolic repair procedure. Experimental results show that this framework delivers around 2X more assertions and about 2X higher mutation coverage than traditional assertion mining methods.
CommentsAccepted at MLCAD 2026
