Search papers, labs, and topics across Lattice.
The paper introduces enhancements to Saarthi, an agentic AI framework for end-to-end formal verification, to improve its robustness and reliability. They address the limitations of LLM-based agents in complex tasks by incorporating a structured rulebook and specification grammar for SVA generation, and integrating advanced RAG techniques like GraphRAG for accessing technical knowledge. Benchmarking on NVIDIA's CVDP benchmark shows a 70% improvement in assertion accuracy and a 50% reduction in iterations for coverage closure.
Saarthi's new rulebook and GraphRAG integration boost formal verification accuracy by 70% and cut iteration counts in half, hinting at a path to domain-specific AGI.
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.
