REVIEW 9 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
Using LLMs to Facilitate Formal Verification of RTL
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 9 Pith papers
-
From Language to Logic: Bridging LLMs & Formal Representations for RTL Assertion Generation
ProofLoop achieves 93.7% syntax correctness and 82.0% functional correctness for SVA generation from natural language by combining retrieval, EDA tools, and up to three rounds of JasperGold formal feedback.
-
ChatSVA: Bridging SVA Generation for Hardware Verification via Task-Specific LLMs
ChatSVA achieves 96.12% functional pass rate and 82.5% coverage in SVA generation on 24 RTL designs, delivering 33 percentage point gains and 11x better coverage than prior state-of-the-art.
-
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.
-
CoverAssert: Iterative LLM Assertion Generation Driven by Functional Coverage via Syntax-Semantic Representations
CoverAssert iteratively improves LLM-generated assertions via syntax-semantic clustering and coverage feedback, yielding 9.57% branch, 9.64% statement, and 15.69% toggle coverage gains on four open-source designs when...
-
Large Lemma Miners: Can LLMs do Induction Proofs for Hardware?
A neurosymbolic method using two LLM prompting frameworks generates provably correct inductive arguments for 84% of a set of mid-size open-source RTL hardware designs.
-
Automated SVA Generation with LLMs
SVA Generator improves semantic correctness of LLM-generated SystemVerilog Assertions by 22.7 percentage points on average for deeper properties using AST-grounded constraint injection and depth-stratified formal equi...
-
Can LLMs Make (Personalized) Access Control Decisions?
LLMs reflect users' privacy preferences in access control decisions with up to 86% agreement and can promote safer behavior, but personalization trades off higher individual match for potentially less secure results w...
-
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.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.