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

arXiv:2609.25637 · cs.CR, cs.AR, cs.LO · Submitted 2026-09-22 · Read on arXiv

cs.CR, cs.AR, cs.LO

Submitted: 2026-09-22

Updated: 2026-09-22

Comments: Accepted at the 32nd Asia and South Pacific Design Automation Conference (ASP-DAC 2027). 7 pages, 3 figures, and 5 tables

Code: https://github.com/lowRISC/ibex

License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/

Terminology

• Verification — 30× in this paper · explained in 2 episodes
• Verifier — 16× in this paper · explained in 2 episodes
• Benchmark — 8× in this paper · explained in 2 episodes
• Alignment — 7× in this paper · explained in 1 episode
• Ablation — 6× in this paper · explained in 1 episode
• Consistency — 5× in this paper · explained in 3 episodes
• Abstraction — 4× in this paper · explained in 1 episode
• Formal Verification — 4× in this paper · explained in 2 episodes
• Core — 2× in this paper · explained in 2 episodes
• Trace — 2× in this paper · explained in 2 episodes
• Ablation Studies — 1× in this paper · explained in 1 episode
• Alignment Problem — 1× in this paper · explained in 1 episode
• Formal Methods — 1× in this paper · explained in 3 episodes
• Hybrid Approach — 1× in this paper · explained in 4 episodes
• IEEE Symposium on Security and Privacy — 1× in this paper

Sources

• Guarded Equivalence Predicates for Scalable Formal Hardware Information-Flow Verification
• LLM4DV: Using Large Language Models for Hardware Test Stimuli Generation

Related papers

• SoK: AI-Augmented Binary Reversing
• Relaxed Sender Anonymity for CBDC Interbank Settlement: A Zero-Knowledge Approach on Permissioned EVM
• Calibration-Family Overfit: Why Trusted Sabotage Monitors Don't Transfer Across Lineages
• Efficient Fuzzy PSI under One-Sided Assumptions
• Sealing the Audit-Runtime Gap for LLM Skills
• Token Composition: A Graph Based on EVM Logs