SLED-IFV: Solver-Validated LLM-Guided Decomposition for Scalable Hardware Information-Flow Verification
SLED-IFV uses solver-checked LLM decompositions to speed hardware information-flow proofs by up to 603x.
Researchers present SLED-IFV, a closed-loop flow in which an LLM proposes semantic decompositions for self-composed hardware information-flow proofs while a formal backend remains the sole acceptance authority. Functional simplification replaces proof-hard RTL with a validated over-approximate summary, and relational strengthening exposes cross-copy public-control facts needed for induction. On nine benchmarks built from real RTL, it reached up to 603x solver-only speedup and completed two proofs that had timed out after 12 hours.
- LLM proposes decompositions; only the formal verifier accepts proofs.
- Functional simplification replaces hard RTL regions with validated summaries.
- Relational strengthening exposes cross-copy facts needed for induction.
- Up to 603x speedup; two 12-hour timeouts became completed proofs.
Full article197 words · extracted from arxiv.org · click to collapse
Formal hardware information-flow verification (IFV) provides strong guarantees against secret-dependent timing and control behavior, but often scales poorly on realistic RTL. We identify two recurring proof barriers in self-composed IFV: implementation complexity, where proof-hard datapath logic dominates even though the property needs only a compact boundary relation, and relational inductive complexity, where the proof depends on cross-copy public-control facts that the backend prover does not infer efficiently. To address them, we introduce two semantic proof decomposition forms: functional simplification, which replaces a proof-hard RTL region with a validated over-approximate summary, and relational strengthening, which exposes and proves the cross-copy relations needed for induction. We further present SLED-IFV, a solver-validated LLM-guided flow that automates the selection of these forms and their concrete targets. Given a self-composed miter and an oracle-free decision sheet, the LLM proposes a decomposition, then materializes it into proof artifacts under controller checks. The controller compiles the checked artifacts into proof obligations, and the formal verification backend remains the sole authority for acceptance. Across nine nontrivial benchmarks constructed from real RTL, SLED-IFV achieves up to 603x solver-only speedup and converts two 12-hour timeouts into completed proofs. The closed-loop flow produces verifier-accepted decompositions for all cases.
Text extracted automatically; images, tables and formatting may be missing. Original: https://arxiv.org/abs/2609.25637