H-Houdini: Scalable Invariant Learning

Paper: H-HOUDINI: Scalable Invariant Learning
Reviewer: The Guardian (Adversarial Skeptic)

---

Summary

The authors present H-HOUDINI, a framework intended to scale inductive invariant learning by replacing monolithic SMT queries with a hierarchical, incremental approach based on relative inductivity. The core idea is to decompose the proof of a target property into a series of smaller proof obligations that correspond to the dataflow dependencies within the hardware design. The framework is instantiated as VELOCT to solve the Safe Instruction Set Synthesis Problem (SISP) for hardware security. The authors evaluate VELOCT on the RISC-V Rocketchip and, notably, on several variants of the out-of-order BOOM core, claiming significant performance improvements over prior monolithic approaches and the first successful automated invariant learning for a design of BOOM's complexity.

Strengths

1. The fundamental concept of decomposing a monolithic invariant proof into a hierarchy of smaller, relatively inductive proofs that mirror the circuit's cone-of-influence is a sound and compelling strategy for tackling the scalability bottleneck of SMT-based verification.
2. The successful application of the framework to the BOOM processor, a notoriously complex open-source out-of-order design, is a significant empirical result. Prior work has struggled to scale to this level, so demonstrating any automated analysis is a notable achievement.
3. The framework's design inherently supports a high degree of parallelism, which is a practical and necessary feature for analyzing large hardware designs.

Weaknesses

My primary concerns with this work center on the significant overstatement of its automation, the fragility of its formal arguments, and the heuristic nature of its core components, which call into question the generality and robustness of the approach.

1. The Claim of "Mostly Push-Button" Automation is Substantially Undermined by the Requirement for Expert Annotation. The paper claims the tool is "(mostly) push-button" (Abstract) and learns an invariant for Rocketchip with "no expert annotations" (Abstract). However, the success on the more complex and significant BOOM target is contingent on "modest expert annotations" (Section 6.2). This "modest" effort involves a graduate student manually identifying and annotating valid bits in multiple microarchitectural structures (ALU/CSR/FPU issue buffers, etc.) for "example masking" (Section 5.2.1) and manually adding predicates for micro-ops (InSafeUop) and ALU opcodes (Section 6.2). This is a critical, non-trivial manual intervention. The anecdotal measure of "less than a day" is not a rigorous metric of effort; for a different, more complex, or less well-documented design, this could be a multi-week reverse-engineering task requiring deep microarchitectural expertise. This manual effort effectively encodes a partial invariant into the system, guiding the "learning" process in a way that significantly weakens the central claim of automated invariant discovery.

2. The Soundness of the Entire Framework Relies on the Quality of Positive Examples. The soundness of the hierarchical decomposition, as presented in Section 3.1, hinges on the "Premise for Soundness (P-S)": each partial invariant H_i must be consistent with all positive examples. This premise is used to ensure the stepwise-proven H_i are not contradictory. However, this only guarantees non-contradiction with respect to the sampled examples, not the entire space of valid behaviors. If the positive examples are not sufficiently diverse, the algorithm could derive a set of locally consistent but globally contradictory partial invariants, leading to an unsound final invariant H that is vacuously true. The paper provides no formal argument or empirical evidence to suggest the example generation strategy is sufficient to prevent this.

3. The Predicate Mining and Abduction Oracles are Heuristic and Potentially Incomplete.

   • The predicate mining oracle O_mine (Algorithm 2, Section 5.1.2) generates candidate predicates based on properties that hold true across all provided positive examples (e.g., a register always being equal across two runs, or holding a constant value). This is a fragile heuristic. A single, valid but idiosyncratic positive example could prevent a necessary predicate from being mined, causing the entire proof to fail. The paper does not provide a formal argument for the completeness of this oracle—i.e., that it is guaranteed to generate the necessary predicates if an invariant exists within the language.
   • The abduction oracle O_abduct (Section 3.2.3) relies on extracting a minimal UNSAT core. The authors note that cvc5 "guarantees locally minimal unsat cores." This is a key weakness. The choice of UNSAT core can dramatically influence the subsequent search, and a "locally minimal" core is not guaranteed to be the simplest or most general explanation (abduct). The performance and even success of the algorithm may be highly sensitive to the SMT solver's non-deterministic core extraction heuristics, a dependency which is not explored.

4. The Evaluation is Incomplete, Weakening the Central Claims. In Section 6.4, the authors state they were "unable to verify the safety of the auipc instruction" on BOOM due to unexpected variable timing behavior. They subsequently "leave investigating why to future work." This is a critical admission. The work cannot claim to have solved the SISP for BOOM if it fails on a standard, non-privileged ISA instruction. This failure suggests a potential blind spot in the predicate language or the learning methodology when faced with certain microarchitectural timing patterns, which is a more fundamental issue than an incomplete run.

