QiMeng-CodeV-SVA: Training Specialized LLMs for Hardware Assertion Generation via RTL-Grounded Bidirectional Data Synthesis
Authors: Yutong Wu, Chenrui Cao, Pengwei Jin, Di Huang, Rui Zhang, Xishan Zhang, Zidong Du, Qi Guo, +1 more
Organizations: SKL of Processors, Institute of Computing Technology, CAS Beijing, China · University of Chinese Academy of Sciences Beijing, China · University of Science and Technology of China Hefei, Anhui, China · Cambricon Technologies Beijing, China
SystemVerilog Assertions (SVAs) are crucial for hardware verification. Recent studies leverage general-purpose LLMs to translate natural language properties to SVAs (NL2SVA), but they perform poorly due to limited data. We propose a data synthesis framework to tackle two challenges: the scarcity of high-quality real-world SVA corpora and the lack of reliable methods to determine NL-SVA semantic equivalence. For the former, large-scale open-source RTLs are used to guide LLMs to generate real-world SVAs; for the latter, bidirectional translation serves as a data selection method. With the synthesized data, we train CodeV-SVA, a series of SVA generation models. Notably, CodeV-SVA-14B achieves 75.8% on NL2SVA-Human and 84.0% on NL2SVA-Machine in Func.@1, matching or exceeding advanced LLMs like GPT-5 and DeepSeek-R1.
Figures & tables
Figure 1. The relationship between data size and average 3-gram TF-IDF distance of different SVA sources.
Figure 2. An example of bidirectional data selection.
Figure 3. The overview of our data synthesis and training framework.
Figure 4. Concise prompts and examples of NL verification property analysis (Sec. 3.1 ) and SVA2NL (Sec. 3.2 ).
Method
NL2SVA-Human
NL2SVA-Machine
Func.@1
Func.@16
Func.@1
Func.@16
w/o Tutorial
74.6
90.3
81.0
93.3
w/ Tutorial
71.5
90.0
83.7
93.7
Table 1. The performance (%) of DeepSeek-R1 with and without tutorial prompts. See Sec. 4.2 for details of benchmarks.
Model
NL2SVA-Human
NL2SVA-Machine
F@1
F@16
F@32
F@1
F@16
F@32
( Advanced General-Purpose Models )
DeepSeek-R1-671B
74.6
90.3
90.4
81.0
93.3
94.3
GPT-5
71.8
90.2
92.7
81.8
93.2
94.3
DeepSeek-V3.1-671B
63.1
81.4
84.9
83.8
92.9
93.6
GPT-4o
64.1
75.2
78.1
68.5
81.3
83.7
Table 2. The evaluation results (%) of CodeV-SVA and other LLMs. “F@ k ” refers to Func.@ k score (Section 4.2 ).
SVA Source
Data
NL2SVA-Human
NL2SVA-Machine
Size
F@1
F@16
F@32
F@1
F@16
F@32
Synthesized (ours)
5K
55.4
84.0
86.3
75.7
94.0
95.1
DeepCircuitX
5K
22.3
59.0
64.4
39.2
58.8
61.1
VERT
20K
1.9
8.8
11.0
6.4
16.0
19.1
Table 3. The performance (%) comparison between different SVA sources in training data. Synthesized: LLM-synthesized SVAs. DeepCircuitX: SVAs in open-source repositories. VERT: Rewriting open-source SVAs with manual rules.
Method
Data
NL2SVA-Human
NL2SVA-Machine
Size
F@1
F@16
F@32
F@1
F@16
F@32
CodeV-SVA (ours)
83K
72.0
88.8
90.4
83.5
96.3
97.2
( Ablation on data refinement )
w/o R
89K
63.9
80.0
82.2
81.1
91.2
92.2
w/o R, D
97K
62.2
80.4
82.2
81.1
91.6
92.6
w/o R, D, J
105K
63.5
80.1
82.2
77.2
91.5
92.6
Table 4. The performance (%) of removing each component in data refinement (Sec. 3.3 ) and selection (Sec. 3.2 and 3.1 ). R: Reasoning trajectories; D: Difficulty filtering; J: LLM-as-a-judge; B: Bidirectional data selection; V: Formal verification under RTL code.
Spec2NL
NL2SVA
#SVA
#SynC
#Proven
APB
GPT-4o
GPT-4o
436
377
106
CodeV-SVA-8B (ours)
442
384
180
DeepSeek-R1
DeepSeek-R1
515
281
122
CodeV-SVA-8B (ours)
529
466
211
ETHMAC
Table 5. Evaluation results of CodeV-SVA on AssertionForge.
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