深度分析
結合形式化規格與 LLM 的硬體生成：從需求到可合成 RTL 的逐步細化
隨著大型語言模型在軟體開發上的突破，硬體設計仍面臨錯誤風險。本研究提出結合形式化方法的逐步細化框架，讓LLM在每一步都受到可驗證規則約束，最終產生正確的RTL程式。實驗顯示此流程在VerilogEval基準上穩定生成符合規範的硬體描述。此技術有望加速晶片設計流程，降低人力成本。
深度分析
隨著大型語言模型在軟體開發上的突破，硬體設計仍面臨錯誤風險。本研究提出結合形式化方法的逐步細化框架，讓LLM在每一步都受到可驗證規則約束，最終產生正確的RTL程式。實驗顯示此流程在VerilogEval基準上穩定生成符合規範的硬體描述。此技術有望加速晶片設計流程，降低人力成本。
速報
以人工智慧輔助程式撰寫的潮流面臨兩大障礙：目標難以精準轉為提示（提示工程實際上屬於需求工程的一環）以及AI產生幻覺導致錯誤輸出。為提升程式實用性與正確性，研究主張把人工智慧的創意與形式化規格方法、形式化程式驗證結合，並以現代證明工具支援。