利用大语言模型将自然语言描述转化为 SystemVerilog 断言（SVA），表面上是“代码生成”的一个应用分支，但其真正的挑战并非语法，而是语义。例如，一个“握手后必须响应”的需求，可能涉及时序蕴含、复位屏蔽、信号稳定性、延迟窗口以及位级抽象等多种微妙的逻辑选择。

研究论文揭示，在自然语言到 SVA（NL-to-SVA）任务中，超过 80% 的功能性错误源于时序算子的误用。其中，仅 |-> 与 |=> 这两个算子的混淆，就导致了 50% 至 64% 的断言失效。这类错误在文本层面具有极高的相似度，却会使形式验证的结果完全相反。

面对 NL-to-SVA 任务，大语言模型的常规推理往往生成功能错误的 SVA。NVlabs 提出的 FVRULELEARNER 框架则另辟蹊径，通过学习到的算子推理树（OP-TREE）来生成功能正确的 SVA。下图直观对比了传统 LLM 与 FVRULELEARNER 在 SVA 生成上的差异，直指 LLM 在 NL-to-SVA 任务中因时序算子理解不足和训练数据有限而导致的功能错误问题。传统 LLM 难以精准匹配硬件时序语义，而 FVRULELEARNER 依托于算子推理树的结构化推理，锚定 SVA 算子的正确使用逻辑，从根源上解决了功能失配问题。这验证了 OP-TREE 对提升 SVA 功能正确性的核心价值，也奠定了该框架的技术创新基础。

一旦 LLM 将 |-> 误写为 |=>，或者遗漏了某个 enable 条件，尽管文本的相似度可能依然很高，但形式验证的结果会大相径庭。

FVRULELEARNER: Operator-Level Reasoning Tree (OP-TREE)-Based Rules Learning for Formal Verification
FVRuleLearner 是一个面向 NL2SVA 的规则学习流水线。当前发布的主线为 src 目录下的纯提示词链路，并采用 JasperGold 进行语法与功能评估。
代码：https://github.com/NVlabs/FVRuleLearner
论文：https://arxiv.org/abs/2604.03245

NVlabs/FVRuleLearner 的核心价值在于，它将那些失败的样本从一次性的错误，转化为可被后续检索、排序、解释和复用的规则资产。

FVRULELEARNER 的流程概览及训练中 OP-TREE 的示例如下图所示。该图拆解了 FVRULELEARNER 训练与测试的双阶段核心流程：训练阶段通过 OP-TREE 的三层结构模拟验证工程师的调试逻辑，提炼有效的算子推理轨迹；测试阶段则通过算子-语义混合检索匹配轨迹，经规则适配后生成新任务的 Op-Rule。OP-TREE 让推理过程变得可解释，解决了 LLM 生成 SVA 时的“黑盒”问题，同时双阶段设计保障了规则的有效性与跨任务泛化能力。

该框架并非简单地堆叠提示词，而是在训练阶段构建三层 OP-Tree，深入追问错误原因，通过上下文诊断、理论锚定和规则生成，创建可验证的算子级规则，仅保留经 JasperGold 验证功能等价的推理路径；在推理阶段则采用算子-语义混合评分的 RAG 机制，结合信号抽象的规则适配，生成精准的断言。

下图对比了通用规则与算子级规则对 SVA 生成的影响。通用规则因其抽象性，无法指导 LLM 精准使用时序算子，最终生成功能错误的断言；而 Op-Rule 作为针对 SVA 算子的细粒度可执行指令，明确界定了时序算子的使用场景，彻底消除了语义歧义。这一对比验证了算子级规则的精准性是解决 LLM 时序语义缺陷的关键，也是 FVRULELEARNER 区别于传统规则学习的核心创新。

实验数据表明，该框架相比 SOTA 基线，语法正确性提升了 3.95%，功能正确性平均提升了 31.17%，各类算子功能错误平均减少了 70.33%。此外，它仅需 48% 的训练数据即可达到性能饱和，并开源了包含 1000 条真实硬件设计的 NL2SVA-OpenCore 基准数据集。

下表展示了 LLM 模型在三类 NL-to-SVA 测试集上的实验结果。对比 GPT-4o、Claude 4.5 Sonnet、o3-mini 在不同基线与 FVRULELEARNER 下的 BLEU、语法正确性、功能正确性等指标，FVRULELEARNER 在所有模型和数据集上均大幅领先，功能正确性平均提升 31.17%，语法正确性接近 100%。结果证明，该框架不依赖特定 LLM，具备极强的普适性，能全面弥补各类 LLM 在 SVA 生成上的语义缺陷。

本文目录

