REVIEW 7 cited by
Using LLMs to Facilitate Formal Verification of RTL
Not yet reviewed by Pith; the record is open.
This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.
SPECIMEN: schema-true, not a live event
T0 review · schema-true
One-sentence machine reading of the paper's core claim.
pith:XXXXXXXX · record.json · timestamp
read the original abstract
Formal property verification (FPV) has existed for decades and has been shown to be effective at finding intricate RTL bugs. However, formal properties, such as those written as SystemVerilog Assertions (SVA), are time-consuming and error-prone to write, even for experienced users. Prior work has attempted to lighten this burden by raising the abstraction level so that SVA is generated from high-level specifications. However, this does not eliminate the manual effort of reasoning and writing about the detailed hardware behavior. Motivated by the increased need for FPV in the era of heterogeneous hardware and the advances in large language models (LLMs), we set out to explore whether LLMs can capture RTL behavior and generate correct SVA properties. First, we design an FPV-based evaluation framework that measures the correctness and completeness of SVA. Then, we evaluate GPT4 iteratively to craft the set of syntax and semantic rules needed to prompt it toward creating better SVA. We extend the open-source AutoSVA framework by integrating our improved GPT4-based flow to generate safety properties, in addition to facilitating their existing flow for liveness properties. Lastly, our use cases evaluate (1) the FPV coverage of GPT4-generated SVA on complex open-source RTL and (2) using generated SVA to prompt GPT4 to create RTL from scratch. Through these experiments, we find that GPT4 can generate correct SVA even for flawed RTL, without mirroring design errors. Particularly, it generated SVA that exposed a bug in the RISC-V CVA6 core that eluded the prior work's evaluation.
Forward citations
Cited by 7 Pith papers
-
GoGoTB: Agentic RTL Verification with Specification-Grounded Coverage Closure
An agentic LLM framework reports 100% verification-environment generation success and ~83% functional coverage on eight RTL designs by tying every coverage bin to a named specification behavior.
-
Large Lemma Miners: Can LLMs do Induction Proofs for Hardware?
LLMs, verified by a symbolic model checker, produced correct inductive strengthenings for 82 of 94 curated RTL safety properties.
-
SVAgent: AI Agent for Hardware Security Verification Assertion
SVAgent is a prompt-engineering framework that decomposes security requirements into sub-questions to generate SystemVerilog assertions with higher reported accuracy and consistency than direct LLM generation.
-
AnalogTester: A Large Language Model-Based Framework for Automatic Testbench Generation in Analog Circuit Design
An LLM multi-agent framework automatically generates TED testbenches for op-amps, bandgap references, and low-dropout regulators from research papers, with reported task success rates above 80 percent.
-
LLM Assisted Verification Assertion Generation: Challenges and Future Directions
A review of LLM-based SystemVerilog Assertion generation frameworks, identifying challenges in specification processing, signal mapping, vacuity, and evaluation, with guidelines for future research.
-
The 4/$\delta$ Bound: Designing Predictable LLM-Verifier Systems for Formal Method Guarantee
The 4/δ bound is the mean of four geometric distributions, not a new theorem, and the simulation validation is circular.
-
Large Language Models (LLMs) for Electronic Design Automation (EDA)
A review of LLM applications in EDA, summarizing prior work and three case studies on hardware design, testing, and optimization.
Discussion (0). Continue with ORCID to comment.