发表机构
DFKI GmbH; University of Bremen（德国人工智能研究中心; 不来梅大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文提出一种基于LLM的行为驱动硬件开发工作流，利用受控自然语言规范（FV Gherkin场景）结合形式化属性验证，显著提升RTL设计功能正确性与断言覆盖率。
AI 中文摘要
近年来，在电子设计自动化（EDA）生命周期中，大型语言模型（LLMs）在不同任务中的应用已被广泛研究，但缺乏一个集成视图。规范是该生命周期的基础，但用自然语言编写时存在歧义，这尤其影响LLM输出的质量。形式化规范减轻了这些歧义，但带来了自身的挑战。另一方面，受控自然语言（CNL）规范可以作为一个中间地带，在减少歧义的同时保持可解释性。在这项工作中，我们提出了LLM在EDA中使用的集成视图，并建立了一个基于LLM的行为驱动硬件开发工作流。我们引入并定义了形式化验证Gherkin场景（FV Gherkin场景），通过形式化属性验证（FPV）解锁CNL规范作为形式化验证硬件设计的基础。实验评估表明，我们的工作流在生成的寄存器传输级（RTL）设计的功能正确性上比其它已建立的基于LLM的方法高出2.48倍，在用于FPV的生成断言的形式化覆盖率上高出2.54倍。
英文摘要
Recently, the use of Large Language Models (LLMs) for different tasks in the Electronic Design Automation (EDA) life-cycle has been studied extensively, but an integrated view is lacking. Specifications are the foundation of this life-cycle, but they suffer from ambiguity when written in natural language, which especially affects the quality of LLM output. Formal specifications mitigate these ambiguities, but they come with their own challenges. On the other hand, Controlled Natural Language (CNL) specifications can serve as a middle-ground, reducing ambiguity while retaining interpretability. In this work, we propose an integrated view on the use of LLMs for EDA and establish an LLM-enabled behavior driven hardware development workflow. We introduce and define Formal Verification Gherkin Scenarios (FV Gherkin Scenarios), unlocking CNL specifications as the foundation for formally verified hardware designs via Formal Property Verification (FPV). Experimental evaluation shows that our workflow is able to outperform other established LLM-based methods by 2.48x in functional correctness of generated Register Transfer Level (RTL) designs and by 2.54x in formal coverage of generated assertions for FPV.
