../

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
  • This is also propose a small benchmark
  • It seems to be mostly opencores designs

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

“Our benchmark consists of 20 open-source designs, covering a diverse array of applications including microprocessors, system-on-chip architectures, communication protocols, arithmetic units, and cryptographic modules." Page 6

“IV. EXPERIMENTAL RESULTS” Page 6

“A. Experimental Setup” Page 6

“B. Evaluation Metrics” Page 6

“C. Assertion Generation Quality” Page 7

“To illustrate the efficacy of AssertLLM, we apply it to a comprehensive design case: the ”I2C” protocol." 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-07-11T14:10:38.606-04:00 %%