Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

LAAG-RV: LLM Assisted Assertion Generation for RTL Design Verification

Karthik Maddala, Bhabesh Mali, Chandan Karfa

TL;DR

This work tackles the challenge of generating SystemVerilog Assertions (SVAs) from natural-language design specifications for RTL verification. It introduces LAAG-RV, a framework that employs a custom GPT-4–based LLM and a one-time Verilog synchronization loop to align signal nomenclature with RTL, combined with iterative, error-driven prompts guided by simulator feedback. Experiments on OpenTitan designs show that LLMs can substantially simplify assertion generation, though initial outputs may contain flaws that are corrigible through targeted prompts and human-in-the-loop refinement. The results indicate that LAAG-RV can reduce development effort and improve assertion quality, highlighting the practical value of LLM-assisted ABV while pointing to ongoing needs to ensure completeness and consistency with the design specification.

Abstract

Writing SystemVerilog Assertions (SVA) is an important but complex step in verifying Register Transfer Level (RTL) designs. Conventionally, experts need to understand the design specifications and write the SVA assertions, which is time-consuming and error-prone. However, with the recent advancement of transformer models, the Large Language Models (LLMs) assisted assertion generation for design verification is gaining interest in recent times. Motivated by this, we proposed a novel LLM-based framework, LAAG-RV, to generate SVA from the natural language specifications of the design. Our framework provides a one-time Verilog loop for signal synchronization in the generated SVA to improve the generated assertion quality. For our experiments, we created a custom LLM based on OpenAI GPT-4. Furthermore, we developed test cases to validate the LLM-generated assertions. Initial observations show that some generated assertions contain issues and did not pass all the test cases. However, by iteratively prompting the LLMs using carefully crafted manual prompts derived from test case failures in a simulator, the framework can generate correct SVAs. Our results on OpenTitan designs demonstrate that LLMs significantly simplify the process of generating assertions, making it efficient and less error-prone.

LAAG-RV: LLM Assisted Assertion Generation for RTL Design Verification

TL;DR

This work tackles the challenge of generating SystemVerilog Assertions (SVAs) from natural-language design specifications for RTL verification. It introduces LAAG-RV, a framework that employs a custom GPT-4–based LLM and a one-time Verilog synchronization loop to align signal nomenclature with RTL, combined with iterative, error-driven prompts guided by simulator feedback. Experiments on OpenTitan designs show that LLMs can substantially simplify assertion generation, though initial outputs may contain flaws that are corrigible through targeted prompts and human-in-the-loop refinement. The results indicate that LAAG-RV can reduce development effort and improve assertion quality, highlighting the practical value of LLM-assisted ABV while pointing to ongoing needs to ensure completeness and consistency with the design specification.

Abstract

Writing SystemVerilog Assertions (SVA) is an important but complex step in verifying Register Transfer Level (RTL) designs. Conventionally, experts need to understand the design specifications and write the SVA assertions, which is time-consuming and error-prone. However, with the recent advancement of transformer models, the Large Language Models (LLMs) assisted assertion generation for design verification is gaining interest in recent times. Motivated by this, we proposed a novel LLM-based framework, LAAG-RV, to generate SVA from the natural language specifications of the design. Our framework provides a one-time Verilog loop for signal synchronization in the generated SVA to improve the generated assertion quality. For our experiments, we created a custom LLM based on OpenAI GPT-4. Furthermore, we developed test cases to validate the LLM-generated assertions. Initial observations show that some generated assertions contain issues and did not pass all the test cases. However, by iteratively prompting the LLMs using carefully crafted manual prompts derived from test case failures in a simulator, the framework can generate correct SVAs. Our results on OpenTitan designs demonstrate that LLMs significantly simplify the process of generating assertions, making it efficient and less error-prone.
Paper Structure (16 sections, 3 figures, 1 table)

This paper contains 16 sections, 3 figures, 1 table.

Table of Contents

  1. Introduction
  2. related works and Background
  3. LLM Overview
  4. LLM-Driven Automatic Assertion Generation
  5. System Design Methodology and Case Study
  6. Specification for the LLM
  7. Prompting and Training LLMs
  8. Custom LLM
  9. Design-Specific Prompts to LLMs
  10. Signal Synchronization with Implementation
  11. Error-Specific Prompts
  12. Case study
  13. Experimental Results and Discussion
  14. Results of LAAG-RV
  15. Comparison with ChIRAAG
  16. ...and 1 more sections

Figures (3)

  • Figure 1: SVA Generation flow of LAAG-RV
  • Figure 2: Block Diagram of RV Timer
  • Figure 3: Comparison between the number of LAAG-RV and ChIRAAG Prompts