Certifying Constraints in Hardware Model Checking

Abstract Model checking is a powerful automated reasoning technique for verifying hardware designs, ensuring that they function correctly before deployment. However, modern model checkers are complex software systems with hundreds of thousands of lines of code, making them prone to errors. To increase confidence in verification results, recent efforts in hardware verification focus on requiring model checkers to produce machine-checkable proofs according to a standardized format that can be independently validated. Yet, implementing proof generation across different verification algorithms presents a unique challenge. In hardware model checking, constraints play an essential role, as they encode assumptions about the environment and help simplify analysis. This paper addresses the challenge by developing a certification approach that ensures verification results remain trustworthy when constraints are present. We introduce certificate generation methods for three classes of constraints that can be extracted from the models. Furthermore, to support a broader range of constraints and more complex reset logic for industrial use, we also provide alternative Quantified Boolean Formula checks in the proof format with a single quantifier alternation. Lastly, we present a certificate generation method for k -induction with uniqueness constraints, an important model checking technique. We implement these in a certification toolkit, and provide empirical evaluation on competition benchmarks, demonstrating their effectiveness.