一、快速上手使用
二、项目要解决的根问题：SVA 生成不是翻译，而是可验证语义对齐
2.1 从自然语言到形式断言的语义鸿沟
2.2 三类任务与数据入口
三、总体架构：训练沉淀规则，推理检索规则，评估闭环验证
3.1 主入口是一台状态机
3.2 配置不是附属品，而是实验协议
四、Q-Tree：把一次错误拆成可学习的推理路径
4.1 为什么需要树，而不是一条反思文本
4.2 Q-Tree 构建流程
五、RAG 与增强检索：不是找相似答案，而是找相似错误修复经验
5.1 RAGAgent 如何组织文档
5.2 Q-Tree 增强检索的入口
六、LLM 编排：轻量路径与 AutoGen 路径并存
6.1 FVProcessor 是流水线调度器
6.2 规则如何进入提示词
七、JasperGold 闭环：文本像不等于功能对
7.1 Tcl 脚本定义形式评估语义
7.2 评估输出如何汇总
八、SystemVerilog 资源：testbench 不是背景板，而是语义锚点
8.1 annotated_tb 承载验证上下文
8.2 opencore 路径的特殊性
九、知识如何落盘：suggestions 与 qtrees 是项目的长期记忆
9.1 Q-Tree 保存为机器与人都能读的格式
9.2 与普通 RAG 的根本区别
十、限制、边界与值得借鉴之处
10.1 需要谨慎表述的限制
10.2 对 AI+EDA 系统的启发
10.3 如果把它比作编译器
结语：真正的突破在于让形式验证经验可积累

一、快速上手使用

项目主线与快速上手

FVRuleLearner 当前发布版本的核心路径遵循 README 中描述的 prompt-only 模式，其代码入口集中在 src/ 目录下，主要承担 nl2sva_human、nl2sva_machine 和 nl2sva_opencore 三大核心任务。以下是快速搭建运行环境的标准流程：

# 来源：README.md  
conda create -n fvrulelearner python=3.10  
conda activate fvrulelearner  
pip install -r requirements.txt

启动运行之前，必须配置好 LLM 接口以及 JasperGold 形式验证工具的环境变量：

# 来源：README.md  
export OPENAI_API_KEY=...  
# 或：export ANTHROPIC_API_KEY=...  
export PATH=/path/to/jasper/bin:$PATH  
export LM_LICENSE_FILE=<your_jasper_license_server>  
export CDS_LIC_FILE=<your_jasper_license_server>

在仓库根目录下执行以下命令即可启动主流程：

# 来源：README.md  
cd FVRuleLearner  
python3 src/main.py

所有核心参数均集中在 src/config.py 文件中。训练阶段需进行如下配置：

# 来源：src/config.py  
# 选择执行阶段：train / inference / eval  
# global_task = 'inference'  
global_task = 'train'  
# global_task = 'eval'  

# 支持的发布任务：  
# task = "nl2sva_human"  
# task = "nl2sva_machine"  
task = "nl2sva_opencore"  

LLM_gateaway = "openai"  
# LLM_gateaway = "claude"  

llm_model = 'gpt-4o'  
# llm_model = "claude-sonnet-4-5-20250929"

训练完成后，输出结果会存放在以下目录结构中：

# 来源：README.md  
src/logs/train_<timestamp>_<hostname>_<user>/  
suggestions.pkl  
qtrees.pkl  
qtrees.json  
log.txt  
FLAGS.klepto

当需要执行推理时，只需将 global_task 切换为 "inference"，并将 load_suggestions_path 指向之前训练生成的日志目录。此外，也可以通过设置环境变量 FVRULELEARNER_TRAIN_LOGDIR 来覆盖默认的日志路径。关于数据集映射关系、推荐参数配置以及仅评估（eval-only）的使用方式，请参阅仓库的完整 README 文档：https://github.com/NVlabs/FVRuleLearner/blob/main/README.md。

二、核心挑战：SVA 生成远非简单翻译，而是可验证的语义对齐

2.1 自然语言到形式断言之间的语义鸿沟

表面上看，NL2SVA 任务似乎只是将一句自然语言描述转换成 SVA 代码，比如“当写有效且 FIFO 未满时，写指针应更新”。然而，在形式验证的严苛语境中，这句话背后隐藏着一系列工程约束条件：

断言应该基于哪个时钟沿进行采样？
在复位期间是否需要禁用该断言？
前件（antecedent）与后件（consequent）之间应该使用 |-> 还是 |=> 操作符？
是否需要引入 $stable、$past 或 ##[n:m] 等时序操作？
所涉及的信号是否来自 testbench 的抽象层，而非原始的 RTL 代码？
如何判断参考断言之间的等价性，而不仅仅是字符串层面的相似度？

FVRuleLearner 的学术论文题为《Operator-Level Reasoning Tree (OP-Tree)-Based Rules Learning for Formal Verification》[1]。仓库的 README 文件明确指出，它是一个专为 NL2SVA 设计的规则学习流水线，并借助 JasperGold 进行语法和功能性的全面评估。换言之，该项目并不满足于“生成一段看起来像 SVA 的代码”，其真正目标是学习“为什么某条断言是错误的，以及当再次遇到类似的算子级模式时，应该如何修正”。

2.2 三类任务及其数据入口

在配置文件中，发布版本的任务被严格限制为以下三类：

# 来源：src/config.py  
if task == "nl2sva_human":  
dataset_path = os.path.join(ROOT, "FVEval", "data_nl2sva", "data", "nl2sva_human.csv")  
elif task == "nl2sva_machine":  
dataset_path = os.path.join(ROOT, "FVEval", "data_nl2sva", "data", "nl2sva_machine_updated.csv")  
elif task == "nl2sva_opencore":  
dataset_path = os.path.join(ROOT, "FVEval", "data_1k", "module_sva_nl_manual_editing.csv")  
else:  
raise ValueError(f"Unsupported release task: {task}")

