PaperlayerView exact revision on arXiv

Source-linked AI summary

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

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

arXiv:2402.00386v4cs.AR

TL;DR

Generating high-quality assertions from natural-language specifications is difficult because existing methods often depend on human-extracted sentences and substantial manual effort. AssertLLM processes complete specification files through three specialized LLM phases and supplies an open-source evaluation benchmark. On a complete design with 23 signals, 89% of generated assertions were syntactically and functionally accurate.

  • Problem

    Existing assertion-generation methods are limited by unstructured specifications, human sentence extraction, and the difficulty of producing sufficient high-quality SVAs.

    Source: §I · pp. 1–2

  • Method

    AssertLLM uses specialized LLMs for structural specification extraction, signal-definition mapping, and assertion generation from complete specification files.

    Source: §I · p. 2

  • Results

    89% of generated SVAs were correct both syntactically and functionally in an evaluation covering 23 signals and 56 assertions.

    Source: §I · p. 2, §VI · p. 8

  • Takeaways & Limitations

    AssertLLM supports comprehensive assertion generation and evaluation across architectural signals using an open-source benchmark with golden specifications and RTL designs.

    Source: §I · p. 2, §VI · p. 8

Abstract

from arXiv · show

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.

I. INTRODUCTION

Assertion-based verification checks RTL behavior against specifications, but generating sufficient high-quality SVAs from natural-language documents remains difficult and labor-intensive. AssertLLM addresses this gap by processing complete specification files with specialized LLM stages and an adaptable benchmark, achieving 89% syntactic and functional correctness on a complete design.

Motivation

  • Manual SVA design is time-consuming and error-prone, although ABV is widely used to verify RTL functional behavior against specifications.ABV can use simulation or formal property verification, commonly with SystemVerilog Assertions.Source: §I · p. 1

Prior Work

  • Existing approaches rely on dynamic traces, templates, or machine-learning methods, while specification extraction and design-specific evaluation limit practical generalization.Dynamic methods may inherit RTL flaws, and many pre-RTL methods process engineer-selected sentences rather than complete documents.Source: §I · pp. 1–2

AssertLLM

  • AssertLLM processes complete natural-language specification files and generates comprehensive SVAs for each architectural signal.The framework targets bit-width, connectivity, and functional assertions.Source: §I · p. 2
  • Three customized LLMs separately extract structural information, map signal definitions, and translate specifications into SVA types.The decomposition addresses unstructured specifications and the complexity of combining design understanding with SVA expertise.Source: §I · p. 2

Evaluation Infrastructure

  • The work provides an open-source benchmark containing golden specifications and RTL designs, with model-checking evaluation intended to support varied design types.The benchmark and general evaluation method are presented as adaptable across design types.Source: §I · p. 2, Table I · p. 2

Evaluation

  • 89% of 56 generated SVAs for 23 signals were correct both syntactically and functionally.The assertions covered 23 bit-width, 16 interface, and 17 function checks.Source: §I · p. 2

II. PRELIMINARIES AND PROBLEM FORMULATION

The specification defines architecture-level design information through six complementary parts, while omitting internal RTL signals and providing an open-source implementation.

B. LLM for EDA

LLMs are being explored across EDA tasks, while AssertLLM formulates assertion generation from specification files and evaluates generated assertions against golden RTL implementations.

B. LLM for EDA

  • LLM-based EDA research spans assertion generation, RTL code generation, syntax correction, EDA-tool interaction, accelerator architecture, security fixes, and specification-document support.Source: B. LLM for EDA · p. 3

C. Problem Fromulation

III. METHODOLOGY

AssertLLM decomposes assertion generation from complete specifications into extraction, signal alignment, and SVA generation, using customized LLMs to structure dispersed information.

A. Workflow Overview

  • The workflow uses three customized LLMs and adds an open-source benchmark and evaluation methodology for generated SVAs.Source: A. Workflow Overview · p. 3
  • The three workflow steps are extracting relevant specification information, aligning specification and HDL signal names, and generating high-quality SVAs.Source: A. Workflow Overview · p. 3

B. Specification Information Extraction

A. Workflow Overview

  • Figure 2 presents the generation and evaluation workflow, including structural extraction, signal mapping, SVA translation, and model-checking assessment on golden RTL.Source: Figure 2 · p. 4

B. Specification Information Extraction

  • Figure 3 depicts the custom instructions used by LLM 1 SPEC Analyzer.Source: Figure 3 · p. 4

C. Signal Definition Mapping

Signal Definition Mapping addresses the gap between architecture-level specification signals and internal RTL signals by aligning natural-language names with HDL declarations.