Questions to Address In Rebuttal

1. Please provide a more rigorous, quantitative characterization of the "expert annotation" effort required for BOOM. How many lines of annotation code were required? How many distinct hardware signals needed to be identified? How can the authors justify the "mostly automated" claim when this manual, expert-driven effort appears critical to success on the paper's main target?

2. The soundness of the approach (Section 3.1) relies on positive examples to ensure partial invariants are not contradictory. Please provide a more robust argument for why this is sufficient. How can you provide confidence that the generated examples are comprehensive enough to prevent the learning of a vacuous invariant that holds for the examples but not for all possible safe executions?

3. The failure to verify auipc on BOOM (Section 6.4) is a significant gap. Does this failure indicate a fundamental limitation in your predicate language or learning algorithm? Why should the committee be confident that this approach is generalizable if it fails on a standard instruction in its primary case study?

4. How sensitive is the H-HOUDINI algorithm, in terms of both performance and its ability to find an invariant, to the SMT solver's UNSAT core generation strategy? Given the reliance on "locally minimal" cores, what is the risk that the algorithm explores a suboptimal proof path or fails entirely due to the solver's heuristic choices?

Reviewer: The Synthesizer (Contextual Analyst)

Summary

This paper introduces H-HOUDINI, a novel and compelling algorithm for scalable inductive invariant learning. The core contribution is a powerful synthesis of two major paradigms in formal verification: the predicate abstraction and example-driven nature of Machine Learning Inspired Synthesis (MLIS) and the incremental, structure-aware nature of SAT-based methods like IC3/PDR. H-HOUDINI cleverly decomposes the expensive, monolithic SMT queries typical of MLIS into a hierarchy of smaller, localized, and highly parallelizable relative inductive checks. This decomposition is guided by the program or circuit's dataflow structure (specifically, the 1-step cone of influence), effectively creating a "white-box" MLIS framework.

The authors instantiate this algorithm in a tool called VELOCT to tackle the challenging Safe Instruction Set Synthesis Problem (SISP) in hardware security. The empirical results are exceptional: VELOCT learns an invariant for the RISC-V Rocketchip core over 2800x faster than the state-of-the-art and, most impressively, is the first tool to successfully learn invariants for the entire family of complex RISC-V BOOM out-of-order cores, a task previously considered intractable for this class of automated tools.

Strengths

1. A Powerful Conceptual Bridge: The most significant strength of this work is its elegant conceptual contribution. It identifies a fundamental tension between the scalability of SAT-based "white-box" incremental methods and the search-space pruning power of MLIS's "black-box" approach. The proposed solution—using the design's structure to guide a divide-and-conquer learning process—is a truly insightful hybrid. It feels less like a heuristic and more like a principled way to combine the best of both worlds. The connection made in the related work (Section 7, page 11) to RICE-learning (Relative ICE) correctly positions this as a foundational step forward for MLIS-based techniques.

2. Landmark Scalability Result: The paper doesn't just present a new idea; it demonstrates its power on a problem of recognized difficulty. Scaling automated invariant synthesis to an out-of-order processor like BOOM is a major achievement for the hardware verification community. Prior work often stops at simpler, in-order cores. By successfully analyzing a design with over 133K state bits (MegaBOOM), the authors have significantly pushed the boundary of what is considered possible, transforming the problem from "impossible" to "achievable in hours." This result alone makes the paper highly significant.

3. Excellent Problem Choice and Grounding: Applying H-HOUDINI to the SISP for constant-time verification is a perfect choice. It's not a toy problem but a critical challenge in hardware security, with direct implications for building trustworthy systems. This grounding in a practical, high-impact domain makes the work immediately relevant and compelling.

4. Clear and Effective Exposition: The core idea of hierarchical decomposition is explained very clearly, both conceptually with the AND gate example (page 2) and formally with Algorithm 1 (page 5). The worked example in Appendix C (pages 14-16) is particularly helpful for building intuition about how the recursive abduction, backtracking, and memoization fit together.

Weaknesses

While the core idea and results are outstanding, there are areas where the framework's current limitations and dependencies could be further explored. My perspective here is not to diminish the contribution but to contextualize its current instantiation and highlight avenues for future work.

1. Reliance on Manual Annotation and Oracles: The paper claims H-HOUDINI is a "(mostly) push-button" algorithm, but the successful application to BOOM required a "modest number of annotations" (Section 6.2, page 9). These include augmenting the predicate language (e.g., InSafeUop) and, critically, annotating valid bits for "example masking." While this is a practical and necessary step to achieve the result, it represents a knowledge-transfer bottleneck. The power of the general H-HOUDINI framework is somewhat tied to the quality of the domain-specific Omine oracle and these annotations.

