一句话：提出 H-Houdini，用可并行、可记忆化的分层增量 SMT 检查替代整体式检查，使归纳不变式学习扩展到大型硬件设计。
形式验证在硬件设计中至关重要，但现有技术在自动化与效率上的进展仍难以扩展到大规模设计。本文提出 H-Houdini：一种（基本）一键式的归纳不变式学习算法，融合了机器学习启发的综合（MLIS）与基于 SAT 的增量学习。其关键创新在于把 MLIS 中整体式的 SMT 检查替换为一套精心构造的、更小的增量 SMT 检查层次结构，这些检查可以并行化、记忆化，并以构造即正确（correct-by-construction）的方式重新组装为原初的“整体”不变式。作者将其实现为 VeloCT 框架，通过学习关系型不变式来证明硬件安全属性，并在微体系结构安全中的“安全指令集综合”问题上进行评测。VeloCT 无需专家标注即可在 10 秒内为 RISC-V Rocketchip 学到不变式，比当前最优方法快 2880 倍；它还是首个扩展到 RISC-V 乱序核 BOOM 的工作，能在 6.95 至 199.1 分钟内（基本自动地）验证从 Small 到 Mega 的全部 BOOM 变体。
Formal verification is a critical task in hardware design today. Yet, while there has been significant progress in improving technique automation and efficiency, scaling to large hardware designs remains a significant challenge. We address this challenge by proposing H-HOUDINI: a new algorithm for (mostly) push-button inductive invariant learning that scales to large hardware designs. H-HOUDINI combines the strengths of Machine Learning Inspired Synthesis (MLIS) and SAT-based Incremental Learning. The key advance is a method that replaces the monolithic SMT-style checks made by MLIS with a carefully-constructed hierarchy of smaller, incremental SMT checks that can be parallelized, memoized and reassembled into the original 'monolithic' invariant in a correct-by-construction fashion. We instantiate H-HOUDINI as VeloCT, a framework that proves hardware security properties by learning relational invariants. We benchmark VeloCT on the 'safe instruction set synthesis' problem in microarchitectural security. Here, VeloCT automatically (with no expert annotations) learns an invariant for the RISC-V Rocketchip in under 10s (2880x faster than state of the art). Further, VeloCT is the first work to scale to the RISC-V out-of-order BOOM and can (mostly-automatically) verify all BOOM variants (ranging from Small to Mega) in between 6.95 minutes to 199.1 minutes.