Spec2Assertion: Automatic Pre-RTL Assertion Generation using Large Language Models with Progressive Regularization

TL;DR

The paper tackles the labor-intensive task of generating SystemVerilog Assertions by proposing Spec2Assertion, an RTL-agnostic, specification-driven framework that uses large language models with progressive regularization and Chain-of-Thought prompting to produce pre-RTL SVAs. It introduces a four-phase pipeline—Regulated Function Description Extraction, Semantic Regularization, Formal Description Generation, and Regulated Assertion Generation—coupled with a novel evaluation methodology based on Signal Dependency Graphs and assertion-importance scoring. Empirical results show substantial gains over prior work, with $70\%$ more syntax-correct SVAs and roughly $2\times$ higher assertion quality on average, as well as improved formal-verification pass rates. The approach significantly reduces manual effort and enhances bug localization capability, marking a meaningful advance in specification-driven formal verification for hardware design.

Abstract

SystemVerilog Assertions (SVAs) play a critical role in detecting and debugging functional bugs in digital chip design. However, generating SVAs has traditionally been a manual, labor-intensive, and error-prone process. Recent advances in automatic assertion generation, particularly those using machine learning and large language models (LLMs), have shown promising potential, though most approaches remain in the early stages of development. In this work, we introduce Spec2Assertion, a new technique for automatically generating assertions from design specifications prior to RTL implementation. It leverages LLMs with progressive regularization and incorporates Chain-of-Thought (CoT) prompting to guide assertion synthesis. Additionally, we propose a new evaluation methodology that assesses assertion quality across a broad range of scenarios. Experiments on multiple benchmark designs show that Spec2Assertion generates 70% more syntax-correct assertions with 2X quality improvement on average compared to a recent state-of-the-art approach.

Figures (7)

• Figure 1: Overview of Spec2Assertion and its quality evaluation.
• Figure 2: Phase 1. Regulated Function Description Extraction Prompt and the Response Example
• Figure 3: Phase 3. Formal Description Generation Prompt and Response Example
• Figure 4: An example of signal dependency graph, where signal $a$ participates in two events in the antecedent, and there are two signals $b1$ and $b2$ with different transition times in the consequent.
• Figure 5: Top 10 normalized importance scores for I2C.