需要注意的是，该项目并非面向任意 Verilog 仓库的通用断言生成器，而是围绕特定基准测试格式组织起来的研究原型。每条数据记录通常包含自然语言提示、参考断言、设计名称、任务标识符、测试平台及相关上下文信息。

Python 主控部分负责组织样本、调用 LLM 生成 SVA 并保存结果；
FVEval 组件则负责将生成的结果与参考答案一同放入 JasperGold 可执行的评估框架中，进行闭环验证。

三、整体架构：训练阶段沉淀规则，推理阶段检索规则，评估阶段形成闭环

3.1 主入口本质上是一台状态机

3.1 三段式流水线：训练、推理与评估

src/main.py 的代码虽然简短，却清晰地定义了项目的三阶段核心流程：train（训练）、inference（推理）和 eval（评估）。

# 来源：src/main.py  
def main():  
if FLAGS.global_task in ['inference', 'train']:  

if FLAGS.model == 'agent':  
start_time = time.time()  
from fv_harwareagent_example import FVProcessor  
processor = FVProcessor()  
processor.main_fv()  
saver.save_stats('overall_runtime', time.time()-start_time)  

elif FLAGS.model == 'timing_agent':  
from hardware_agent.examples.timing_summary_hardwareagent_example import main  
main()  
else:  
raise NotImplementedError()  

if FLAGS.global_task == 'inference':  
from eval import eval  
eval(Path(saver.logdir))  

elif FLAGS.global_task == "eval":  
from eval import eval  
eval(FLAGS.folder_to_eval)

关键逻辑如下：

训练与推理：两者均通过 FVProcessor 模块执行。唯一的区别在于，推理任务完成后会自动触发评估流程。
仅评估：如果指定 global_task 为 "eval"，系统会直接针对已有的推理结果目录重新进行性能评估。

这种设计构成了一个清晰的三段式流水线：

# 来源：基于 src/main.py 与 README 简化  
train:  
数据集样本 -> LLM生成SVA -> 与参考断言比较 -> Q-Tree追问错误 -> 保存 suggestions.pkl/qtrees.json  

inference:  
新prompt -> 检索相似examples/suggestions/qtrees -> LLM生成或修正SVA -> JasperGold语法修复 -> 保存输出  

eval:  
LLM输出目录 -> 文本相似度评估 + JasperGold功能性评估 -> CSV汇总

3.2 配置：不止是附属，更是实验的“协议”

在 src/config.py 文件中，训练与推理阶段的配置被明确区分。训练阶段会关闭 RAG（检索增强生成）和 JasperGold 主评估功能，重点在于生成 suggestion 和构建 Q-Tree：

# 来源：src/config.py  
if global_task == 'train' and 'nl2sva' in task:  
# Training builds suggestions / Q-Trees; retrieval is disabled here.  
use_RAG = False  
use_JG = False  
RAG_content = ['Suggestions']  
# Number of self-improvement iterations per training sample.  
num_iter = 25  

train_temp_setting = "random"  
if train_temp_setting == "random":  
change_only_bleu_same = True  
low_temp = 0  
high_temp = 1.0  

use_QTree = True  
if use_QTree:  
# Number of questions expanded per Q-Tree level.  
question_tree_width = 3  

PEC_method = 'JasperGold'

在推理过程中，系统会激活 RAG 模块并启用 Q-Tree enhanced retrieval 机制：

