FVRuleLearner: Operator-Level Reasoning Tree (OP-Tree)-Based Rules Learning for Formal Verification

📄 arXiv: 2604.03245 📥 PDF

作者: Lily Jiaxin Wan, Chia-Tung Ho, Yunsheng Bai, Cunxi Yu, Deming Chen, Haoxing Ren

分类: cs.AR, cs.AI, cs.SE

发布日期: 2026-04-07

💡 一句话要点

FVRuleLearner：提出基于算子推理树的规则学习框架，提升形式验证中SVA生成的正确性。

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 形式验证 SystemVerilog断言 自然语言处理 规则学习 算子推理树

📋 核心要点

  1. 现有方法在形式验证中，难以有效利用大型语言模型生成正确的SystemVerilog断言（SVA），主要受限于训练数据和FV算子的复杂性。
  2. FVRuleLearner提出了一种基于算子推理树（OP-Tree）的规则学习框架，通过结构化推理和算子对齐检索来生成更准确的SVA。
  3. 实验结果表明，FVRuleLearner在SVA的语法正确性和功能正确性方面均优于现有方法，并显著减少了SVA的功能故障。

📝 摘要（中文）

大型语言模型（LLMs）在推理和代码生成方面的卓越能力激发了人们对自动化形式验证（FV）的兴趣。形式验证通过数学上精确的断言来确保硬件的正确性，但其劳动强度很高，尤其是在将自然语言转换为SystemVerilog断言（NL-to-SVA）的过程中。然而，由于训练数据有限以及FV算子的内在复杂性，LLMs在SVA生成方面仍然面临挑战。因此，对于确保正确的SVA算子选择，更有效和稳健的方法至关重要。为了应对这些挑战，我们提出了FVRuleLearner，这是一个基于新型算子推理树（OP-Tree）的算子级规则（Op-Rule）学习框架，它将SVA生成建模为结构化的、可解释的推理。FVRuleLearner分两个互补的阶段运行：（1）训练：构建OP-Tree，将NL-to-SVA对齐分解为细粒度的、算子感知的提问，组合导致正确断言的推理路径；（2）测试：执行算子对齐的检索，从学习到的OP-Tree中获取相关的推理轨迹，并为未见过的规范生成新的规则。综合研究表明，所提出的FVRuleLearner在语法正确性方面优于最先进的基线3.95%，在功能正确性方面平均优于31.17%。此外，FVRuleLearner通过功能分类分析，成功地减少了各种算子类别中平均70.33%的SVA功能故障，表明了将学习到的OP-Tree应用于Op-Rule生成对于未见过的NL-to-SVA任务的有效性。这些结果确立了FVRuleLearner作为形式验证中特定领域推理和规则学习的新范例。

🔬 方法详解

问题定义：论文旨在解决形式验证中，将自然语言描述转换为SystemVerilog断言（NL-to-SVA）时，大型语言模型（LLMs）由于训练数据不足和FV算子复杂性而导致的SVA生成错误问题。现有方法难以保证SVA的功能正确性，需要人工干预，效率低下。

核心思路：论文的核心思路是将NL-to-SVA的转换过程建模为结构化的、可解释的推理过程。通过构建算子推理树（OP-Tree），将复杂的NL-to-SVA对齐分解为细粒度的、算子感知的提问，从而实现更精确的算子选择和规则生成。这种方法旨在提高SVA生成的功能正确性，并减少人工干预。

技术框架：FVRuleLearner框架包含两个主要阶段：训练阶段和测试阶段。在训练阶段，框架构建OP-Tree，该树将NL-to-SVA对齐分解为一系列算子相关的推理步骤，并组合导致正确断言的推理路径。在测试阶段，框架执行算子对齐的检索，从学习到的OP-Tree中获取相关的推理轨迹，并为未见过的规范生成新的规则。

关键创新：该论文的关键创新在于提出了算子推理树（OP-Tree）的概念，它是一种结构化的、可解释的知识表示方法，用于建模NL-to-SVA的转换过程。OP-Tree将复杂的转换过程分解为一系列细粒度的、算子感知的推理步骤，从而提高了SVA生成的功能正确性。与现有方法相比，OP-Tree能够更好地捕捉FV算子的语义信息，并生成更准确的SVA。

关键设计：OP-Tree的构建涉及对NL-to-SVA对齐数据的分析，提取算子相关的特征，并构建推理路径。在测试阶段，框架使用算子对齐的检索方法，从OP-Tree中找到与当前输入最相关的推理轨迹。具体的参数设置和损失函数等技术细节在论文中未详细描述，属于未知信息。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

FVRuleLearner在语法正确性方面比最先进的基线提高了3.95%，在功能正确性方面平均提高了31.17%。通过功能分类分析，FVRuleLearner成功地减少了各种算子类别中平均70.33%的SVA功能故障。这些结果表明，FVRuleLearner在SVA生成方面具有显著的优势。

🎯 应用场景

FVRuleLearner可应用于硬件设计的形式验证流程中，自动化生成SystemVerilog断言，减少人工编写断言的工作量，提高验证效率和质量。该研究成果有助于推动形式验证技术的普及，降低硬件设计的出错风险，尤其是在复杂SoC设计中具有重要价值。

📄 摘要（原文）

The remarkable reasoning and code generation capabilities of large language models (LLMs) have recently motivated increasing interest in automating formal verification (FV), a process that ensures hardware correctness through mathematically precise assertions but remains highly labor-intensive, particularly through the translation of natural language into SystemVerilog Assertions (NL-to-SVA). However, LLMs still struggle with SVA generation due to limited training data and the intrinsic complexity of FV operators. Consequently, a more efficient and robust methodology for ensuring correct SVA operator selection is essential for producing functionally correct assertions. To address these challenges, we introduce FVRuleLearner, an Operator-Level Rule (Op-Rule) learning framework built on a novel Operator Reasoning Tree (OP-Tree), which models SVA generation as structured, interpretable reasoning. FVRuleLearner operates in two complementary phases: (1) Training: it constructs OP-Tree that decomposes NL-to-SVA alignment into fine-grained, operator-aware questions, combining reasoning paths that lead to correct assertions; and (2) Testing: it performs operator-aligned retrieval to fetch relevant reasoning traces from the learned OP-Tree and generate new rules for unseen specifications. In the comprehensive studies, the proposed FVRuleLearner outperforms the state-of-the-art baseline by 3.95% in syntax correctness and by 31.17% in functional correctness on average. Moreover, FVRuleLearner successfully reduces an average of 70.33% of SVA functional failures across diverse operator categories through a functional taxonomy analysis, showing the effectiveness of applying learned OP-Tree to the Op-Rule generations for unseen NL-to-SVA tasks. These results establish FVRuleLearner as a new paradigm for domain-specific reasoning and rule learning in formal verification.