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

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

4 Nov 2024 | Wenji Fang, Mengming Li, Min Li, Zhiyuan Yan, Shang Liu, Hongce Zhang, Zhiyao Xie
AssertLLM is an automatic assertion generation framework that processes complete specification files to generate SystemVerilog Assertions (SVAs) from natural language specifications. The framework breaks down the complex task into three phases: extracting structural specifications, mapping signal definitions, and generating assertions. It incorporates three customized Large Language Models (LLMs) for each phase. The evaluation of AssertLLM on a full design with 23 I/O signals shows that 89% of the generated assertions are both syntactically and functionally accurate. Hardware functional verification is critical in the VLSI design flow, ensuring that an implementation adheres to its specification. Assertion-based verification (ABV) is a widely adopted technique that uses assertions crafted from specifications to verify the functional behavior of RTL designs. ABV can be conducted through simulation with testbenches or using formal property verification (FPV) techniques. However, generating sufficient, high-quality assertions remains a challenge. Current methods for generating SVAs manually are time-consuming and error-prone. To address this challenge, research has focused on generating SVAs automatically. Automatic approaches can be categorized into dynamic mining from simulation traces and static analysis of specifications. Dynamic methods generate assertions by combining simulating test traces and static analysis of design constraints. However, these methods have limitations as they rely on the same RTL design for both generation and evaluation. Static methods depend on predefined templates or machine learning (ML) technologies. Template-based methods require a deep understanding of the design function, while ML-based methods explore traditional natural language processing (NLP) and emerging Generative AI techniques like LLMs. AssertLLM is the first work that can handle full-size specification files and generate comprehensive types of SVAs for each architectural signal. It also provides the first open-source benchmark for assertion generation and evaluation from natural language specifications. The framework processes complete natural language specification files, automatically producing SVAs for each architectural signal. This approach benefits both design-time bug prevention and verification-time bug detection. The framework includes three customized LLMs: SPEC Analyzer for extracting structural information from specifications, Signal Mapper for mapping signal definitions, and SVA Generator for translating specifications into various SVA types. The resulting SVAs include bit-width, connectivity, and functional assertions. The framework also provides an open-source benchmark to evaluate the quality of the generated SVAs. The evaluation method is designed to be applicable across a variety of design types. In the I2C protocol example, AssertLLM generated 56 SVAs for 23 signals, with 23 for bit-width, 16 for connectivity, and 17 for function. 89% of these generated SVAs were evaluated to be correct both syntactically and functionally. The framework also demonstrates the effectiveness of using AssertLLM to evaluate and enhance the quality of specifications. By identifying gaps between specifications and verification, it can guide architects to provide more comprehensive information. This approach to evaluating specification quality offers benefits such asAssertLLM is an automatic assertion generation framework that processes complete specification files to generate SystemVerilog Assertions (SVAs) from natural language specifications. The framework breaks down the complex task into three phases: extracting structural specifications, mapping signal definitions, and generating assertions. It incorporates three customized Large Language Models (LLMs) for each phase. The evaluation of AssertLLM on a full design with 23 I/O signals shows that 89% of the generated assertions are both syntactically and functionally accurate. Hardware functional verification is critical in the VLSI design flow, ensuring that an implementation adheres to its specification. Assertion-based verification (ABV) is a widely adopted technique that uses assertions crafted from specifications to verify the functional behavior of RTL designs. ABV can be conducted through simulation with testbenches or using formal property verification (FPV) techniques. However, generating sufficient, high-quality assertions remains a challenge. Current methods for generating SVAs manually are time-consuming and error-prone. To address this challenge, research has focused on generating SVAs automatically. Automatic approaches can be categorized into dynamic mining from simulation traces and static analysis of specifications. Dynamic methods generate assertions by combining simulating test traces and static analysis of design constraints. However, these methods have limitations as they rely on the same RTL design for both generation and evaluation. Static methods depend on predefined templates or machine learning (ML) technologies. Template-based methods require a deep understanding of the design function, while ML-based methods explore traditional natural language processing (NLP) and emerging Generative AI techniques like LLMs. AssertLLM is the first work that can handle full-size specification files and generate comprehensive types of SVAs for each architectural signal. It also provides the first open-source benchmark for assertion generation and evaluation from natural language specifications. The framework processes complete natural language specification files, automatically producing SVAs for each architectural signal. This approach benefits both design-time bug prevention and verification-time bug detection. The framework includes three customized LLMs: SPEC Analyzer for extracting structural information from specifications, Signal Mapper for mapping signal definitions, and SVA Generator for translating specifications into various SVA types. The resulting SVAs include bit-width, connectivity, and functional assertions. The framework also provides an open-source benchmark to evaluate the quality of the generated SVAs. The evaluation method is designed to be applicable across a variety of design types. In the I2C protocol example, AssertLLM generated 56 SVAs for 23 signals, with 23 for bit-width, 16 for connectivity, and 17 for function. 89% of these generated SVAs were evaluated to be correct both syntactically and functionally. The framework also demonstrates the effectiveness of using AssertLLM to evaluate and enhance the quality of specifications. By identifying gaps between specifications and verification, it can guide architects to provide more comprehensive information. This approach to evaluating specification quality offers benefits such as
Reach us at info@study.space