1 Introduction↩︎

Design verification is a critical stage in the chip design flow, ensuring that an implementation satisfies its intended functional specification. Among different verification methodologies, assertion-based verification (ABV) is widely adopted as it allows design intent to be expressed as formal properties and checked against the RTL implementation. Traditionally, verification engineers manually write properties from design description and encode them as SystemVerilog Assertions (SVAs), while design engineers implement the RTL using a Hardware Description Language (HDL). These SVAs specify the expected functionality of the design and verification tool verify whether the RTL implementation satisfies the specified properties. Manually writing SVAs is labour-intensive and complex, making it time-consuming and prone to human error. Therefore, researchers have now moved towards automatic assertion generation frameworks [1], [2].

The introduction of the Transformer architecture [3] by Google in 2017 has provided the foundation for modern Large Language Models (LLMs). This progress has motivated the use of LLMs in ABV process, particularly focusing on generating functional SVAs automatically. Existing frameworks use diverse strategies for LLM-based assertion generation, including structured specification processing, multi-agent pipelines for information extraction and property generation, RTL-assisted prompting, and evaluation using different quality metrics. These variations raise an important question: How can LLM-based assertion generation be made more systematic and quality-aware by effectively representing design information, including Natural Language Specifications (NLS) and RTL?.

In this paper, we review existing LLM-based assertion-generation works to characterize the current state of the field. Through this analysis, we identify key design choices, limitations, and requirements for developing more systematic and quality-aware LLM-based assertion-generation flows. The results and reports of the case studies performed can be found in [4]. The primary contributions of this paper are as follows:

• We provide a structured study of recent LLM-based assertion-generation frameworks, understanding their prompt inputs, generation strategies, refinement mechanisms, and evaluation methodologies.

• We identify critical quality challenges in LLM-generated assertions, including signal-name inconsistency, vacuous proofs, redundancy, incomplete functional coverage, and misleading coverage inflation, and discuss their impact on formal verification reliability.

• We discuss quality-aware analysis mechanisms for evaluating generated assertions, including vacuity analysis, coverage-based evaluation, and cone-of-influence (COI)-based assertion importance analysis.

• We conducted case studies to demonstrate the impact of different approaches and identified promising directions and provided guidelines for making LLM-based assertion generation systematic and quality-aware

The paper is organized as follows: Section II provides an overview of the different challenges encountered when generating LLM-based SVAs. Section III provides guidelines and directions for resolving the various challenges. Section IV concludes the paper.

2 Challenges in LLM Assisted Assertion Generation↩︎

Assertion checking can be performed either dynamically through simulation-based testbenches (dynamic ABV) or statically using formal verification tools (static ABV). In dynamic ABV, assertions are evaluated over simulation traces, whereas in static ABV, also called as Formal Property Verification (FPV), formal tools construct a state-space representation of the design and exhaustively check whether the specified properties hold over all reachable behaviours. We focus in particular on assertion-based model checking as a formal verification technique. However, properties are traditionally written manually, and for large IPs or industry-level designs, it can take a long time to check them against the implementation. As reported by Wilson Research Group [5], nearly 50% to 60% of chip design development time is spent on the design verification cycle. Therefore, automated assertion generation can reduce the manual effort and complexity involved in design verification. In this Section, we will discuss several challenges in LLM assisted assertion generation.

2.1 Specifications vs RTL↩︎

The first fundamental question that arises in LLM-based assertion generation is: Should we generate assertions from Specification or RTL or should we use both?

Initial Works: Early studies primarily used RTL descriptions as the main source of information for generating assertions. M. Orenes-Vera et al. [6] proposed an iterative correction loop–based framework that uses RTL code to generate functional assertions. While R. Kande et al. [7] proposed an approach to generate assertions from code comments, RTL context, and example assertions using LLMs. However, RTL may not always accurately represent the intended design behaviour, as it can contain bugs or incomplete implementations. Formal assertions are intended to check whether the RTL satisfies the specification. Hence, generating assertions directly from RTL or code comments may produce incomplete or misleading properties. Case Study 1 illustrates the observation of using RTL to generate assertions.

