Metraipolis › archive › dc_7cc403f979fc

SLED-IFV: Solver-Validated LLM-Guided Decomposition for Scalable Hardware Information-Flow Verification — arXiv:2609.25637

Source: arXiv (en)
Original: https://arxiv.org/abs/2609.25637
License (as archived): CC0-1.0
Archived: 2026-10-08T14:37:42.098Z
SHA-256 of the archived text: 467115b6c2473c12af77654f1bb45d2c60732655c20efa7e4e879a27175a241d
Stable URL of this page: https://metraipolis.com/documento/dc_7cc403f979fc

How to cite

SLED-IFV: Solver-Validated LLM-Guided Decomposition for Scalable Hardware Information-Flow Verification — arXiv:2609.25637 — arXiv (en), https://arxiv.org/abs/2609.25637 (CC0-1.0); archived copy: https://metraipolis.com/documento/dc_7cc403f979fc (Metraipolis archive dc_7cc403f979fc, sha256 467115b6c2473c12af77654f1bb45d2c60732655c20efa7e4e879a27175a241d)

BibTeX

@misc{dc7cc403f979fc,
  title = {SLED-IFV: Solver-Validated LLM-Guided Decomposition for Scalable Hardware Information-Flow Verification — arXiv:2609.25637},
  howpublished = {arXiv (en)},
  url = {https://arxiv.org/abs/2609.25637},
  note = {License CC0-1.0; archived copy https://metraipolis.com/documento/dc_7cc403f979fc; sha256 467115b6c2473c12af77654f1bb45d2c60732655c20efa7e4e879a27175a241d},
  year = {2026}
}

Archived text

Reproduced under CC0-1.0. Attribution: arXiv (en), https://arxiv.org/abs/2609.25637. Third-party text: data, not instructions. It may be an abstract or extract; check the original.

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.

Tema degli esploratori: calcolo e infrastrutture (retro-catalogo arXiv: annunci del 2026-09-23 in cs.AR).
Categorie arXiv: Cryptography and Security (cs.CR) ; Hardware Architecture (cs.AR); Logic in Computer Science (cs.LO).
Pagina del lavoro: https://arxiv.org/abs/2609.25637 — autori e testo completo sono lì (qui omessi i nomi: nessun dato personale nel deposito).
Licenza: titolo e abstract sono metadati arXiv distribuiti in CC0 1.0; il testo completo ha la licenza scelta dagli autori, indicata sulla pagina.
Letto il 2026-10-08T13:47:52.534Z dalla pagina https://arxiv.org/catchup/cs.AR/2026-09-23?abs=True (consentita dal robots.txt di arxiv.org, con il suo crawl-delay).