LLM生成的断言在代码改写后稳定性差,需改进评估方式
Robustness of LLM-Generated SystemVerilog Assertions to Semantics-Preserving RTL Transformations
- 用语义不变的RTL变换测试LLM生成断言的鲁棒性
- 10%-27%正确断言在变换后变错,最高19.5%原正确项失败
- 适合关注AI硬件验证可靠性的研究人员
大型语言模型(LLMs)正被用于自动化SystemVerilog断言(SVA)生成,但多数评估仅基于单一语法表示的正确率,无法反映相同行为以不同写法表达时模型输出的稳定性。本文通过受控的元测试评估方法,在语义保持的RTL变换下检验基于LLM的SVA生成能力。基于VERT数据集,构建了质量筛选后的条件控制池和包含295种赋值行为的40程序分层评估集。评估Qwen2.5-Coder-7B与DeepSeek-Coder-V2-Lite两个开源代码模型,使用相同提示和贪婪解码。研究三种变换:操作数重排、确定性标识符重命名、冗余括号添加。除基础准确率外,还测量条件鲁棒性、非不变性失败率及任意翻转率,采用10,000样本聚类自举区间进行程序级分析。在所有六种模型-变换组合中,9.7%-27.0%原本正确的行为在变换后变为错误。聚合准确率可能掩盖显著不稳定性:在标识符重命名下,DeepSeek-Coder-V2-Lite准确率从53.9%提升至63.7%,但19.5%的原正确行为失效。对30个正确转错误样本的手动审查发现,问题包括路径谓词丢失、分支极性错误、布尔结构破坏和输出契约违反。结果表明,仅靠点准确率不足以刻画LLM在断言生成中的可靠性,亟需引入鲁棒性意识的评估范式以支持人工智能辅助硬件验证。
原文摘要 · Abstract (English)
Large language models (LLMs) are increasingly being explored for automating SystemVerilog Assertion (SVA) generation, yet most evaluations report correctness on a single syntactic representation of an input. Such point accuracy does not reveal whether a model's correct output is stable when the same RTL behavior is written differently. This paper presents a controlled metamorphic evaluation of LLM-based SVA generation under semantics-preserving RTL transformations. Starting from the VERT dataset, we construct a quality-filtered conditional-control pool and a stratified 40-program evaluation set containing 295 assignment behaviors. We evaluate two open code models, Qwen2.5-Coder-7B and DeepSeek-Coder-V2-Lite, with an identical evaluation prompt and greedy decoding. Three transformations are studied: operand reordering, deterministic identifier renaming, and redundant parenthesization. Beyond baseline and transformed accuracy, we measure conditional robustness, invariance failure, and any-flip rate, with 10,000-sample clustered bootstrap intervals at the RTL-program level. Across all six model-transformation conditions, 9.7%-27.0% of behaviors that were correct on the original RTL become incorrect after a semantics-preserving transformation. Aggregate accuracy can therefore hide substantial instability: under identifier renaming, DeepSeek-Coder-V2-Lite improves from 53.9% to 63.7% accuracy while 19.5% of its originally correct behaviors fail. Manual review of 30 sampled correct-to-wrong transitions identifies dropped path predicates, branch-polarity errors, Boolean-structure corruption, and output-contract violations. The results show that point accuracy alone is insufficient for characterizing LLM reliability in assertion generation and motivate robustness-aware evaluation for AI-assisted hardware verification.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。