Recent Works: To address this concern, the researchers moved toward specification-driven assertion generation, where specification serves as the primary source of design intent, while RTL is used only as supporting information for signal mapping, refinement, or verification tasks. ChIRAAG [8] is one of the first LLM-based frameworks for generating SVAs from NLS and evaluating them using RTL and a formal verification tool. Then, LAAG-RV [9] introduced the assistance of RTL to preserve consistent signal names between SVAs and the implementation. However, its signal-alignment strategy was not sufficiently strict, leaving scope for further improvement. These works initiated a broader shift toward specification-driven SVA generation, where different frameworks use NLS, structured specifications, waveform descriptions, or knowledge representations to generate formal properties, taking RTL implementation as an assistance. More recent works in this direction include [10]–[12], which are explained in Section III (B). Case Study 2 illustrates the signal name inconsistency problem while generating SVAs.

2.2 Ambiguity in Natural Language Specification↩︎

The second fundamental question is: How can design specifications be represented in a structured form to reduce ambiguity and preserve functional intent consistently during LLM-based SVA generation?

As discussed, the recent frameworks use design specifications as the primary source for generating SVAs. However, design specifications can confuse an LLM when generating the complete set of assertions, as they are sometimes ambiguous and incomplete. This becomes a challenge for researchers to provide a uniform specification to the LLM to generate the assertions. Case Study 3 presents observations on the impact of ambiguity in NLS.

Recent Works: Initial works such as ChIRAAG [8] and LAAG-RV [9] involve extracting the important information from design specifications and transforming them into JSON format. AssertLLM [10] and SANGAM [12] extract signal-wise information from the design specification, where each signal is associated with structured descriptions such as its definition, functionality, interconnections, additional constraints, and related signals. However, SANGAM generates assertions using the Monte Carlo Tree Self-refine (MCTSr) method, forming a tree of depth four where each node in the tree represents a set of assertions. Building on such structured extraction, recent works have explored richer specification representations to provide LLMs with more complete and precise design-intent information, reducing the ambiguity. AssertionForge [11] structured their specification into a Knowledge Graph (KG), containing ports, registers, modules, etc., as node entities and the edges as relationships between them, if they exist. However, they have also used the RTL to further enhance the KG and provide completeness to generate a better set of assertions. While AssertCoder [13] generates SVAs from multimodal design specifications by first segmenting and classifying the specification contents into different modalities, including text, diagrams, formulas, and tables. It uses dedicated LLM-based analyzers for each modality to extract structured semantic information, which is then merged into a unified specification representation to support the SVA generation task. Case Study 4 analyzes the impact of different NLS representations on assertion generation results.

Despite these efforts, there is still no standardized approach for preprocessing and representing design specifications for assertion generation. Directly using raw specifications as input to LLMs may lead to incomplete or inaccurate assertions due to ambiguity, incompleteness, and heterogeneous specification formats. This motivates the need for a structured specification representation that can support robust assertion generation while using RTL only for necessary implementation-level details.

2.3 Assertion Generation and Verification↩︎

The next step after specification processing is the assertion generation. Different frameworks have used different types of LLM(s) and techniques to generate the set of assertion and rectify them.

One-shot Methods: AssertLLM [10], AssertionForge [11] and security assertion generation framework by Kande et.al [7] do not include an explicit FPV-guided rectification loop for rectifying generated SVAs, i.e., the methods are one shot. Kande et.al [7] evaluated the generated assertion set using simulation testbenches, which they described as exhaustive. While AssertLLM [10] and AssertionForge [11] have used FPV tool to evaluate generated SVAs by checking syntax correctness and property pass/fail status.

Rectification Loop-based Methods: An early work [6] generated assertions by prompting LLMs with RTL descriptions. After generation, the assertions were evaluated using an FPV tool to determine whether they were proven or produced counterexamples (CEx). In the case of a CEx, the verification results were manually inspected, and the prompt rules were refined to guide the LLM toward generating corrected assertions. While, testbench-based evaluation and refinement of LLM-generated assertions has been adopted in works such as ChIRAAG [8] and LAAG-RV [9]. These frameworks check the generated assertions for syntax errors and evaluate whether the assertions pass during verification. If an assertion fails or cannot be resolved after a predefined number of refinement attempts, human intervention is required. While [12] is another work that uses an assertion rectification loop, they have used a formal tool and can therefore perform an exhaustive evaluation.

