H-Houdini: Scalable Invariant Learning
Sushant Dinesh, Yongye Zhu, Christopher W. Fletcher
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.