The remarkable reasoning and code generation capabilities of large language models (LLMs) have recently motivated increasing interest in automating formal verification (FV), a process that ensures hardware correctness through mathematically precise assertions but remains highly labor-intensive, particularly through the translation of natural language into SystemVerilog Assertions (NL-to-SVA). However, LLMs still struggle with SVA generation due to limited training data and the intrinsic complexity of FV operators. Consequently, a more efficient and robust methodology for ensuring correct SVA operator selection is essential for producing functionally correct assertions. To address these challenges, we introduce FVRuleLearner, an Operator-Level Rule (Op-Rule) learning framework built on a novel Operator Reasoning Tree (Op-Tree), which models SVA generation as structured, interpretable reasoning. FVRuleLearner operates in two complementary phases: (1) Training: it constructs Op-Tree that decomposes NL-to-SVA alignment into fine-grained, operator-aware questions, combining reasoning paths that lead to correct assertions; and (2) Testing: it performs operator-aligned retrieval to fetch relevant reasoning traces from the learned Op-Tree and generate new rules for unseen specifications. In the comprehensive studies, the proposed FVRuleLearner outperforms the state-of-the-art baseline by 3.95% in syntax correctness and by 31.17% in functional correctness on average. Moreover, FVRuleLearner successfully reduces an average of 70.33% of SVA functional failures across diverse operator categories through a functional taxonomy analysis, showing the effectiveness of applying learned Op-Tree to the Op-Rule generations for unseen NL-to-SVA tasks. These results establish FVRuleLearner as a new paradigm for domain-specific reasoning and rule learning in formal verification.
Figures & tables
Fig. 1 : Given a NL-to-SVA task, LLM inference often produces functionally incorrect SVAs, whereas our FVRuleLearner framework leverages learned Op-Tree to generate functionally correct SVAs.
Operator Category
Representative Operators
Temporal Implication Operators
|-> , |=>
Temporal Delay Operators
##m , [m:n]
Temporal Sampling Operators
past,rose , fell,stable
Temporal Liveness Operators
s_eventually , s_always , strong
Combinational Logic Operators
&& , || , ! , == , !== , ˆ
Miscellaneous Differences
@(posedge clk) , disable iff(rst)
TABLE I : Operator Categories and SystemVerilog Operators Table.
Fig. 2 : Operator-level functional mismatch analysis between generated and golden SVAs across three datasets. Temporal operators dominate the errors, highlighting the need for operator-aware reasoning.
Fig. 3 : Comparison between General Rules and Op-Rules.
Fig. 4 : The flow overview of FVRuleLearner and an illustration of Op-Tree in training. (a) Training phase: The framework leverages Op-Tree to consolidate the operator-level reasoning traces and they are stored in T∗ . (b) Testing phase: FVRuleLearner firstly generates initial SVA ( y^init ) and retrieve relevant Op-Tree from T∗ according to the similarity score of natural language specification of testing data and the background nodes’ natural language content. Then, the candidate reasoning traces are selected based on the proposed operator alignment and semantic applicability scores. Lastly, the rule adaption step generate Op-Rules for final SVA ( y^ ). (c) An illustrative example of the Op-Tree reasoning process, showing how hierarchical decomposition links design context to theoretical definitions to produce a verified correction rule.
Model / Method
NL2SVA-Human
NL2SVA-Machine
NL2SVA-OpenCore
BLEU
Syn
Func
R.Func
BLEU
Syn
Func
R.Func
BLEU
Syn
Func
R.Func
GPT-4o
FVEval-0-shot
0.5203
0.9333
0.5333
0.6667
0.6054
0.9500
0.4167
0.4500
0.6145
0.9250
0.7050
0.7200
FVEval-3-shot
0.5823
0.9333
0.4000
0.6000
0.6461
0.9500
0.4333
0.5167
0.6187
0.8950
0.6750
0.6950
Ensemble
0.5876
0.8667
0.4000
0.4667
0.6562
0.9667
0.5000
0.6000
0.5922
0.9550
0.7000
0.7150
FVRuleLearner
0.6846
1.0000
0.8000
0.8000
0.7072
0.9667
0.7500
0.8167
0.6976
0.9900
0.8500
0.8750
TABLE II: Experimental Results of LLM Models on NL2SVA-Human , NL2SVA-Machine , and NL2SVA-OpenCore Testing Sets.
Fig. 5 : Comparison of fixing ratio trends over training iterations for FVRuleLearner (circle) versus General Rule Learning (square) methods. Across (a) NL2SVA-Human , (b) NL2SVA-Machine , and (c) NL2SVA-OpenCore , the proposed Op-Tree rules learning methodology consistently accelerates convergence and achieves higher final accuracy, improving the fixing rate by an average of 23.33%.
Fig. 6 : Effect of Training Data Ratio on FVRuleLearner Performance on the NL2SVA-Machine dataset.
Model / Method
Syn
Func
R.Func
o3-mini
FVEval-3-shot
0.9500
0.4833
0.5833
General Rules
0.9500
0.6667
0.7500
Static Op-Rules
0.9500
0.7167
0.7833
FVRuleLearner
0.9667
0.7833
0.8333
TABLE III : Rule Retrieval Ablation Study Results for o3-mini on NL2SVA-Machine Dataset.
Op. Category
NL2SVA-Human
NL2SVA-Machine
NL2SVA-OpenCore
Base
Ours
Red.
Base
Ours
Red.
Base
Ours
Red.
Temp. Impl.
4
1
-75%
19
4
-79%
41
5
-88%
Temp. Delay
2
0
-100%
1
0
-100%
20
9
-55%
Temp. Sampl.
0
0
–
3
2
-33%
2
1
-50%
Temp. Live.
1
0
-100%
4
3
-25%
0
0
–
Comb. Logic
0
0
–
2
2
0%
0
0
–
TABLE IV : Operator-Level Failure Analysis showing the reduction in functional mismatches. The “Red.” column indicates the percentage reduction, where bold blue values highlight significant improvements achieved by FVRuleLearner . “Red.” is the percentage reduction (Temp.=Temporal, Comb.=Combinational, Impl. =Implication, Sampl.=Sampling, Live.=Liveness).
Functional verification consumes over 50% of the IC development lifecycle, where SystemVerilog Assertions (SVAs) are indispensable for formal property verification and enhanced simulation-based debugging. However, manual SVA authoring is labor-intensive and error-prone. While Large Language Models (LLMs) show promise, their direct deployment is hindered by low functional accuracy and a severe scarcity of domain-specific data. To address these challenges, we introduce ChatSVA, an end-to-end SVA generation system built upon a multi-agent framework. At its core, the AgentBridge platform enables this multi-agent approach by systematically generating high-purity datasets, overcoming the data scarcity inherent to few-shot scenarios. Evaluated on 24 RTL designs, ChatSVA achieves 98.66% syntax and 96.12% functional pass rates, generating 139.5 SVAs per design with 82.50% function coverage. This represents a 33.3 percentage point improvement in functional correctness and an over 11x enhancement in function coverage compared to the previous state-of-the-art (SOTA). ChatSVA not only sets a new SOTA in automated SVA generation but also establishes a robust framework for solving long-chain reasoning problems in few-shot, domain-specific scenarios. An online service has been publicly released at https://www.nctieda.com/CHATDV.html.
Lik Tung Fu, Jie Zhou, Shaokai Ren +6
National ASIC Center, School of Integrated Circuits, Southeast University, China · National Center of Technology Innovation for Electronic Design Automation, China · Department of Computer Science, City University of Hong Kong, Hong Kong, China
Recent advances in Large Language Models (LLMs) have enabled workflows that generate SystemVerilog Assertions (SVAs) from natural-language specifications, with the potential to accelerate Formal Verification (FV). However, high-quality assertion synthesis remains challenging because specifications are often ambiguous or incomplete and critical micro-architectural details reside in the Register Transfer Level (RTL). Many existing approaches treat the specification and RTL as loosely structured text, which weakens specification-to-RTL grounding and leads to semantic mismatches and frequent syntax failures during formal parsing and elaboration. This work addresses these limitations with a verification-centric Knowledge Graph (KG) constructed from structured Intermediate Representations (IRs) extracted from the specification, RTL, and formal-tool feedback, including syntax diagnostics, Counterexamples (CEXs), and coverage reports. The KG links requirements, design hierarchy, signals, assumptions, and properties to provide traceable, design-grounded context for generation. A multi-agent workflow queries and updates this KG to generate SVAs and to drive three refinement loops: syntax repair guided by tool diagnostics, CEX-guided correction using trace links, and coverage-directed property augmentation. Evaluation across seven benchmark designs indicates that KG-based context retrieval improves specification-to-RTL grounding and consistently produces compilable SVAs with low syntax-repair overhead. The approach achieves formal coverage ranging from 78.5% to 99.4%, though convergence exhibits design dependence with complex temporal and arithmetic reasoning remaining challenging for current LLM capabilities.
Existing Large Language Model (LLM) approaches to SystemVerilog Assertion (SVA) generation primarily focus on syntactic validity and formal verification outcomes, while semantic alignment between generated assertions and natural language specifications remains difficult to quantify. As a result, hallucinated or misaligned SVAs can reduce confidence and increase debugging efforts in the absence of golden RTL. This paper presents SpecAlign, a framework for semantic evaluation and refinement of LLM-generated SVAs. SpecAlign introduces two iterative alignment loops that assess both natural language properties and SVAs against the design specification using entailment-based classification. We improve alignment decisions by generating multiple reasoning paths using chain-of-thought prompting and aggregating them via a self-consistency voting mechanism. Misaligned assertions are analyzed to generate actionable feedback for refinement. We further define a quantitative alignment score to measure semantic consistency across iterations. Experimental results demonstrate that SpecAlign effectively detects semantic inconsistencies and improves assertion alignment without relying on golden RTL, providing a scalable complement to traditional formal verification evaluation metrics.
Jaime Rafael Imperial, Hao Zheng
Bellini College of Cybersecurity, AI, and Computing University of South Florida Tampa, USA