2. Demonstrated Generality: The work is masterfully demonstrated on a 2-safety (non-interference) property. This relational structure is a natural fit for the product-construction methodology used. It is less clear how the H-HOUDINI framework would apply to other important verification tasks, such as verifying functional correctness properties or liveness properties. The core hierarchical idea seems general, but its instantiation would require fundamentally different predicate languages and oracle implementations, the challenges of which are not fully explored.

3. Sensitivity to Positive Examples: The performance and correctness hinge on the quality of the positive examples used to prune the predicate space and avoid backtracking. The paper notes that backtracking occurs due to non-exhaustive examples (Section 6.3, page 10, Figure 5). While the strategy of simulating instructions seems effective, the framework's robustness in the face of a poor or incomplete set of examples is an important practical question. A few "bad" examples could potentially prune necessary predicates, leading to failure.

Questions to Address In Rebuttal

1. The Path to Full Automation: The expert annotations required for BOOM were key to success. Could the authors comment on the prospects for automating this "expert-in-the-loop" step? For instance, could static analysis of the RTL or a preliminary data-flow analysis automatically identify structures like instruction queues and their corresponding "valid" bits to guide example masking? How much of this domain knowledge could be formalized and integrated into the Omine oracle?

2. Beyond 2-Safety: The paper's conclusion rightly points to exploring other properties as future work. Could the authors elaborate on the conceptual challenges of applying H-HOUDINI to a standard functional correctness property (e.g., proving that a pipelined processor correctly implements the ISA specification)? What would the Ptarget, the predicate language, and the "positive examples" look like in that context?

3. Robustness of Example-Driven Learning: The backtracking analysis in Figure 5 is insightful. Could you provide more intuition on the failure modes? When H-HOUDINI fails to find an invariant (or backtracks excessively), is it typically due to a missing predicate in the language, insufficient positive examples missing a corner case, or fundamental scalability limits of the SMT solver on certain sub-problems? Understanding this could help guide future users.

Innovator Review Form

Isolate the Novel Claim:
The authors propose H-HOUDINI, an algorithm for scalable inductive invariant learning. The central novel claim is the synthesis of two distinct verification paradigms: the predicate-abstraction and example-guided search from Machine Learning Inspired Synthesis (MLIS), and the incremental, relatively inductive checks from white-box, SAT-based methods like IC3/PDR.

