FVEval: Understanding Language Model Capabilities in Formal Verification of Digital Hardware
This work addresses the lack of holistic evaluation for LLMs in formal verification of digital hardware, which is crucial for automating tasks that currently demand significant human effort in chip design.
The authors tackled the problem of evaluating large language models (LLMs) for formal verification (FV) in digital hardware design by creating FVEval, a comprehensive benchmark with three sub-tasks measuring capabilities from generating SystemVerilog assertions to reasoning about design RTL. They evaluated a wide range of LLMs, providing insights into current performance and potential for improving productivity in FV workflows.
The remarkable reasoning and code generation capabilities of large language models (LLMs) have spurred significant interest in applying LLMs to enable task automation in digital chip design. In particular, recent work has investigated early ideas of applying these models to formal verification (FV), an approach to verifying hardware implementations that can provide strong guarantees of confidence but demands significant amounts of human effort. While the value of LLM-driven automation is evident, our understanding of model performance, however, has been hindered by the lack of holistic evaluation. In response, we present FVEval, the first comprehensive benchmark and evaluation framework for characterizing LLM performance in tasks pertaining to FV. The benchmark consists of three sub-tasks that measure LLM capabilities at different levels: from the generation of SystemVerilog assertions (SVAs) given natural language descriptions to reasoning about the design RTL and suggesting assertions directly without additional human input. As test instances, we present both collections of expert-written verification collateral and methodologies to scalably generate synthetic examples aligned with industrial FV workflows. A wide range of existing LLMs, both proprietary and open-source, are evaluated against FVEval, based on which we investigate where today's LLMs stand and how we might further enable their application toward improving productivity in digital FV. Our benchmark and evaluation code is available at \url{https://github.com/NVlabs/FVEval}.