Reproduce “FVEval: Understanding Language Model Capabilities in Formal Verification of Digital Hardware” on OpenResearch
Turn your favorite coding agents into research agents that review literature, develop hypotheses, and run experiments.
Universal app for Apple silicon and Intel. Requires macOS 11 or later.
About this paper
Minwoo Kang, Mingjie Liu, Ghaith Bany Hamad, Syed Suhaib, Haoxing Ren
FVEval introduces the first comprehensive benchmark for evaluating large language models (LLMs) in hardware formal verification, assessing their capabilities in generating SystemVerilog Assertions (SVAs) from natural language and directly from Register-Transfer Level (RTL) code. The framework utilizes industry-standard formal verification tools to provide objective metrics on syntax and functional correctness across various LLMs.
Key insights
- LLMs consistently demonstrate high syntax correctness in SVA generation, but a significant gap (often >30%) exists between syntax and functional correctness, particularly in translating complex temporal logic.
- Multi-sample generation (pass@k) substantially improves functional correctness, showing that LLMs can effectively serve as 'drafting' tools for engineers by providing a selection of plausible assertions.
- LLMs exhibit a nascent ability to understand hardware semantics and generate provable formal properties directly from RTL code, especially for finite-state machines.
Summary by alphaXiv.
Tip: change arxiv.org to autoarxiv.org in any arXiv abstract link to open the paper here.