C. Signal Definition Mapping

  • Specifications omit internal wires and registers that appear in detailed RTL implementations, creating a signal-definition gap for assertion generation.Source: C. Signal Definition Mapping · p. 4
  • LLM 2 Signal Mapper aligns natural-language signal names with signal declarations found in initialized HDL code.Source: C. Signal Definition Mapping · p. 4
  • The mapper receives the specification and signal-definition HDL code, examines declarations and comments, and establishes their mapping relationship.Source: C. Signal Definition Mapping · p. 4
  • Figure 4 provides a prompt-and-response example for LLM 1 SPEC Analyzer.Source: Figure 4 · p. 4
  • Figure 5 presents the custom instructions for LLM 2 Signal Mapper.Source: Figure 5 · p. 4

D. Automatic Assertion Generation

AssertLLM generates assertions from structured specifications and mapped signal relationships, using RAG and custom instructions to guide SVA generation.

E. Generated Assertion Evaluation

AssertLLM evaluates generated assertions against bug-free golden RTL with formal property verification and introduces a broad benchmark spanning diverse VLSI designs.

E. Generated Assertion Evaluation

F. Proposed Benchmark

  • The benchmark contains 20 open-source designs covering microprocessors, system-on-chip architectures, communication protocols, arithmetic units, and cryptographic modules.Source: F. Proposed Benchmark · p. 6
  • Each benchmark design provides a complete natural-language specification, HDL signal definitions, and a golden RTL implementation verified to be bug-free.Source: F. Proposed Benchmark · p. 6

IV. EXPERIMENTAL RESULTS

The experiments compare GPT-3.5, GPT-4, and customized AssertLLM using per-signal and per-design metrics for generated, syntax-correct, and FPV-passing SVAs.

A. Experimental Setup

  • The setup evaluates GPT-3.5, GPT-4, and AssertLLM, with AssertLLM customizing GPT-4 Turbo using RAG and task-specific instructions.Source: A. Experimental Setup · p. 6
  • All assertions are generated from a single query, while assertions containing unmapped signals are removed by human engineers before evaluation.Source: A. Experimental Setup · p. 6

B. Evaluation Metrics

  • The evaluation records generated, syntax-correct, and FPV-passed SVA counts for each assertion type and aggregates proportions by design.Source: B. Evaluation Metrics · pp. 6–7
  • Table II evaluates AssertLLM on the I2C design at the design level across 23 signals and 56 generated properties.Source: Table II · p. 7

C. Assertion Generation Quality

On the I2C design, AssertLLM generates width, connectivity, and function assertions for 23 signals, achieving 89% overall correctness while exposing specification-dependent coverage limits.

C. Assertion Generation Quality

D. Ablation Study

The ablation study shows that removing AssertLLM’s structured extraction, assertion-type guidance, and RAG support substantially limits assertion generation and quality. The evaluation discussion also explains why COI coverage is poorly suited to pre-RTL specifications.

D. Ablation Study

  • GPT-4 generated at most 4 SVAs per signal without structured specification extraction and produced only functional assertions without assertion-type guidance.The unstructured file and signal definitions prevented GPT-4 from compiling all useful information for assertion generation.Source: D. Ablation Study · p. 8
  • 8% of GPT-4’s generated assertions were correct overall, with no correct IO-port SVAs and accurate reset checks only for registers.The original model also tended to produce syntax errors, whereas AssertLLM addresses this issue with RAG for SVA and FPV knowledge.Source: D. Ablation Study · p. 8

A. Coverage in SVA Evaluation

  • COI coverage is less applicable at the pre-RTL stage because specifications usually describe IO ports and architectural registers rather than internal signals.COI coverage assumes implementation-level design detail beyond the scope of natural-language specifications.Source: A. Coverage in SVA Evaluation · p. 8

B. Evaluating and Enhancing Specification Quality with AssertLLM

AssertLLM can use assertion-generation performance to assess whether natural-language specifications are sufficiently detailed for verification. The paper further presents this feedback as a way to identify specification gaps, improve verification, and standardize specification writing.

B. Evaluating and Enhancing Specification Quality with AssertLLM

  • AssertLLM can assess specification quality by determining whether documents support a broad and accurate range of generated SVAs.Specifications with clear signal functionalities and connectivities are more verification-friendly than specifications containing only names and simple descriptions.Source: B. Evaluating and Enhancing… · p. 8
  • The framework can identify specification content lacking sufficient detail for SVA generation, guiding architects to provide more comprehensive information.This creates a direct connection between assertion-generation results and gaps in the specification.Source: B. Evaluating and Enhancing… · p. 8
  • Verification-friendly specifications can potentially reduce the time and effort required for verification.The paper presents this as a potential benefit of enhancing specification quality.Source: B. Evaluating and Enhancing… · p. 8
  • Feedback from AssertLLM can help establish specification-writing best practices and promote consistency across design stages.The proposed feedback supports standardizing how specifications are written for automated verification.Source: B. Evaluating and Enhancing… · p. 8

VI. CONCLUSION

  • 89% of assertions generated for a comprehensive 23-signal design were accurate both syntactically and functionally.The paper concludes by pairing this result with AssertLLM’s use for evaluating and enhancing specification quality.Source: §VI · p. 8

Related papers

Loading 2402.00386v4…