Papers for

verification teams in semiconductor companies

Papers whose findings have a practical use for this group, as judged from the abstract. Open a paper to read what it means in practice.

Llm guided workflow improves hardware design correctness and verification

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

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.

Mon 14 SeptHardware ArchitectureSoftware Engineering

The gist

Hardware designers often write the instructions for circuits in regular language, which can be unclear and cause mistakes. The authors present a method that uses large language models (LLMs) with a specially structured, clearer language to write hardware behaviors and verify them formally. This approach, called Formal Verification Gherkin Scenarios, helps produce more accurate hardware designs that are easier to check for correctness. Their tests show that this method creates designs that function better and have more thorough verification compared to current LLM-based techniques.

Open → 2609.15318v1