Iterative LLM-Based Assertion Generation Using Syntax-Semantic Representations for Functional Coverage-Guided Verification

TL;DR

This work tackles the challenge of generating high-quality SystemVerilog assertions (SVAs) from natural-language specifications by addressing gaps in functional coverage. It proposes CoverAssert, a six-module framework that uses syntax-semantic feature fusion, AST-based signal structure, and a coverage-driven feedback loop to iteratively guide LLM-based SVA generators toward uncovered functional points. By splitting specifications into Sub-SPECs, mapping assertions to precise functional points, and terminating when match degree exceeds $\theta=0.85$, CoverAssert enables targeted improvements in assertion quality. Experimental results on four open-source designs show substantial gains in branch, statement, and toggle coverage when integrated with AssertLLM and Spec2Assertion, demonstrating practical impact for ABV and FPV workflows.

Abstract

While leveraging LLMs to automatically generate SystemVerilog assertions (SVAs) from natural language specifications holds great potential, existing techniques face a key challenge: LLMs often lack sufficient understanding of IC design, leading to poor assertion quality in a single pass. Therefore, verifying whether the generated assertions effectively cover the functional specifications and designing feedback mechanisms based on this coverage remain significant hurdles. To address these limitations, this paper introduces CoverAssert, a novel iterative framework for optimizing SVA generation with LLMs. The core contribution is a lightweight mechanism for matching generated assertions with specific functional descriptions in the specifications. CoverAssert achieves this by clustering the joint representations of semantic features of LLM-generated assertions and structural features extracted from abstract syntax trees (ASTs) about signals related to assertions, and then mapping them back to the specifications to analyze functional coverage quality. Leveraging this capability, CoverAssert constructs a feedback loop based on functional coverage to guide LLMs in prioritizing uncovered functional points, thereby iteratively improving assertion quality. Experimental evaluations on four open-source designs demonstrate that integrating CoverAssert with state-of-the-art generators, AssertLLM and Spec2Assertion, achieves average improvements of 9.57 % in branch coverage, 9.64 % in statement coverage, and 15.69 % in toggle coverage.

Figures (6)

• Figure 1: Our proposed framework, CoverAssert, directly enhances assertion generation by accurately identifying uncovered functional descriptions in the specification and providing feedback to prioritize the completion of uncovered functional points, thereby improving overall verification coverage.
• Figure 2: CoverAssert integrates with existing assertion generation methods by extracting semantic and structural features of assertions and signals, which are fused and clustered, then matched with segmented Sub-SPECs. Insufficiently covered Sub-SPECs and their functional descriptions are fed back to guide targeted assertion generation, thereby improving coverage.
• Figure 3: Flowchart of clustering process via fusion of structural and semantic features of assertions.
• Figure 4: Flowchart of the matching process between assertions, Sub-SPECs, and functional points.
• Figure 5: FPV pass-rate evolution across feedback iterations.