2026-01-02

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

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 %%