Table of Contents
Fetching ...

ChIRAAG: ChatGPT Informed Rapid and Automated Assertion Generation

Bhabesh Mali, Karthik Maddala, Vatsal Gupta, Sweeya Reddy, Chandan Karfa, Ramesh Karri

TL;DR

The paper addresses the bottleneck of manually crafting SystemVerilog Assertions for ABV by introducing ChIRAAG, a framework that converts natural-language design specifications into a standardized JSON format and uses GPT-4 to generate SVAs. It employs a log-driven refinement loop, where simulation outputs ($W_{log}$) guide iterative corrections, up to a bound $T$ iterations, achieving accurate SVAs with minimal human intervention. Evaluated on OpenTitan designs, ChIRAAG consistently generates SVAs quickly (less than $15$ seconds per design) and can even reveal or fix implementation bugs, with only $27\%$ requiring refinement after initial generation. The approach demonstrates that LLM-assisted, specification-driven SVA generation can streamline ABV workflows, though domain-specific models and formal checks remain important for ensuring completeness and correctness.

Abstract

System Verilog Assertion (SVA) formulation -- a critical yet complex task is a prerequisite in the Assertion Based Verification (ABV) process. Traditionally, SVA formulation involves expert-driven interpretation of specifications, which is time-consuming and prone to human error. Recently, LLM-informed automatic assertion generation is gaining interest. We designed a novel framework called ChIRAAG, based on OpenAI GPT4, to generate SVA from natural language specifications of a design. ChIRAAG constitutes the systematic breakdown of design specifications into a standardized format, further generating assertions from formatted specifications using LLM. Furthermore, we used few test cases to validate the LLM-generated assertions. Automatic feedback of log messages from the simulation tool to the LLM ensures that the framework can generate correct SVAs. In our experiments, only 27% of LLM-generated raw assertions had errors, which was rectified in few iterations based on the simulation log. Our results on OpenTitan designs show that LLMs can streamline and assist engineers in the assertion generation process, reshaping verification workflows.

ChIRAAG: ChatGPT Informed Rapid and Automated Assertion Generation

TL;DR

The paper addresses the bottleneck of manually crafting SystemVerilog Assertions for ABV by introducing ChIRAAG, a framework that converts natural-language design specifications into a standardized JSON format and uses GPT-4 to generate SVAs. It employs a log-driven refinement loop, where simulation outputs () guide iterative corrections, up to a bound iterations, achieving accurate SVAs with minimal human intervention. Evaluated on OpenTitan designs, ChIRAAG consistently generates SVAs quickly (less than seconds per design) and can even reveal or fix implementation bugs, with only requiring refinement after initial generation. The approach demonstrates that LLM-assisted, specification-driven SVA generation can streamline ABV workflows, though domain-specific models and formal checks remain important for ensuring completeness and correctness.

Abstract

System Verilog Assertion (SVA) formulation -- a critical yet complex task is a prerequisite in the Assertion Based Verification (ABV) process. Traditionally, SVA formulation involves expert-driven interpretation of specifications, which is time-consuming and prone to human error. Recently, LLM-informed automatic assertion generation is gaining interest. We designed a novel framework called ChIRAAG, based on OpenAI GPT4, to generate SVA from natural language specifications of a design. ChIRAAG constitutes the systematic breakdown of design specifications into a standardized format, further generating assertions from formatted specifications using LLM. Furthermore, we used few test cases to validate the LLM-generated assertions. Automatic feedback of log messages from the simulation tool to the LLM ensures that the framework can generate correct SVAs. In our experiments, only 27% of LLM-generated raw assertions had errors, which was rectified in few iterations based on the simulation log. Our results on OpenTitan designs show that LLMs can streamline and assist engineers in the assertion generation process, reshaping verification workflows.
Paper Structure (8 sections, 2 figures, 2 tables, 1 algorithm)

This paper contains 8 sections, 2 figures, 2 tables, 1 algorithm.

Figures (2)

  • Figure 1: ChIRAAG-SVA Generation Framework
  • Figure 2: Block Diagram of RV Timer