发表机构
University of Virginia（弗吉尼亚大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
针对硬件信息流验证扩展性差的问题，提出SLED-IFV，利用LLM生成经求解器验证的分解，通过功能简化和关系强化，实现高达603倍加速并解决超时问题。
AI 中文摘要
形式化硬件信息流验证（IFV）为对抗依赖秘密的时序和控制行为提供了强有力的保证，但在实际RTL上往往扩展性不佳。我们在自组合IFV中识别出两个反复出现的证明障碍：实现复杂性，即尽管属性仅需要紧凑的边界关系，但难以证明的数据路径逻辑占主导地位；以及关系归纳复杂性，即证明依赖于后端证明器无法高效推断的跨副本公共控制事实。为解决这些问题，我们引入了两种语义证明分解形式：功能简化，用经过验证的过近似摘要替换难以证明的RTL区域；以及关系强化，暴露并证明归纳所需的跨副本关系。我们进一步提出了SLED-IFV，一种求解器验证的LLM引导流程，自动化选择这些形式及其具体目标。给定自组合miter和无预言机决策表，LLM提出分解方案，然后在控制器检查下将其物化为证明工件。控制器将检查过的工件编译为证明义务，形式化验证后端仍是接受的唯一权威。在从真实RTL构建的九个非平凡基准测试中，SLED-IFV实现了高达603倍的仅求解器加速，并将两个12小时超时转换为完成的证明。闭环流程为所有案例生成了验证器接受的分解。
英文摘要
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.
CommentsAccepted at the 32nd Asia and South Pacific Design Automation Conference (ASP-DAC 2027). 7 pages, 3 figures, and 5 tables
