Saarthi for AGI: Towards Domain-Specific General Intelligence for Formal Verification

TL;DR

This paper introduces enhancements to the Saarthi AI framework, combining structured rule-based methods and advanced retrieval techniques to improve formal verification accuracy and efficiency, marking progress toward domain-specific general intelligence.

Contribution

The paper presents two key improvements to Saarthi: a structured rulebook for better assertion generation and integration of GraphRAG for knowledge access, advancing formal verification automation.

Findings

70% improvement in assertion accuracy

50% reduction in iterations for coverage closure

Enhanced robustness in formal verification tasks

Abstract

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.