../

AssertionForge: Enhancing Formal Verification Assertion Generation with Structured Representation of Specifications and RTL

Year
2025
Authors
Yunsheng Bai, Ghaith Bany Hamad, Syed Suhaib, Haoxing Ren
DOI
10.48550/arXiv.2503.19174

Related

fangAssertLLMGeneratingEvaluating2024

Persistent Notes

  • This works uses both the RTL and the NL specification to generate assertions
  • They compare their work against fangAssertLLMGeneratingEvaluating2024
  • They use these benchmarks
    • APB
    • ETHMAC
    • OPENMSP430
    • SOCKIT
    • UART
  • The metrics used are
    • Number of assertions generated
    • Number of syntactically correct assertions
    • Number of formally proven assertions
    • COI coverage
      • Statement
      • Branch
      • Functional
      • Toggle
Benchmark Proven Proven %
APB 220/615 35.7
ETHMAC 208/1673 12.4
OPENMSP430 327/1600 20.4
SOCKIT 49/448 10.9
UART 50/279 17.9
Benchmark Syntax Syntax %
APB 549/615 .89
ETHMAC 960/1673 .57
OPENMSP430 698/1600 .44
SOCKIT 136/448 .30
UART 174/279 .62

In-text annotations

“I. INTRODUCTION” Page 1

“Specification-focused approaches like ASSERTLLM extract design intent from the often ambiguous and incomplete specifications” Page 1

“Conversely, RTL-focused approaches can capture implementation details but lack understanding of original design intent and high-level functionality, producing assertions that verify implementation without validating adherence to specifications." Page 1

“We hypothesize that explicitly constructing a structured, interconnected mental model of the design—one that links design intent with RTL behavior—will provide a more robust foundation for assertion generation. This mirrors how verification engineers manually synthesize information from multiple sources to write meaningful assertions." Page 1

“II. RELATED WORK” Page 2

“III. METHODOLOGY” Page 2

“IV. EXPERIMENTS” Page 4

“COI Functional Coverage, COI Branch Coverage, COI Statement Coverage, and COI Toggle Coverage," Page 5

“V. CONCLUSION AND FUTURE WORK” Page 6

%% Import Date: 2026-01-02T14:54:51.714-05:00 %%