AssertCoder [13], on the other hand, evaluates initially generated LLM assertions through mutation injection and model checking. Specifically, it creates assertion-mutation pairs by injecting mutations into the design and checking whether the generated assertions fail under the mutated behavior. The framework further defines a Mutation Score, which measures the number of unique mutations detected by an assertion. A mutation score of zero indicates that the assertion has low bug-detection capability and should be removed. In addition, AssertCoder defines an aggregate metric, Mutation Detection Rate (MDR), which is used to decide whether the SVA should be regenerated. Case Study 5 reports an observation while using one-shot and loop-based assertion generation methods.

2.4 Assertion Evaluation↩︎

After LLM-guided assertion generation and assertion rectification, the resulting assertion set must be evaluated to determine the quality and effectiveness of the generated assertions.

Existing Works: As such SANGAM [12] uses coverage metrics such as Branch Coverage, Property Coverage and Toggle Coverage to check how much of the design implementation is actually been covered by the LLM-generated assertions. Similarly, AssertionForge [11] used Statement, Branch, Functional and Toggle coverage metrics to check the quality of generated assertions. While [8]–[10], [13] haven’t used any coverage metrics, rather relied on the whether the assertions are proven without any CEx. Also, existing LLM-based assertion generation frameworks have not taken strong measures to address the signal mapping process.

While prior works [9], [11], [12] introduce preliminary mechanisms to improve consistency between generated assertions and RTL signals, their prompt-based strategies do not appear sufficiently robust. The main concern is that signal inconsistency between the RTL implementation and the generated assertions can lead to vacuous proofs. In particular, if an antecedent signal used in an assertion is not present in the RTL and the LLM is hallucinated during assertion generation from the NLS, the antecedent may never be activated, causing the assertion to be proven vacuously within a few cycles. This can falsely inflate the reported coverage metrics. This motivates the need for new analysis metrics and mitigation strategies to reduce such issues. Case Study 6 highlights the insufficiency of existing evaluation metrics and the need for vacuity analysis.

2.5 Quality of the Generated Assertion↩︎

Existing SOTA LLM-based assertion generation frameworks, such as SANGAM [12], AssertLLM [10], and AssertionForge [11], provide limited mechanisms for rigorously evaluating the quality of the final generated assertion set. In particular, they do not strongly analyze: (1) whether the final assertion set contains redundant assertions, and (2) whether some assertions are logically dependent on, or weaker than, other assertions in the set. Identifying such redundancy and dependency is important, as removing equivalent or weaker assertions can reduce the size of the assertion set without significantly degrading evaluation metrics. This motivates the need for additional assertion-reduction techniques that retain only a compact and high-quality set of assertions.

2.6 Handling Long-Context Design Specifications↩︎

LLMs have a limited context window, which restricts the amount of specification, RTL, and auxiliary information that can be provided in a single prompt [14]. Directly providing such documents to an LLM for functional assertion generation may produce unstable, incomplete, or inconsistent assertion sets. This issue becomes more critical for industrial IPs/designs, where both the specifications and RTL implementations are typically larger, more complex, and richer in design intent. These observations motivate the need to organize, abstract, and transform specification and RTL information into a structured representation that preserves functional behavior while enabling scalable LLM-based assertion generation.

3 Guidelines and Future Directions↩︎

With respect to the existing works and experiments performed, we provide some guidelines for the future researchers to generate SVA using LLM, while integrating them into their framework. Fig. 6 shows an overview of the different steps involved in LLM-based SVA generation.

3.1 SVA should be generated from design specification↩︎

In LLM-based SVA generation, the primary source of input should always be the design specification. However, RTL can be used as an assistance in certain steps such as signal mapping, FPV etc. The RTL functionality should never be used to generate SVA assertions.

3.2 Mandatory addition of precise signal mapping step in the framework↩︎

In LLM-based SVA generation, signal mapping is a critical preprocessing step. In practical verification settings, design and verification engineers typically agree on the input, output, wire, and register names before implementing the RTL and writing the corresponding properties. Therefore, before generating assertions, the RTL signal names (input/output ports/ wires/registers) should be extracted and provided to the LLM with strict instructions to use only valid RTL signals and avoid introducing any undeclared or specification-only signal names. Any generated signal that does not exactly match an RTL signal should be mapped to the closest valid RTL signal before formal verification.