```python
# 来源：src/config.py  
elif global_task == 'inference' and 'nl2sva' in task:  
use_RAG = True  
similarity_str = ["Question"]  
eval_content = ["similarity","jg"]  

if use_RAG:  
RAG_content = ['Examples', 'Suggestions']  

if 'Examples' in RAG_content:  
prompting_instruction = 0  
Examples_top_k = 1  

if 'Suggestions' in RAG_content:  
Suggestions_top_k = 3  
Suggestions_Reasoning = False  

# Enable FVRuleLearner's Q-Tree-enhanced retrieval.  
retrieval_on_ranking = True  
if retrieval_on_ranking:  
qtree_similarity_top_k = 5  
qtree_ranking_mode = 'prompt'  
rule_source = 'generate'  

llm_score_weight = 0.5  
operator_score_weight = 0.5  
operator_pruning_threshold = 0.0  

deduplication = True  
operator_explanation = False  
filter_functionality = True  
retrieve_str = ["Suggestions"]  
load_suggestions_path = DEFAULT_TRAIN_LOGDIR

这一配置方案值得深入探讨——它将“示例检索”与“规则检索”明确区分开来。

Examples 属于经典的上下文学习（in-context learning）机制；
Suggestions 则是从历史错误修复过程中提炼出的规则知识。

显然，后者才是 FVRuleLearner 真正的技术核心。

unsetunset四、Q-Tree：将一次错误拆解为可学习的推理路径unsetunset

4.1 为何需要树结构，而非简单的反思文本

多数 LLM 自修复系统在遭遇失败后，只会简单地追问一句：“请解释错误并给出建议。”而 FVRuleLearner 选择了一条更具结构化的路径：Q-Tree。它把生成的断言与参考断言之间的差异，分解为多个层级的提问：

背景知识：涵盖自然语言描述、测试平台（testbench）、生成断言、参考断言以及 SVA 语法常识；
探索性问题：从算子（operator）、时序（timing）、比较（comparison）等多个维度提出问题；
具体分析问题：针对每个差异点进行深入追问；
规则生成：将分析结果压缩为一条可复用的规则。

核心数据结构定义在 src/qtree_builder.py 中：

# 来源：src/qtree_builder.py  
class QuestionLevel(Enum):  
"""Levels in the Q-Tree hierarchy"""  
BACKGROUND = "background"  
EXPLORATORY = "exploratory"  
SPECIFIC_ANALYSIS = "specific_analysis"  
RULE_GENERATION = "rule_generation"  


@dataclass  
class QuestionNode:  
"""Node in the Q-Tree structure"""  
id: str  
question: str  
level: QuestionLevel  
parent_id: Optional[str] = None  
children: List[str] = field(default_factory=list)  
answer: Optional[str] = None  
rules_generated: List[str] = field(default_factory=list)  
metrics: Dict[str, Any] = field(default_factory=dict)  


class QTreeBuilder:  
"""Builds Q-Tree for assertion analysis and rule generation"""  

def __init__(self, agents: Dict[str, Any], config_flags=None):  
self.agents = agents  
self.nodes: Dict[str, QuestionNode] = {}  
self.tree_results = []  
self.max_questions_per_level = getattr(config_flags, 'question_tree_width', 3) if config_flags else 3  
self._last_diversity_metrics = None  
self._row_data = None  
self.qa_time = 0.0

可以将其类比为一次形式验证专家的代码审查过程：专家不会仅仅说“错了”，而是会追问“时序蕴含是否正确？”“比较操作符是否匹配四态逻辑？”“条件应该放在 antecedent 还是 consequent？”——这些问题构成树状结构，最终沉淀为可复用的规则。

4.2 Q-Tree 构建流程

# 来源：src/qtree_builder.py  
def build_qtree_for_assertion_pair(self,  
generated_assertion: str,  
reference_assertion: str,  
row: Any,  
metrics: Dict[str, Any]) -> List[QuestionNode]:  
"""  
Build a Q-Tree to analyze differences between generated and reference assertions  

Tree Structure:  
Root: Background Knowledge (context about the problem)  
Level 1: Exploratory questions about major differences  
Level 2: Specific analysis questions for each difference  
Level 3: Rule generation based on the analysis  
"""  
tree_nodes = []  
node_counter = 0  
self._row_data = row  

background_knowledge = self._get_background_knowledge(row, generated_assertion, reference_assertion)  

exploratory_questions = self._generate_exploratory_questions(  
generated_assertion, reference_assertion, metrics, row  
)  

for question in exploratory_questions:  
node = QuestionNode(  
id=f"explore_{node_counter}",  
question=question,  
level=QuestionLevel.EXPLORATORY,  
parent_id=None,  
metrics=metrics  
)  
node.answer = self._answer_exploratory_question(  
question, generated_assertion, reference_assertion, row  
)  

# Level 2: Generate specific analysis questions  
for parent_node in exploratory_nodes:  
specific_questions = self._generate_specific_analysis_questions(  
parent_node, generated_assertion, reference_assertion  
)  

# Level 3: Generate rules based on analysis  
for parent_node in specific_nodes:  
rules = self._generate_rules_from_analysis(  
parent_node, generated_assertion, reference_assertion  
)

这段代码的设计理念非常清晰：Q-Tree 并非直接用于“修复代码”，而是首先将错误空间进行结构化整理。对于 SVA 这种极度依赖操作符语义的语言而言，结构化的追问机制远比一次性反思更加稳定可靠。举例来说：

|-> 与 |=> 是否代表同一种“蕴含”关系？答案是否定的——前者是同一周期内的重叠蕴含，后者则是下一周期才触发的非重叠蕴含。
== 与 === 仅仅是编码风格上的差异吗？并非如此，后者执行的是四态（case equality）比较。
&& 与 || 能否仅凭语言直觉来选用？不能，这种选择直接决定了 antecedent 条件的范围是过宽还是过窄。

Q-Tree 的核心价值在于，它将上述差异转化为“可解释的问题节点”，随后将这些节点压缩为后续可检索的规则（rule）。

五、RAG 与增强检索：不是找相似答案，而是找相似错误修复经验

5.1 RAGAgent 如何组织文档

FVRuleLearner 中的 RAGAgent 支持两类检索模式：Examples 和 Suggestions。Examples 模式旨在寻找相似的问题与答案范例，而 Suggestions 模式则用于检索历史规则。在初始化过程中，系统会自动选择一个 embedding 模型，默认配置为 all-MiniLM-L6-v2。

# 来源：src/rag_agent.py  
class RAGAgent:  
def __init__(self, documents, rag_type, embedding_model='sbert'):  
self.delimiter = "<---->"  
self.rag_type = rag_type  
self.qtree_engine = None  

if rag_type == "Suggestions":  
if FLAGS.filter_functionality:  
documents = [doc for doc in documents if self.check_functionality(doc)]  
print(f"@@@DEBUG: Length of the filtered documents is @@@ {len(documents)} @@@")  

self.original_documents = [doc.replace(self.delimiter, "n").strip() for doc in documents]  
self.documents = [self.extract_section(doc, FLAGS.similarity_str, full_string=True) for doc in documents]  

if rag_type == "Suggestions":  
self.retrieve_documents = [self.extract_section(doc, FLAGS.retrieve_str, full_string=True) for doc in documents]  
elif rag_type == "Examples":  
self.retrieve_documents = [self.extract_section(doc, ["all"], full_string=True) for doc in documents]  

self.model = self._load_model(embedding_model)  
self.embeddings = self._index_documents()

这里存在一个关键过滤机制：当 filter_functionality=True 时，系统仅保留那些 Functionality 值为 1.0 的 suggestion。换言之，项目默认不会将所有失败经验都纳入知识库，而是只挑选那些已通过功能性验证的修复经验放入检索池。 这一设计对于形式验证至关重要，因为一条错误的规则比完全没有规则更具破坏性。

5.2 Q-Tree 增强检索的入口

当 retrieval_on_ranking=True 且 rag_type 为 Suggestions 时，普通的向量检索机制会升级为 Q-Tree 检索。

# 来源：src/rag_agent.py  
def retrieve_with_qtree(self, query, top_k=5, testbench=None):  
"""  
Retrieve suggestions using Q-Tree based inference.  
Supports multiple modes via FLAGS.qtree_retrieval_mode:  
    - 'prompt': Original Q-Tree inference  
    - 'initial_sva_generation': Generate SVA, hybrid ranking, operator pruning  
    - 'rule_generation': Generate rules from Q-Trees  
"""  
if FLAGS.retrieval_on_ranking:  
try:  
from qtree_enhanced_retrieval import integrate_enhanced_retrieval  

qtree_file = os.path.join(FLAGS.load_suggestions_path, "qtrees.json")  
if os.path.exists(qtree_file):  
with open(qtree_file, 'r') as f:  
qtree_data = json.load(f)  

result = integrate_enhanced_retrieval(  
query=query,  
qtree_data=qtree_data,  
testbench=testbench,  
csv_df=csv_df,  
top_k=top_k  
)  

if isinstance(result, dict):  
suggestions = result.get('suggestions', [])  
initial_sva = result.get('initial_sva', None)  
operator_explanations = result.get('operator_explanations', {})  
return {'suggestions': suggestions, 'initial_sva': initial_sva, 'operator_explanations': operator_explanations}

这段代码反映了一个非常现实的工程判断：检索到的知识并不总是一段 suggestion；它也有可能直接生成一条 initial SVA，或者附带 operator explanations。因此，返回值被设计为一个字典结构，包含 suggestions、initial_sva 和 operator_explanations 三个字段。后续的调用方会根据获取到的结果，决定是“直接使用初始断言”还是“将规则追加到 prompt 中再生成”。

六、LLM 编排：轻量路径与 AutoGen 路径并存

6.1 FVProcessor 是流水线调度器

FVProcessor 是负责训练与推理流程的核心调度类。在其初始化阶段，系统会根据具体任务创建一个基准测试启动器（benchmark launcher），而在推理过程中则负责加载示例（examples）与建议（suggestions）。

来源：src/fv_harwareagent_example.py

class FVProcessor:
def init(self):
self.dataset_path = FLAGS.dataset_path
self.model_name = FLAGS.llm_model
self.agent_arch = FLAGS.agent_arch
self.num_icl_examples = FLAGS.num_icl
self.debug = FLAGS.debug
self.save_dir = FLAGS.save_dir
self.experiment_id = self.dataset_path.split(“.csv”)[0].split(“/”)[-1]

        self.example_rag_agent = None  
        self.suggestion_rag_agent = None  
        self.assertion_generator = None  
        if FLAGS.global_task == 'train':  
            self.train_launcher = OrderedDict()  
            for task in FLAGS.src_examples:  
                bmark_launcher_src = self._create_bmark_launcher(task)  
                self.train_launcher[task] = bmark_launcher_src  
        elif FLAGS.global_task == 'inference':  
            self.bmark_launcher = self._create_bmark_launcher(FLAGS.task)

紧接着，在 main_fv() 函数中会依次创建 user、Coding、Reflection 等多个智能体（agent）。对于以 OpenAI 或 Claude 为主线的流程，系统采用了更为轻量的直接调用方式；而针对其他网关，则会回退到基于 HardwareAgent 的 AutoGen 编排机制。

6.2 规则如何融入提示词

最核心的生成逻辑体现在 _run_lightweight_nl2sva 函数中。该函数首先拼接示例（Examples），然后检索建议（Suggestions）。如果 Q-Tree 返回了初始的 SVA 断言，并且没有附带任何建议，那么就直接返回该断言；否则，会将检索到的建议作为“Additional knowledge/suggestions”附加到 prompt 中。

# 来源：src/fv_harwareagent_example.py  
def _run_lightweight_nl2sva(self, agents, system_prompt, fv_prompt, row):  
agents["Coding"].system_message = system_prompt  
message = fv_prompt  

if getattr(FLAGS, "use_RAG", False):  
full_question = f"Question: Create a SVA assertion that checks: {row.prompt}"  

if self.example_rag_agent is not None and "Examples" in getattr(FLAGS, "RAG_content", []):  
retrieved_docs = self.example_rag_agent.retrieve(  
full_question,  
top_k=getattr(FLAGS, "Examples_top_k", 1),  
)  
examples_list = [f"-  {doc}n" for doc in retrieved_docs]  
message = (  
f"{message}nn"  
"Additional context from similar documents:n"  
                + "".join(examples_list)  
)  

if self.suggestion_rag_agent is not None and "Suggestions" in getattr(FLAGS, "RAG_content", []):  
retrieved_result = self.suggestion_rag_agent.retrieve(  
full_question,  
top_k=getattr(FLAGS, "Suggestions_top_k", 3),  
testbench=row.testbench,  
)  

if isinstance(retrieved_result, dict):  
retrieved_docs = retrieved_result.get("suggestions", [])  
initial_sva = retrieved_result.get("initial_sva")  
else:  
retrieved_docs = retrieved_result  

if len(retrieved_docs) == 0 and initial_sva and not getattr(FLAGS, "operator_explanation", False):  
saver.save_stats("used_suggestions", 0)  
return initial_sva  

suggestions_list = []  
seen_suggestions = set()  
for doc in retrieved_docs:  
cleaned_doc = re.sub(r"^Suggestions:s*", "", str(doc).strip())  
for suggestion in cleaned_doc.split("n"):  
if getattr(FLAGS, "deduplication", True):  
if suggestion in seen_suggestions:  
continue  
seen_suggestions.add(suggestion)  
suggestions_list.append(suggestion)  

appended_suggestions = "n".join(suggestions_list)  
if appended_suggestions:  
saver.save_stats("used_suggestions", 1)  
message = (  
f"{message}nn"  
"Additional knowledge/suggestions to follow/obey:n"  
f"{appended_suggestions}"  
)  

response = initiate_chat_with_retry(  
agents["user"],  
agents["Coding"],  
message=message,  
)  
return response

这正是 FVRuleLearner 与“普通 RAG 生成”的核心差异所在：它检索到的并非现成的参考答案，而是“必须遵守的修复规则”。从模型行为的角度来看，这相当于为 LLM 配备了一本形式验证专家的经验笔记。

七、JasperGold 闭环：文本像不等于功能对

7.1 Tcl 脚本定义形式评估语义

在 FVEval 框架中，Tcl 脚本扮演了指挥 JasperGold 执行属性验证的关键角色。以 human/machine 任务为例，该脚本首先解析生成的 .sva 文件，随后调用 PEC 工具，用以检查语言模型生成的断言与参考断言之间是否等价。

# 来源：FVEval/tool_scripts/run_jg_nl2sva_human.tcl  
# 分析属性文件  
clear -all  
analyze -clear  
analyze -sv12 ${SV_DIR}/${EXP_ID}_${TASK_ID}.sva  
# 详细阐述设计与属性  
elaborate  

clear -all  
include tool_scripts/pec/pec.tcle  
set signal_list [split $SIGNAL_LIST ","]  
prop_eq_checker $LM_ASSERT_TEXT $REF_ASSERT_TEXT "" "" $signal_list

尽管这段 Tcl 代码篇幅不长，但它正是整个项目严谨性的基石。如果没有形式化验证工具，LLM 生成的 SVA 只能依赖 BLEU、ROUGE、精确匹配等纯文本指标进行评估；而引入 JasperGold 后，系统能够判断语法是否可解析，以及断言的语义是否与参考属性等价或足够接近。

7.2 评估输出的汇总方式

FVEval/fv_eval/evaluation.py 文件会同时计算文本相似度与 JasperGold 评估结果，并在推理模式下将两者合并。

# 来源：FVEval/fv_eval/evaluation.py  
def run_evaluation(self):  
for exp_name, result_list in self.llm_results:  
if ("similarity" in FLAGS.eval_content and FLAGS.global_task == 'eval') or (FLAGS.global_task == 'inference'):  
text_similiarty_eval_results = self.evaluate_text_similiarty(result_list)  
text_similiarty_eval_results = [  
asdict(r) for r in text_similiarty_eval_results  
]  
text_similiarty_eval_results = pd.DataFrame(text_similiarty_eval_results)  
text_similiarty_eval_results.to_csv(  
f"{self.save_dir}/{exp_name}_sim.csv", index=False  
)  
results = text_similiarty_eval_results  

if ("jg" in FLAGS.eval_content and FLAGS.global_task == 'eval') or (FLAGS.global_task == 'inference'):  
jg_eval_results = self.evaluate_jg(result_list)  
jg_eval_results = [asdict(r) for r in jg_eval_results]  
jg_eval_results = pd.DataFrame(jg_eval_results)  
jg_eval_results.to_csv(f"{self.save_dir}/{exp_name}_jg.csv", index=False)  
results = jg_eval_results  

if ("similarity" in FLAGS.eval_content and "jg" in FLAGS.eval_content and FLAGS.global_task == 'eval') or (FLAGS.global_task == 'inference'):  
combined_results = pd.merge(  
text_similiarty_eval_results,  
jg_eval_results,  
on=["experiment_id", "task_id", "model_name"],  
)  

# JasperGold Bug 快速修复  
combined_results.loc[combined_results['bleu'] == 1.0, 'functionality'] = 1.0  
combined_results.loc[combined_results['bleu'] == 1.0, 'func_relaxed'] = 1.0

这里有一个值得留意的工程细节：代码中标注了“JasperGold Bug Quick Fix”。当 BLEU 分数为 1.0 时，系统会将 functionality 和 func_relaxed 字段也强制设为 1.0。这本质上是一个工程层面的修补逻辑，不应在文章中被夸大为理论上的保证。更严谨的说法是：该项目同时采用了文本指标与 JasperGold 指标，并对完全字符串匹配的情况进行了保守修正。

八、SystemVerilog 资源：testbench 并非背景板，而是语义锚点

8.1 annotated_tb 承载验证上下文

仓库中包含了大量 annotated_tb 类型的 SystemVerilog 文件，例如 FIFO、RAM、FSM、计数器等。这些文件并非普通的示例代码，而是 NL2SVA 任务中的语义上下文：自然语言提示词往往依赖于 testbench 中定义的抽象信号、状态寄存器以及辅助 wire。

好的，以下是您要求的深度重写与降重后的文本，已严格遵循所有规则。

以 FIFO 代码片段为例

// 来源：FVEval/data_nl2sva/annotated_tb/fifo_1r1w.sv  
wire wr_push;  
wire rd_pop;  

wire tb_reset;  
assign tb_reset = (reset_ == 1'b0);  

wire fifo_full;  
assign wr_push = wr_vld && wr_ready;  
assign rd_pop = rd_vld && rd_ready;  

reg [DATA_WIDTH-1:0]             fifo_array [FIFO_DEPTH-1:0]; //fifo array - shift register  
reg [FIFO_DEPTH_log2-1:0]        fifo_rd_ptr;                 //fifo array - rd_ptr  
wire                             actual_fifo_pop;             // actual pop == pop  
reg                              fifo_empty;                  // fifo empty  
wire [DATA_WIDTH-1:0]            fifo_out_data;               // dout

假设一个提示词提到“当写入握手发生时……”，那么正确的断言应当直接引用 wr_push 信号，而不是生硬地拼接 wr_vld && wr_ready。同样，若涉及复位逻辑，则应使用测试平台中定义的 tb_reset。这表明，SVA的生成并非孤立的文本翻译，而是一个必须围绕测试平台的命名规范和辅助抽象进行语义对齐的过程。

8.2 opencore 路径的独特性

nl2sva_opencore 任务基于 FVEval/data_1k/module_sva_nl_manual_editing.csv 文件，并且其配置也调用了一套不同的 Tcl 脚本：

# 来源：src/config.py  
if task == "nl2sva_machine":  
tcl_file_path = os.path.join(ROOT, "FVEval", "tool_scripts", "run_jg_only_analysis.tcl")  
tcl_eval_file_path = os.path.join(ROOT, "FVEval", "tool_scripts", "run_jg_nl2sva_machine.tcl")  
elif task == "nl2sva_human":  
tcl_file_path = os.path.join(ROOT, "FVEval", "tool_scripts", "run_jg_only_analysis.tcl")  
tcl_eval_file_path = os.path.join(ROOT, "FVEval", "tool_scripts", "run_jg_nl2sva_human.tcl")  
elif task == "nl2sva_opencore":  
tcl_file_path = os.path.join(ROOT, "FVEval", "tool_scripts", "run_jg_only_syntax_opencore.tcl")  
tcl_eval_file_path = os.path.join(ROOT, "FVEval", "tool_scripts", "run_jg_nl2sva_opencore.tcl")

这清晰地表明，不同基准测试的评估条件存在差异。在撰写技术解读文章时，务必避免将某个特定任务的评估方法错误地推广到所有任务上。

九、知识如何沉淀：suggestions 与 qtrees 构建项目长期记忆

9.1 Q-Tree：一种机器与人皆可读的存储格式

训练阶段会生成多个产物，包括 suggestions.pkl、qtrees.pkl 和 qtrees.json。其中，qtrees.json 因其良好的可读性，最适合用于调试和深入理解。其保存逻辑定义在 src/saver.py 中：

# 来源：src/saver.py  
def save_qtree_correction(self, qtree_data, task_id, design_name=None, prompt=None, testbench=None, generated_sva=None, previous_metrics=None, final_metrics=None):  
"""Save a qtree that led to functionality correction"""  
qtree_entry = {  
'qtree_data': qtree_data,  
'task_id': task_id,  
'design_name': design_name,  
'prompt': prompt,  
'testbench': testbench,  
'previous_metrics': previous_metrics,  
'final_metrics': final_metrics,  
'generated_sva': generated_sva  
}  
self.qtree_corrections.append(qtree_entry)  

def dump_qtree_corrections_to_disk(self):  
"""Save all qtree corrections to disk (similar to suggestions)"""  
pkl_filename = os.path.join(self.logdir, "qtrees.pkl")  
with open(pkl_filename, "wb") as pkl_file:  
pickle.dump(self.qtree_corrections, pkl_file)  

json_filename = os.path.join(self.logdir, "qtrees.json")  
with open(json_filename, 'w') as f:  
json.dump(self.qtree_corrections, f, indent=2)

这段代码的设计哲学可以概括为：一次成功的修复，其价值远不止于一个更优的 SVA。它是一条包含了上下文、性能指标、提示词、测试平台以及最终生成结果的“经验记录”。在后续的推理阶段，系统会检索这些记录，从而构成了项目所谓的“规则学习管道”（rule-learning pipeline）。

9.2 与普通 RAG 的本质差异

传统的 RAG（检索增强生成）通常只是简单地将相似的文档片段塞入提示词中。相比之下，FVRuleLearner 的 RAG 机制更像一个经验知识库。它存储的不是孤立的文档，而是包含了完整上下文和修复过程的经验记录，这使得其检索和利用效率远超普通的文档匹配。

Examples 提供了相似的输入与输出对照；
Suggestions 给出了过往的修复方案；
qtrees.json 记录了错误的解析路径；
operator_explanations 提供了 SVA 操作符的背景知识；
JasperGold 则返回了语法与功能方面的反馈。

所以，其核心并非“获取更多上下文”，而是“获取经过验证的纠错经验”。

十、限制、边界与值得借鉴之处

10.1 需要谨慎表述的限制

首先，该项目依赖外部的商业 EDA 工具 JasperGold。README 中明确要求 jg 命令必须位于 PATH 环境变量中，并且需要设置 LM_LICENSE_FILE 与 CDS_LIC_FILE 等环境变量。如果缺少这些条件，语法与功能评估的闭环就无法完整复现。
其次，当前 release 的主线是位于 src/ 目录下的 prompt-only 路径，它并非一个开箱即用的通用 RTL 形式验证平台。整个系统是围绕 NL2SVA 基准测试、CSV 数据集、预设的 Tcl 脚本以及固定的配置来组织的。
第三，配置中存在硬编码的训练 ID，这是为了避免数据泄漏。对于论文实验来说，这种做法是必要的，但也意味着如果要迁移到新的数据集，就需要重新设计数据划分方案和检索池。
第四，部分工程逻辑体现了研究原型的特点，例如评估中的 BLEU=1.0 功能性修正、opencore Tcl 脚本中某些 analyze/elaborate 语句被注释掉，以及 fv_harwareagent_example.py 文件名存在拼写历史的痕迹。这些细节不影响对核心思想的理解，但提醒我们：应将其视为研究代码，而非成熟的商业产品。

10.2 对 AI+EDA 系统的启发

FVRuleLearner 最值得借鉴的，并非某个具体的提示词，而是以下三个系统设计原则：

把失败转化为结构化知识：失败样本如果仅仅用于重试，那它就是成本；但如果将其拆解为 Q-Tree，它就成了经验资产。
让工具评估参与学习闭环：JasperGold 不仅是最终的评分器，更是规则可信度的来源。
检索规则而非照抄答案：对于形式验证这类高精度任务，直接复用答案容易产生偏差，而复用“操作符级别的修正规则”则更具泛化意义。

10.3 如果把它比作编译器

可以将 FVRuleLearner 看作一台“面向断言生成的经验编译器”：

自然语言提示词是源程序；
LLM 是不稳定的前端生成器；
Q-Tree 是错误分析的中间表示（IR）；
suggestions 和 qtrees 是优化流程的知识库；
RAG 是流程管理器；
JasperGold 是后端的验证器；
评估 CSV 是最终的编译报告。

传统编译器将源代码编译成机器码，并借助类型系统、优化器和后端约束来保证正确性；而 FVRuleLearner 则是将自然语言编译成 SVA，并利用规则学习、检索增强和形式工具评估来尽可能缩小语义偏差。

结语：真正的突破在于让形式验证经验可积累

LLM 进入 EDA 领域的早期阶段，最容易展示的能力是“它能写出一段代码”。但对形式验证而言，能写只是起点，能被证明、能被修正、能从修正中学习，才是走向可用系统的关键。FVRuleLearner 的贡献正在于此：它没有把 SVA 生成当成一次性翻译，而是将每一次错误拆解为操作符级别的问题，把每一次修复沉淀为 Q-Tree 和 suggestion，再在新任务中通过 RAG 与排序机制复用这些经验。

这套思路或许不会让 LLM 一夜之间成为形式验证专家，但它提供了一条更工程化的路线：让模型不再孤立地“猜答案”，而是在可追踪、可验证、可积累的规则空间中生成答案。

对于 AI 辅助 EDA 来说，这比单纯提升一次生成的命中率更为重要，因为它指向的是一种长期学习机制：将专家经验、工具反馈和模型推理，合并为一个持续增值的验证知识系统。

参考资料[1]

Operator-Level Reasoning Tree (OP-Tree)-Based Rules Learning for Formal Verification: https://arxiv.org/pdf/2604.03245

NVlabs FVRuleLearner：用算子推理树终结LLM写SystemVerilog断言的时序错误，形式验证正确率飙升