Showing cs.CRShow all
2 papers · 1 filter
cs.CR2026
SLED-IFV: Solver-Validated LLM-Guided Decomposition for Scalable Hardware Information-Flow Verification
Liangtao Dai, Yimin Gao, Melika Morsali +1
Formal hardware information-flow verification (IFV) provides strong guarantees against secret-dependent timing and control behavior, but often scales poorly on realistic RTL. We id…
cs.CR2026
Guarded Equivalence Predicates for Scalable Formal Hardware Information-Flow Verification
Liangtao Dai, Yimin Gao, Melika Morsali +1
Formal hardware information-flow verification is a principled way to rule out secret-dependent functional or timing observations, but scaling such proofs remains difficult. Self-co…