Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

AssertLLM: Generating and Evaluating Hardware Verification Assertions from Design Specifications via Multi-LLMs

Wenji Fang, Mengming Li, Min Li, Zhiyuan Yan, Shang Liu, Zhiyao Xie, Hongce Zhang

TL;DR

AssertLLM tackles automatic generation of hardware verification assertions from complete natural-language specifications. It decompose into three specialized LLMs: SPEC Analyzer, Signal Mapper, and SVA Generator, augmented with Retrieval Augmented Generation and a golden RTL evaluation framework. It processes complete specification documents, producing SVAs across bit-width, connectivity, and functional categories, and validates them with a formal property verification approach. The work also contributes an open-source benchmark of 20 designs and demonstrates how specification quality can be assessed and improved via the AssertLLM framework.

Abstract

Assertion-based verification (ABV) is a critical method for ensuring design circuits comply with their architectural specifications, which are typically described in natural language. This process often requires human interpretation by verification engineers to convert these specifications into functional verification assertions. Existing methods for generating assertions from natural language specifications are limited to sentences extracted by engineers, discouraging its practical application. In this work, we present AssertLLM, an automatic assertion generation framework that processes complete specification files. AssertLLM breaks down the complex task into three phases, incorporating three customized Large Language Models (LLMs) for extracting structural specifications, mapping signal definitions, and generating assertions. Our evaluation of AssertLLM on a full design, encompassing 23 I/O signals, demonstrates that 89\% of the generated assertions are both syntactically and functionally accurate.

AssertLLM: Generating and Evaluating Hardware Verification Assertions from Design Specifications via Multi-LLMs

TL;DR

AssertLLM tackles automatic generation of hardware verification assertions from complete natural-language specifications. It decompose into three specialized LLMs: SPEC Analyzer, Signal Mapper, and SVA Generator, augmented with Retrieval Augmented Generation and a golden RTL evaluation framework. It processes complete specification documents, producing SVAs across bit-width, connectivity, and functional categories, and validates them with a formal property verification approach. The work also contributes an open-source benchmark of 20 designs and demonstrates how specification quality can be assessed and improved via the AssertLLM framework.

Abstract

Assertion-based verification (ABV) is a critical method for ensuring design circuits comply with their architectural specifications, which are typically described in natural language. This process often requires human interpretation by verification engineers to convert these specifications into functional verification assertions. Existing methods for generating assertions from natural language specifications are limited to sentences extracted by engineers, discouraging its practical application. In this work, we present AssertLLM, an automatic assertion generation framework that processes complete specification files. AssertLLM breaks down the complex task into three phases, incorporating three customized Large Language Models (LLMs) for extracting structural specifications, mapping signal definitions, and generating assertions. Our evaluation of AssertLLM on a full design, encompassing 23 I/O signals, demonstrates that 89\% of the generated assertions are both syntactically and functionally accurate.
Paper Structure (21 sections, 2 equations, 8 figures, 2 tables)

This paper contains 21 sections, 2 equations, 8 figures, 2 tables.

Table of Contents

  1. Introduction
  2. Preliminaries and Problem Formulation
  3. Natural Language Specification
  4. LLM for EDA
  5. Problem Fromulation
  6. Methodology
  7. Workflow Overview
  8. Specification Information Extraction
  9. Signal Definition Mapping
  10. Automatic Assertion Generation
  11. Generated Assertion Evaluation
  12. Proposed Benchmark
  13. Experimental Results
  14. Experimental Setup
  15. Evaluation Metrics
  16. ...and 6 more sections

Figures (8)

  • Figure 1: AssertLLM in VLSI design and verification flow. AssertLLM automatically generates SVAs from natural language specifications, facilitating functional verification for both bug avoidance and bug hunting.
  • Figure 2: AssertLLM generation and evaluation workflow. AssertLLM incorporates three customized LLMs, each enhanced with specific techniques for the decomposed tasks: extracting structural information from specifications, mapping signal definitions, and translating specifications into various SVA types. To evaluate the performance of the generation methods, the generated SVAs are further assessed based on the golden RTL implementations using model checking tools.
  • Figure 3: Custom Instructions for LLM SPEC Analyzer
  • Figure 4: Prompt and Response Example of LLM SPEC Analyzer
  • Figure 5: Custom Instructions for LLM Signal Mapper
  • ...and 3 more figures