Hardware Model Checking Certification with Certifaiger and Cerbtora

Lecture notes in computer science, pp. 276–285

Abstract

Abstract Certificates are machine-checkable witnesses that help increase confidence in verification results by providing independently verifiable evidence beyond a simple yes/no answer. In this short paper, we present two certificate checkers for hardware model checking, Certifaiger and Cerbtora, which target bit-level and word-level verification of hardware designs, respectively. Certifaiger has been adopted in recent editions of the Hardware Model Checking Competition, but not described in the literature before. Cerbtora extends the same theoretical framework to the word level, in which certificates are expressed in the same modeling language as the design under test and are validated using efficient automated reasoning engines. We describe the architecture and main components of both tools and evaluate them on competition benchmarks.

Authors 2

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, The Netherlands