LLM 生成的 SystemVerilog 断言对保留语义的 RTL 转换的鲁棒性

arXiv:2609.05658v1 公告类型：新 摘要：人们越来越多地探索大型语言模型 (LLM) 来自动生成 SystemVerilog 断言 (SVA)，但大多数评估报告输入的单个语法表示的正确性。这样的点精度并不能揭示当相同的 RTL 行为以不同的方式编写时模型的正确输出是否稳定。本文提出了在保留语义的 RTL 转换下基于 LLM 的 SVA 生成的受控变形评估。从 VERT 数据集开始，我们构建了一个质量过滤的条件控制池和一个包含 295 个分配行为的分层 40 程序评估集。我们使用相同的评估提示和贪婪解码来评估两个开放代码模型 Qwen2.5-Coder-7B 和 DeepSeek-Coder-V2-Lite。研究了三种转换：操作数重新排序、确定性标识符重命名和冗余括号。除了基线和转换精度之外，我们还通过 RTL 程序级别的 10,000 个样本集群引导间隔来测量条件鲁棒性、不变性故障和任意翻转率。在所有六种模型转换条件中，原始 RTL 上正确的行为中有 9.7%-27.0% 在语义保留转换后变得不正确。因此，聚合准确度可能会隐藏很大的不稳定性：在标识符重命名下，DeepSeek-Coder-V2-Lite 的准确度从 53.9% 提高到 63.7%，而其最初正确的行为有 19.5% 失败。对 30 个采样的正确到错误转换的手动审查可识别丢失的路径谓词、分支极性错误、布尔结构损坏和输出契约违规。结果表明，仅点精度不足以表征断言生成中的 LLM 可靠性，并不足以激发人工智能辅助硬件验证的鲁棒性感知评估。