大模型
arxiv.org ·
面向形式化验证硬件设计的 LLM 赋能行为驱动开发工作流
该论文提出将 LLM 用于 EDA 全生命周期的整合视角，并建立 LLM 赋能的行为驱动硬件开发工作流。作者定义 Formal Verification Gherkin Scenarios（FV Gherkin Scenarios），以受控自然语言（CNL）规格作为形式化验证硬件设计的基础，通过形式属性验证（FPV）落地。实验称其工作流在生成 RTL 设计的功能正确性上优于既有 LLM 方法 2.48 倍，在 FPV 断言的形式化覆盖率上提升 2.54 倍。
AI推荐理由 arXiv 预印本，作者来自硬件架构与软件工程方向，摘要给出了具体方法（FV Gherkin Scenarios、CNL 规格、FPV）和量化对比结果（RTL 功能正确性提升 2.48x、断言形式化覆盖率提升 2.54x），信息密度较高。局限在于仅为预印本、未经同行评审，且实验细节与基线设置未在摘要中展开，2.48x/2.54x 的具体口径无法从片段核实。
78
正文
Computer Science > Hardware Architecture
arXiv:2609.15318 (cs)
[Submitted on 14 Sep 2026]
Title:LLM-enabled Behavior Driven Development Workflow for Formally Verified Hardware Designs
Authors:Luca Müller, Qian Liu, Rolf Drechsler
View a PDF of the paper titled LLM-enabled Behavior Driven Development Workflow for Formally Verified Hardware Designs, by Luca M\"uller and 2 other authors
View PDF
HTML (experimental)
Abstract: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.
Subjects:
Hardware Architecture (cs.AR); Software Engineering (cs.SE)
Cite as:
arXiv:2609.15318 [cs.AR]
(or
arXiv:2609.15318v1 [cs.AR] for this version)
https://doi.org/10.48550/arXiv.2609.15318
Focus to learn more
arXiv-issued DOI via DataCite (pending registration)
Submission history
From: Luca Müller [view email]
[v1]
Mon, 14 Sep 2026 10:08:48 UTC (101 KB)
Full-text links:
Access Paper:
View a PDF of the paper titled LLM-enabled Behavior Driven Development Workflow for Formally Verified Hardware Designs, by Luca M\"uller and 2 other authors
View PDF
HTML (experimental)
TeX Source
view license
Current browse context:
cs.AR
new
|
recent
| 2026-09
Change to browse by:
cs
cs.SE
References & Citations
NASA ADS
Google Scholar
Semantic Scholar
export BibTeX citation
Loading...
BibTeX formatted citation
×
loading...
Data provided by:
Bookmark
Bibliographic Tools
Bibliographic and Citation Tools
Bibliographic Explorer Toggle
Bibliographic Explorer (What is the Explorer?)
Connected Papers Toggle
Connected Papers (What is Connected Papers?)
Litmaps Toggle
Litmaps (What is Litmaps?)
scite.ai Toggle
scite Smart Citations (What are Smart Citations?)
Code, Data, Media
Code, Data and Media Associated with this Article
alphaXiv Toggle
alphaXiv (What is alphaXiv?)
Links to Code Toggle
CatalyzeX Code Finder for Papers (What is CatalyzeX?)
DagsHub Toggle
DagsHub (What is DagsHub?)
GotitPub Toggle
Gotit.pub (What is GotitPub?)
Huggingface Toggle
Hugging Face (What is Huggingface?)
ScienceCast Toggle
ScienceCast (What is ScienceCast?)
Demos
Demos
Replicate Toggle
Replicate (What is Replicate?)
Spaces Toggle
Hugging Face Spaces (What is Spaces?)
Spaces Toggle
TXYZ.AI (What is TXYZ.AI?)
Related Papers
Recommenders and Search Tools
Link to Influence Flower
Influence Flower (What are Influence Flowers?)
Core recommender toggle
CORE Recommender (What is CORE?)
Author
Venue
Institution
Topic
About arXivLabs
arXivLabs: experimental projects with community collaborators
arXivLabs is a framework that allows collaborators to develop and share new arXiv features directly on our website.
Both individuals and organizations that work with arXivLabs have embraced and accepted our values of openness, community, excellence, and user data privacy. arXiv is committed to these values and only works with partners that adhere to them.
Have an idea for a project that will add value for arXiv's community? Learn more about arXivLabs.
Which authors of this paper are endorsers? |
Disable MathJax (What is MathJax?)