3.3 Resolving Ambiguity in NLS with Advanced representation↩︎

To reduce ambiguity in NLS, a KG-based specification representation can serve as an effective preprocessing step, where signals, such as inputs, outputs, wires, and registers, and design elements are modeled as nodes, while their interactions are modeled as edges. The RTL can also be used as an assistance to add missing or incomplete signal-level information; however, it should not be treated as the primary source of design intent.

3.4 Beyond Coverage Metrics: Evaluating LLM-based SVAs↩︎

As we have discussed and shown in Case Study 6, the coverage metrics are insufficient. In this regard, we discuss several possible directions below:

(1) Beyond coverage metrics, another important quality indicator is the Vacuity Metric. This metric helps distinguish assertions that are genuinely proven by the formal tool from those that are proven vacuously due to issues such as inactivated antecedents, over-constrained environments, or signal name mismatches etc. FV tools, such as Cadence JasperGold, report vacuous and non-vacuous properties, which can be used to quantify the extent of vacuous proofs in the generated assertion set. Furthermore, the vacuous assertion set can be passed to an LLM-based refinement framework to identify and mitigate the underlying causes of vacuity, including signal mismatches between the generated assertions and the RTL implementation at that level.

(2) Another important aspect to investigate is the Cone-of-Influence (COI) of each assertion (wrt signals). By identifying unique COIs, one can analyze the functional impact of individual assertions on the design. Assertions with broader or more distinct COIs may be prioritized first, and their contribution can be evaluated using coverage metrics. Subsequently, additional assertions whose COIs cover lower-priority or previously uncovered design regions can be incrementally added, while observing the corresponding changes in coverage. This process can help identify the most influential assertions that fully or partially capture the functional behavior of the design.

3.5 Redundant and weak assertions should be removed from the final assertion set.↩︎

After generating the final assertion set, additional steps should be taken to analyze redundant and weak assertions. Since FPV can be time-consuming, reducing the assertion set while preserving its functional intent can help improve verification efficiency. One possible direction is to perform redundancy and strong/weak analysis among the generated assertions. Redundant assertions can be identified through equivalence checking between assertion pairs; if two assertions are equivalent, one of them can be removed [15]. After eliminating redundant assertions, strong/weak relationships can be analyzed. If one assertion is stronger than another, the weaker assertion can be removed, as it is subsumed by the stronger one [15].

3.6 Inclusion of Rectification Loop↩︎

Current LLM-based assertion generation methods remain prone to errors, as LLMs may misinterpret prompts or generate incorrect responses. Therefore, instead of using one-shot methods to generate assertions, future frameworks should use a formal log-guided rectification loop. In such a loop, an FPV tool verifies the generated SVAs against the RTL implementation and produces logs that capture syntactic errors, semantic errors, and counterexamples. These logs, together with the original assertions, can then be provided to an LLM for refinement, enabling the generation of a more correct assertion set.

3.7 Long-Context problem should be handled with advanced representation of NLS and RTL↩︎

To address this challenge, one promising direction is to structure and utilize large-scale specification and RTL information through signal-wise representations. Tools such as Microsoft GraphRAG [16], LlamaIndex [17] etc., can be used to construct a structured representation, e.g., a knowledge graph, of both the specification and RTL in a signal-wise manner. In such settings, generating all possible functional assertions in a single step may be ineffective. Instead, assertions can be generated incrementally at the signal level. For example, when using a KG, the relevant specification information associated with each target signal can be retrieved and organized into a signal-specific context. This context can then be provided to an LLM for assertion generation, avoiding the need to supply the entire design information in a single prompt.

4 Conclusion↩︎

In this paper, we present a detailed analysis of recent LLM-based SVA-generation frameworks. We examine how existing methods use RTL implementations, NLS, or both as input sources for assertion generation. We further analyze different design-representation strategies for extracting assertion-relevant information and discuss the evaluation metrics used to assess the quality of LLM-generated SVAs. Furthermore, we provide Key Takeaways and guidelines which can serve as practical direction for the future researchers for generating high-quality assertion sets.

References↩︎