The precise mechanism claimed as novel is the replacement of the traditional monolithic inductivity check (H => H') with a hierarchical decomposition. This process involves:

1. Identifying a target predicate (P_target).
2. Using the 1-step cone-of-influence (COI) to find relevant predicates from a universe (P_V).
3. Synthesizing a "local" abduct A using a relative inductive query (A ^ P_target => P_target').
4. Recursively and parallelly solving for the inductivity of each predicate within the abduct A.

This creates a property-directed, recursive "wavefront" of smaller, parallelizable SMT checks that compose to prove the inductivity of the global invariant by construction, avoiding any single monolithic check.

Execute a "Prior Art" Search:
The foundational concepts leveraged in this work are well-established.

1. MLIS: The core MLIS algorithm, HOUDINI [28], is over two decades old. Its use of a predicate universe and filtering based on counterexamples is the baseline.
2. Incremental/Relative Inductive Learning: The idea of using relative induction to incrementally build invariants is the core of IC3/PDR [8, 22]. These methods, however, are typically driven by generalizing negative counterexamples, not by a predefined predicate abstraction guided by positive examples.
3. Abductive Inference for Invariants: The use of abduction and interpolants to infer strengthening predicates is also not new, with notable prior work by McMillan [39] on interpolants and Dillig et al. [18] on abductive inference for loop invariants.
4. Relative ICE (RICE) Learning: The most proximate prior art is the concept of RICE-learning proposed by Vizel et al. in "IC3-flipping the E in ICE" (VMCAI 2017) [48]. They explicitly proposed replacing the monolithic inductive query in the ICE-learning framework (a generalization of MLIS) with a relative inductive query.

Evaluate the Delta:
The core idea of "blending" MLIS with relative induction is therefore not fundamentally new; it was conceptualized as RICE-learning. The authors rightly acknowledge this in their Related Work section (Section 7, page 11).

However, the novelty of H-HOUDINI is not the concept, but the algorithm. Vizel et al. introduced the conceptual framework of a "RICE-learner" but did not provide a concrete, scalable, hierarchical algorithm for implementing it. H-HOUDINI is, to my knowledge, the first work to present such an algorithm. The "delta" over prior art is the specific, structured methodology for decomposing the problem:

• COI-Guided Decomposition: The explicit use of the 1-step COI to structure the recursive search is a novel and practical mechanism for applying the RICE concept to hardware verification.
• Hierarchical Abduction: While abduction for invariants exists, the structured, DFS-like recursive application of abduction to build up the invariant piece by piece is a new algorithmic pattern in this context.
• Scalability via Parallelism and Memoization: The algorithm is designed from the ground up for parallelism and memoization within its recursive structure. This is a significant engineering and algorithmic contribution that moves the RICE concept from theory to a highly practical tool.

In summary, H-HOUDINI does not invent a new category of learning but provides the first practical and scalable algorithmic blueprint for an existing, high-level idea.

Analyze the Complexity vs. Benefit Trade-off:
The proposed H-HOUDINI algorithm is significantly more complex than classic HOUDINI. It requires white-box access to the design, a COI slicer, multiple oracles, and management of a parallel, recursive search state with memoization.

However, the benefit overwhelmingly justifies this complexity. The results presented are not incremental; they are transformative for the problem domain.

• A 2880x speedup on Rocketchip (from 8 hours to <10 seconds) is a step-function improvement.
• The ability to verify BOOM variants—a task where the prior MLIS-based art (CONJUNCT) failed to scale at all—demonstrates that H-HOUDINI breaks a fundamental scalability barrier.

This is a clear case where a more complex, novel algorithmic structure unlocks a new level of capability. The marginal gains critique does not apply here; the gains are substantial and qualitative.

---

Review Form

Summary

This paper presents H-HOUDINI, a novel algorithm that significantly advances the state-of-the-art in automated invariant learning for hardware verification. The core contribution is a new method that synthesizes the strengths of MLIS (predicate abstraction, positive examples) and SAT-based incremental learning (relative induction). The algorithm replaces expensive, monolithic SMT queries with a hierarchical wavefront of smaller, independent, and parallelizable relative inductivity checks. This is achieved by recursively applying abductive reasoning guided by the cone-of-influence of target predicates. The authors instantiate H-HOUDINI as VELOCT and demonstrate its power by learning security invariants for the complex RISC-V BOOM out-of-order processor, a task that was intractable for prior MLIS-based techniques.

Strengths

1. Novel Algorithmic Synthesis: The primary strength is the concrete and scalable algorithm that successfully instantiates the high-level concept of a Relative ICE (RICE) learner. The hierarchical decomposition based on the design's COI is a principled and effective method for breaking down a monolithic verification problem.
2. Demonstrated Step-Function Scalability: The work does not present a minor improvement. By scaling to the BOOM processor family, it solves a problem that was out of reach for prior art in this domain. The 2880x speedup on Rocketchip further underscores the significance of the algorithmic advance.
3. Principled Design: The algorithm is sound by construction and its design choices (e.g., use of positive examples to prune search, memoization, parallelism) are well-justified and contribute directly to its performance.

Weaknesses

1. Positioning of Novelty: The paper's framing could more clearly distinguish its contribution from prior conceptual work. The core idea of using relative induction in an MLIS/ICE context was previously proposed by Vizel et al. [48]. While the authors correctly cite this in the related work, the introduction could be more precise by stating that H-HOUDINI's novelty lies in being the first scalable, hierarchical algorithm to realize this concept, rather than the invention of the concept itself.
2. Dependence on Oracles and Annotations: The practical instantiation, VELOCT, relies on several oracles and, for the complex BOOM core, a modest number of expert annotations (Section 6.2, page 9). While the core search algorithm is the main contribution, this reliance on domain-specific configuration slightly detracts from the novelty of a fully automated, "push-button" solution.

Questions to Address In Rebuttal

1. Could the authors more explicitly delineate the novel algorithmic contributions of H-HOUDINI beyond the initial RICE-learning concept proposed by Vizel et al. [48]? Specifically, is the primary contribution the COI-based decomposition, the recursive abduction strategy, or the parallel/memoized implementation of the search?
2. The hierarchical decomposition seems tightly coupled to the 1-step COI of a hardware transition system. How does the core H-HOUDINI algorithm generalize to other domains, such as software verification, where the notion of a static, 1-step dependency graph is less clear or may be much larger? Does the novelty hold if the slicing oracle is less precise?
3. The paper presents a specific SMT query for the abduction oracle O_abduct (Section 3.2.3, page 6) based on UNSAT cores. How critical is this specific formulation to the algorithm's success? Could it be replaced with other interpolation or abduction techniques without fundamentally changing the performance characteristics of the overall H-HOUDINI search?