Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

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

TL;DR

This work presents AssertLLM, an automatic assertion generation framework that processes complete specification document files and demonstrates that 89% of the generated assertions are both syntactically and functionally accurate.

Abstract

Assertion-based verification (ABV) is a critical method to ensure logic designs comply with their architectural specifications. ABV requires assertions, which are generally converted from specifications through human interpretation by verification engineers. Existing methods for generating assertions from specification documents are limited to sentences extracted by engineers, discouraging their practical applications. In this work, we present AssertLLM, an automatic assertion generation framework that processes complete specification documents. AssertLLM can generate assertions from both natural language and waveform diagrams in specification files. It first converts unstructured specification sentences and waveforms into structured descriptions using natural language templates. Then, a customized Large Language Model (LLM) generates the final assertions based on these descriptions. Our evaluation demonstrates that AssertLLM can generate more accurate and higher-quality assertions compared to GPT-4o and GPT-3.5.

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

TL;DR

This work presents AssertLLM, an automatic assertion generation framework that processes complete specification document files and demonstrates that 89% of the generated assertions are both syntactically and functionally accurate.

Abstract

Assertion-based verification (ABV) is a critical method to ensure logic designs comply with their architectural specifications. ABV requires assertions, which are generally converted from specifications through human interpretation by verification engineers. Existing methods for generating assertions from specification documents are limited to sentences extracted by engineers, discouraging their practical applications. In this work, we present AssertLLM, an automatic assertion generation framework that processes complete specification documents. AssertLLM can generate assertions from both natural language and waveform diagrams in specification files. It first converts unstructured specification sentences and waveforms into structured descriptions using natural language templates. Then, a customized Large Language Model (LLM) generates the final assertions based on these descriptions. Our evaluation demonstrates that AssertLLM can generate more accurate and higher-quality assertions compared to GPT-4o and GPT-3.5.

Paper Structure

This paper contains 16 sections, 6 figures, 3 tables.

Table of Contents

  1. Introduction
  2. Methodology
  3. Workflow Overview
  4. Natural Language Analyzer
  5. Waveform Analyzer
  6. Template Generation
  7. Description Generation
  8. Automatic Assertion Generation
  9. Evaluation of Generated Assertions
  10. Case Study
  11. Experimental Setup
  12. Evaluation Metrics
  13. Assertion Generation Quality
  14. Assertion Generation for More Designs
  15. Discussion: the Impact of Specification Quality
  16. ...and 1 more sections

Figures (6)

  • Figure 1: AssertLLM generation and evaluation workflow. AssertLLM incorporates three LLMs, each enhanced with specific techniques for the decomposed tasks: extracting structural information from natural language, extracting structural information from waveform diagrams, and translating extractions into various SVA types. The generated SVAs are further evaluated based on the golden RTL implementations using model checking tools.
  • Figure 2: Prompt and Response Example of LLM Natural Language Analyzer
  • Figure 3: Prompt and Response Example for template generation in LLM Waveform Analyzer
  • Figure 4: Prompt and Response Example for description generation in LLM Waveform Analyzer
  • Figure 5: Prompt and Response Example of LLM SVA Generator
  • ...and 1 more figures