Abstract

To mitigate the burden of writing SystemVerilog Assertions (SVA) for Formal Property Verification (FPV), this study explores using LLMs like GPT-4 to automatically generate verification properties directly from RTL code. Researchers designed an iterative FPV evaluation framework and successfully crafted prompting rules to enable GPT-4 to generate correct safety properties, even for flawed designs. Crucially, this LLM-facilitated approach proved effective by uncovering a bug previously missed in the complex open-source RISC-V CVA6 processor core.

Report

Structured Report: Using LLMs to Facilitate Formal Verification of RTL

Key Highlights

• Automated Formal Verification: The core innovation is leveraging Large Language Models (LLMs), specifically GPT-4, to automatically generate robust SystemVerilog Assertions (SVA) properties based on Register-Transfer Level (RTL) code.
• Bug Discovery: The LLM-generated SVA successfully exposed a previously undetected bug within the verification of the widely used open-source RISC-V CVA6 core.
• Framework Development: An FPV-based evaluation framework was created to rigorously measure the correctness and completeness of the LLM-generated SVA.
• Rule Crafting: The study identifies a refined set of syntax and semantic rules necessary to prompt GPT-4 effectively toward creating high-quality SVA.
• Open-Source Integration: The improved GPT-4 flow was integrated into and extended the open-source AutoSVA framework, adding new capability for safety properties.

Technical Details

• Model Used: GPT-4 was the primary LLM evaluated and utilized for property generation.
• Target Output: SystemVerilog Assertions (SVA), which define properties for Formal Property Verification (FPV).
• Methodology: The approach involves an iterative, evaluation-driven process to refine prompt engineering, teaching the LLM how to reliably capture hardware behavior and generate error-free SVA.
• Integration Details: The LLM flow was integrated into AutoSVA to generate safety properties, supplementing the existing framework's ability to generate liveness properties.
• Validation: Use cases included measuring the FPV coverage achieved by GPT4-generated SVA on complex RTL, and demonstrating the concept of using generated SVA to prompt GPT4 to create RTL from scratch.

Implications

• Democratization of FPV: Formal verification, traditionally resource-intensive and requiring highly specialized expertise, becomes more accessible and efficient. LLMs significantly reduce the manual effort of writing complex SVA, lowering the barrier to entry for robust verification.
• Enhancing RISC-V Reliability: The success in finding a hidden bug in the complex, open-source CVA6 core validates the method's effectiveness on real-world designs. This capability is crucial for scaling the RISC-V ecosystem, ensuring that community and commercial cores achieve commercial-grade verification quality.
• Future EDA Tooling: This research establishes a strong use case for integrating LLMs directly into Electronic Design Automation (EDA) tools, promising faster design cycles and intrinsically higher-quality hardware by automating critical verification steps.
• Trustworthiness of LLM Verification: The finding that GPT-4 can generate correct SVA even when analyzing flawed RTL (without mirroring the design errors) suggests that LLM verification tools can act as objective and trustworthy auditors of hardware functionality.