Generative AI Augmented Induction-based Formal Verification

TL;DR

This work addresses the labor-intensive nature of induction-based formal verification in hardware designs by introducing a GenAI-enabled workflow that auto-generates lemmas and helper assertions to support $k$-induction proofs. It demonstrates two flows: general lemma generation from specification and RTL, and inductive-step failure analysis using CEX to produce corrective assertions. The results, using counters and ECC designs, indicate that large LLMs (e.g., GPT-4 variants) provide higher-quality, faster proofs, though an OpenAI-model advantage highlights data-driven performance. The study emphasizes the potential of GenAI to speed up formal verification while underscoring the need for human-in-the-loop validation to mitigate hallucinations.

Abstract

Generative Artificial Intelligence (GenAI) has demonstrated its capabilities in the present world that reduce human effort significantly. It utilizes deep learning techniques to create original and realistic content in terms of text, images, code, music, and video. Researchers have also shown the capabilities of modern Large Language Models (LLMs) used by GenAI models that can be used to aid hardware development. Formal verification is a mathematical-based proof method used to exhaustively verify the correctness of a design. In this paper, we demonstrate how GenAI can be used in induction-based formal verification to increase the verification throughput.

Figures (3)

• Figure 1: Helper assertion generation using LLM
• Figure 2: Helper assertion generation for induction step failure using LLM
• Figure 3: Induction step failure (31st bit of count2 is not logic 1)