Saarthi: The First AI Formal Verification Engineer

TL;DR

Saarthi is an autonomous AI tool designed for end-to-end formal verification of RTL designs, leveraging agentic workflows to enhance scalability and efficiency across multiple verification domains.

Contribution

It introduces Saarthi, the first fully autonomous AI formal verification engineer utilizing agentic workflows for scalable, domain-agnostic RTL verification.

Findings

Saarthi successfully verifies RTL designs end-to-end autonomously.

The system is adaptable across various verification domains.

It enables verification teams to focus on complex problems.

Abstract

Recently, Devin has made a significant buzz in the Artificial Intelligence (AI) community as the world's first fully autonomous AI software engineer, capable of independently developing software code. Devin uses the concept of agentic workflow in Generative AI (GenAI), which empowers AI agents to engage in a more dynamic, iterative, and self-reflective process. In this paper, we present a similar fully autonomous AI formal verification engineer, Saarthi, capable of verifying a given RTL design end-to-end using an agentic workflow. With Saarthi, verification engineers can focus on more complex problems, and verification teams can strive for more ambitious goals. The domain-agnostic implementation of Saarthi makes it scalable for use across various domains such as RTL design, UVM-based verification, and others.