Word level property directed reachability
Hari Govind V K, Grigory Fedyukovich, Arie Gurfinkel
Abstract
Verification approaches based on constraint solvers are successfully applied in firmware and other low-level code that interfaces with hardware. While for proving safety of gate-level sequential circuits, it often suffices to bit-blast and reduce to SAT-based IC3 or Property Directed Reachability (IC3/PDR), for handling machine-level instructions that perform arithmetic and data manipulation operations, word-level reasoning should be conducted. However, because of poor support for interpolation and quantifier elimination in the theory of bit-vectors (BV), previous attempts to lift IC3/PDR to word level required integrating it into an external abstraction-refinement loop. Aiming to reach more scalable bit-precise verification, we propose to bring useful insights from PDR-based verification algorithms used in software. In particular, instead of using bit-blasting to eliminate quantifiers from BV-formulas, we present a less expensive method for iterative approximate quantifier elimination in BV. It naturally supports all bit-operators and can be optimized further by applying rules inspired by modular linear arithmetic. Finally, we leverage recent techniques on learning inductive invariants based on explicit global guidance, thus allowing the approach to bypass interpolation. Our implementation on top of Spacer, a PDR-based verifier shows that such a word-level PDR is promising and can be more effective than state-of-the-art.