INSIGHT: Automatic Generation of Explanations for Efficient Identification of Hardware Bugs and Underspecifications

Hardware verification is a critical task in processor development. Functional correctness bugs that escape verification can manifest as serious security vulnerabilities, allowing attackers to violate control and dataflow integrity. A common verification strategy to eliminate functional correctness bugs during design time is to compare the architectural behavior of a device under test, i.e., the hardware implementation, against a golden reference implementation, using model checking or fuzzing to expose mismatches. In practice, a single bug often manifests in many mismatch-triggering programs. Moreover, due to ISA underspecification, not every mismatch corresponds to a bug. Without additional guidance, model checkers repeatedly rediscover programs that trigger the same bug or ISA underspecification, while fuzzers generate large numbers of triggering programs that stem from the same underlying cause, causing substantial manual overhead. This paper presents INSIGHT, a framework that automatically synthesizes generalized, machine-readable explanations of mismatches between a processor implementation and its reference model. INSIGHT (i) guides model checkers towards exposing distinct bugs and underspecifications and (ii) clusters large program corpora by shared explanations, enabling automatic deduplication. INSIGHT translates explanation synthesis into a combinatorial optimization problem and solves it efficiently using Integer Linear Programming solvers. We implement and evaluate INSIGHT on an in-order core and the out-of-order BOOM RISC-V core. We show that with INSIGHT, model checkers can discover more distinct bugs in the same timeframe. INSIGHT can also reduce a large corpus of fuzzing testcases into a small number of clusters.