Saarthi is an agentic AI framework that uses multi-agent collaboration to perform end-to-end formal verification. Even though the framework provides a complete flow from specification to coverage closure, with around 40% efficacy, there are several challenges that need to be addressed to make it more robust and reliable. Artificial General Intelligence (AGI) is still a distant goal, and current Large Language Model (LLM)-based agents are prone to hallucinations and making mistakes, especially when dealing with complex tasks such as formal verification. However, with the right enhancements and improvements, we believe that Saarthi can be a significant step towards achieving domain-specific general intelligence for formal verification. Especially for problems that require Short Term, Short Context (STSC) capabilities, such as formal verification, Saarthi can be a powerful tool to assist verification engineers in their work. In this paper, we present two key enhancements to the Saarthi framework: (1) a structured rulebook and specification grammar to improve the accuracy and controllability of SystemVerilog Assertion (SVA) generation, and (2) integration of advanced Retrieval Augmented Generation (RAG) techniques, such as GraphRAG, to provide agents with access to technical knowledge and best practices for iterative refinement and improvement of outputs. We also benchmark these enhancements for the overall Saarthi framework using challenging test cases from NVIDIA's CVDP benchmark targeting formal verification. Our benchmark results stand out with a 70% improvement in the accuracy of generated assertions, and a 50% reduction in the number of iterations required to achieve coverage closure.
Figures & tables
Fig. 1 : Overview of the basic RAG pipeline [ 27 ]
Fig. 2 : Knowledge graph construction and retrieval in GraphRAG pipeline [ 13 ]
Fig. 3 : Saarthi: Agentic AI based formal verification using multi-agent collaboration
Fig. 4 : Data Collection Flow during HIL
Fig. 5 : A snippet of the cached mistakes that all agents can learn from for future iterations
Fig. 6 : A comparison of the iterative SVA generation process before and after adding the rulebook
Fig. 7 : Overview of the comprehensive multi-agent RCA setup
Design
Metric
Pass@1
Pass@2
Pass@3
GPT-4.1
GPT-5
Llama3.3
GPT-4.1
GPT-5
Llama3.3
GPT-4.1
GPT-5
Llama3.3
ECC
# Assertions
19
28
14
25
32
6
25
48
12
1st generation
No
Yes
No
Yes
Yes
Yes
No
Yes
Yes
# attempts to fix
1
0
2
0
0
0
2
0
0
% Proven
71.86%
89.28%
57.14%
64.00%
75.00%
33.33%
64.00%
81.25%
50.00%
% Coverage
62.67%
58.57%
68.01%
60.21%
61.86%
2.18%
58.15%
93.74%
43.90%
TABLE I : Key Performance Indicators of Saarthi on designs of various complexity
Fig. 8 : Radar chart for Pass@1 for different designs
Fig. 9 : Radar chart for Pass@2 for different designs
Fig. 10 : Radar chart for Pass@3 for different designs
Design
Metric
Without HIL
With HIL
GPT-4.1
GPT-5
Llama3.3
GPT-4.1
GPT-5
Llama3.3
ECC
# Assertions
53
66
19
53
60
19
% Proven
84.90%
78.80%
68.42%
96.06%
80.00%
84.21%
% Coverage
89.31%
92.83%
90.63%
98.05%
95.22%
92.53%
Automotive IP
# Assertions
36
58
19
36
58
19
% Proven
50%
84.48%
26.31%
72.22%
93.10%
63.15%
TABLE II : Coverage improvement with and without HIL at Pass@1
Design
Metric
Coverage improvement without HIL
1 st Iter
2 nd Iter
3 rd Iter
4 th Iter
5 th Iter
ECC
# Assertions
312
318
1258
N/A
N/A
% Proven
91.67%
92.12%
97.93%
N/A
N/A
% Coverage
88.89%
86.86%
87.87%
N/A
N/A
Automotive IP
# Assertions
59
71
134
185
233
% Proven
81.35%
77.46%
85.82%
87.75%
89.69%
TABLE III : Coverage improvement without HIL across iterations (GPT-5)
Fig. 11 : % Proven comparison with and without HIL at Pass@1
Fig. 12 : Coverage comparison with and without HIL at Pass@1
Infineon Technologies India Private Limited, India · Dr. B R Ambedkar National Institute of Technology Jalandhar, India · Infineon Technologies Dresden AG & Co. KG, Germany
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