LLM-enabled Behavior Driven Development Workflow for Formally Verified Hardware Designs

• URL: http://arxiv.org/abs/2609.15318v1
• Date: Mon, 14 Sep 2026 10:08:48 GMT
• Title: LLM-enabled Behavior Driven Development Workflow for Formally Verified Hardware Designs
• Abstract summary: Controlled Natural Language (CNL) specifications can serve as a middle-ground, reducing ambiguity while retaining interpretability.<n>We introduce and define Formal Verification Gherkin Scenarios (FV Gherkin Scenarios), unlocking CNL specifications as the foundation for formally verified hardware designs.
• Score: 6.993866597392993
• License: http://creativecommons.org/licenses/by/4.0/
• 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.

Related papers

• Interpretable and Verifiable Hardware Generation with LLM-Driven Stepwise Refinement [6.8152454268325835]
  Large language models (LLMs) have achieved remarkable success in software development.<n>They are susceptible to hallucinations, meaning that they can introduce subtle semantic and logical errors.<n>We propose a hardware generation framework that combines the creativity and broad knowledge of LLMs with the explainability and mathematical rigor of formal methods.
  arXiv  Detail & Related papers  (2026-06-16T01:28:22Z)
• LLM-Assisted Repository-Level Generation with Structured Spec-Driven Engineering [4.751657370831477]
  State-of-the-art Large Language Models (LLMs) excel in code generation at the function level, but output quality significantly declines when scaling to repository-level systems.<n>To address this, we propose structured spec-driven engineering (SSDE)<n>We argue that structured specifications as LLM inputs make high-quality, repository-level code generation a tangible goal, while at the same time offering superior verifiability.
  arXiv  Detail & Related papers  (2026-05-04T10:58:22Z)
• LLM-FSM: Scaling Large Language Models for Finite-State Reasoning in RTL Code Generation [3.4714122723537333]
  We present LLM-FSM, a benchmark that evaluates how well large language models (LLMs) can recover finite-state machine (FSM) behavior.<n>Unlike prior specification-to-RTL benchmarks that rely on manually constructed examples, LLM-FSM is built through a fully automated pipeline.
  arXiv  Detail & Related papers  (2026-02-03T04:48:26Z)
• Latent Factor Models Meets Instructions: Goal-conditioned Latent Factor Discovery without Task Supervision [50.45597801390757]
  Instruct-LF is a goal-oriented latent factor discovery system.<n>It integrates instruction-following ability with statistical models to handle noisy datasets.
  arXiv  Detail & Related papers  (2025-02-21T02:03:08Z)
• FVEval: Understanding Language Model Capabilities in Formal Verification of Digital Hardware [4.480157114854711]
  We present FVEval, the first comprehensive benchmark for characterizing large language models (LLMs) performance in tasks pertaining to formal verification (FV) The benchmark consists of three sub-tasks that measure LLM capabilities at different levels. We present both collections of expert-written verification collateral and methodologies to scalably generate synthetic examples aligned with FV.
  arXiv  Detail & Related papers  (2024-10-15T21:48:57Z)
• Embodied Agent Interface: Benchmarking LLMs for Embodied Decision Making [85.24399869971236]
  We aim to evaluate Large Language Models (LLMs) for embodied decision making.<n>Existing evaluations tend to rely solely on a final success rate.<n>We propose a generalized interface (Embodied Agent Interface) that supports the formalization of various types of tasks.
  arXiv  Detail & Related papers  (2024-10-09T17:59:00Z)
• SELF-GUIDE: Better Task-Specific Instruction Following via Self-Synthetic Finetuning [70.21358720599821]
  Large language models (LLMs) hold the promise of solving diverse tasks when provided with appropriate natural language prompts. We propose SELF-GUIDE, a multi-stage mechanism in which we synthesize task-specific input-output pairs from the student LLM. We report an absolute improvement of approximately 15% for classification tasks and 18% for generation tasks in the benchmark's metrics.
  arXiv  Detail & Related papers  (2024-07-16T04:41:58Z)
• $\forall$uto$\exists$val: Autonomous Assessment of LLMs in Formal Synthesis and Interpretation Tasks [21.12437562185667]
  This paper presents a new approach for scaling LLM assessment in translating formal syntax to natural language. We use context-free grammars (CFGs) to generate out-of-distribution datasets on the fly. We also conduct an assessment of several SOTA closed and open-source LLMs to showcase the feasibility and scalability of this paradigm.
  arXiv  Detail & Related papers  (2024-03-27T08:08:00Z)
• FOFO: A Benchmark to Evaluate LLMs' Format-Following Capability [70.84333325049123]
  FoFo is a pioneering benchmark for evaluating large language models' (LLMs) ability to follow complex, domain-specific formats. This paper presents FoFo, a pioneering benchmark for evaluating large language models' (LLMs) ability to follow complex, domain-specific formats.
  arXiv  Detail & Related papers  (2024-02-28T19:23:27Z)
• If LLM Is the Wizard, Then Code Is the Wand: A Survey on How Code Empowers Large Language Models to Serve as Intelligent Agents [81.60906807941188]
  Large language models (LLMs) are trained on a combination of natural language and formal language (code) Code translates high-level goals into executable steps, featuring standard syntax, logical consistency, abstraction, and modularity.
  arXiv  Detail & Related papers  (2024-01-01T16:51:20Z)
• Assessing the Reliability of Large Language Model Knowledge [78.38870272050106]
  Large language models (LLMs) have been treated as knowledge bases due to their strong performance in knowledge probing tasks. How do we evaluate the capabilities of LLMs to consistently produce factually correct answers? We propose MOdel kNowledge relIabiliTy scORe (MONITOR), a novel metric designed to directly measure LLMs' factual reliability.
  arXiv  Detail & Related papers  (2023-10-15T12:40:30Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.