Certifying Constraints in Hardware Model Checking

Lecture notes in computer science, pp. 170–188

Abstract

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.

Authors 4

1. Nils Froleyks corresponding

   KU Leuven

   Affiliation as printed

   KU Leuven, Leuven, Belgium

2. Emily Yu Aachen

   Leiden University

   Affiliation as printed

   Leiden University, Leiden, Netherlands

3. Armin Biere

   University of Freiburg

   Affiliation as printed

   University of Freiburg, Freiburg, Germany

4. Keijo Heljanko

   University of Helsinki · Helsinki Institute for Information Technology

   Affiliation as printed

   Helsinki Institute for Information Technology, Helsinki, Finland

   University of Helsinki, Helsinki, Finland