AssertLLM: Generating and Evaluating Hardware Verification Assertions from Design Specifications via Multi-LLMs
- Year
- 2024
- Authors
- Wenji Fang, Mengming Li, Min Li, Zhiyuan Yan, Shang Liu, Zhiyao Xie, Hongce Zhang
- DOI
- 10.48550/arXiv.2402.00386
Related
baiAssertionForgeEnhancingFormal2025
Persistent Notes
- They have “three” LLMs to do Spec analyzing, Signal Mapping and SVA Generation
- They are basically customized system prompts to some model
- They test their approach on a golden I2C RTL design
- Their metrics is just syntax and formally proven %
- Their rationale for omitting Coverage is that their approach only uses the spec document, they won’t have access to the internal registers. This makes COI coverage not a suitable choice for them
- Their approach is pre-RTL
In-text annotations
“I. INTRODUCTION” Page 1
“However, a critical limitation of dynamic methods is that both the generation and evaluation of assertions are on the same RTL” Page 1
“design without referring to a golden reference model. This could lead to the generation of incorrect SVAs due to flaws in the RTL design, which these methods might not detect." Page 1
“II. PRELIMINARIES AND PROBLEM FORMULATION” Page 2
“A. Natural Language Specification” Page 2
“B. LLM for EDA” Page 3
“C. Problem Fromulation” Page 3
“B. Specification Information Extraction” Page 3
“C. Signal Definition Mapping” Page 4
“D. Automatic Assertion Generation” Page 4
“Upon inputting the overall architecture diagram of the design, the LLM is provided with the structured specifications and mapped signal relationships from the previous LLMs for each signal." Page 5
Will an architecture diagram be available for every design? Page 5
“E. Generated Assertion Evaluation” Page 5
“F. Proposed Benchmark” Page 6
“IV. EXPERIMENTAL RESULTS” Page 6
“A. Experimental Setup” Page 6
“B. Evaluation Metrics” Page 6
“C. Assertion Generation Quality” Page 7
“D. Ablation Study” Page 8
“V. DISCUSSION” Page 8
“A. Coverage in SVA Evaluation” Page 8
“Given that our SVA generation process is based solely on the information available in the specification documents, which typically detail external interfaces like IO ports and” Page 8
“architectural-level registers rather than internal signals, COI coverage does not align well with our evaluation criteria. This coverage metric assumes a level of design implementation detail that goes beyond the scope of natural language specifications, making it less applicable for assessing the completeness or effectiveness of SVAs generated at this pre-RTL stage." Page 8
“B. Evaluating and Enhancing Specification Quality with AssertLLM” Page 8
“VI. CONCLUSION” Page 8
%% Import Date: 2026-01-02T15:10:52.551-05:00 %%