A Single-Instance Incremental SAT Formulation of Proof- and Counterexample-Based Abstraction

TL;DR

This paper introduces a unified, incremental SAT-based approach that combines counterexample-based and proof-based abstraction methods for bit-level verification, simplifying implementation and broadening solver compatibility.

Contribution

A novel single-instance incremental SAT formulation that interleaves CBA and PBA, eliminating the need for proof-logging and simplifying the abstraction process.

Findings

Simpler conceptual and implementation framework

Eliminates need for proof-logging in PBA

Compatible with a wider range of SAT-solvers

Abstract

This paper presents an efficient, combined formulation of two widely used abstraction methods for bit-level verification: counterexample-based abstraction (CBA) and proof-based abstraction (PBA). Unlike previous work, this new method is formulated as a single, incremental SAT-problem, interleaving CBA and PBA to develop the abstraction in a bottom-up fashion. It is argued that the new method is simpler conceptually and implementation-wise than previous approaches. As an added bonus, proof-logging is not required for the PBA part, which allows for a wider set of SAT-solvers to be used.