arXivAI 研究專業

硬體驗證 AI 的試金石：EquivSVA 形式驗證資料集，揪出 LLM 程式碼生成的虛實

Testing AI Hardware Verification: EquivSVA Dataset Reveals LLM Robustness Across Equivalent RTLs

2026/09/232 分鐘閱讀

硬體驗證 AI 的試金石：EquivSVA 形式驗證資料集，揪出 LLM 程式碼生成的虛實

30 秒看懂

現行 LLM 常用於自動生成晶片設計中的 SystemVerilog 斷言（SVA），但難以評估生成的斷言是真正捕捉到「外部行為」，還是被特定 RTL 實作的細節所綁架。EquivSVA 引入了「行為家族」概念，包含 120 個家族、12 種分類。每個家族內建 4 種結構不同但外部行為等價的 RTL 實作，並附帶標準屬性與突變體，通過 17 項嚴格的形式驗證。基準測試顯示，即使是優秀的 Qwen2.5-Coder，在面對相同功能但不同實作的 RTL 時，生成的正確斷言數量仍有顯著波動，突顯了當前 AI 硬體驗證的穩健性漏洞。

核心重點

行為家族結構設計

每個家族包含 4 個等價但結構不同的 RTL 實作，藉此測試模型是否因實作細節而產生截然不同的斷言品質。

極其嚴格的形式驗證

資料集內所有資料均通過 17 項驗證工作組，包含 RTL 等價性、屬性可達性與突變體區分度，確保無誤導資訊。

暴露出 AI 穩健性漏洞

測試發現，即使外部行為完全一致，主流程式碼模型在 24 個測試家族中有 14 個會因 RTL 實作不同而產生不同數量的正確斷言。

提供標準劃分與開源程式碼

提供家族安全的訓練、開發與測試集劃分，並完整開源生成器、驗證腳本與評估成果。

技術圖解

EquivSVA 行為家族結構與形式驗證流程

為什麼重要

過去評估 LLM 生成硬體斷言（SVA）時，常忽略「等價實作」對 AI 判斷的干擾。EquivSVA 填補了這一空白，透過形式驗證確保資料集本身的絕對正確性。它證明了現今最強的程式碼模型在面對「換湯不換藥」的硬體設計時，生成正確斷言的能力會大幅動搖。這對於自動化晶片驗證、高可信度晶片設計（High-assurance chip design）以及晶片安全評估具有重大指引意義。

對誰有影響

AI 開發者
AI 研究人員
企業決策者

可以怎麼使用

1LLM 硬體斷言（SVA）生成基準測試與穩健性評估
2晶片設計輔助 AI 模型的微調與對齊訓練
3基於突變體的硬體規格自動化分析與漏洞檢測

限制與注意事項

目前僅在 Qwen2.5-Coder-7B-Instruct 上進行了初步基準測試，其他主流大模型的表現仍待社群廣泛驗證。
資料集完全聚焦於 SystemVerilog 斷言（SVA），對於其他硬體驗證或規格描述語言（如 PSL）的適用性仍屬未知。