Verification by parts: reusing component invariant checking results

Abstract

This study explores the utility of reusing proven component invariants in the backward reachability-based sequential equivalence checking paradigm of formal verification. The authors present a formal method for simplifying the process of proving global invariants on an integrated design using the reachability information of the component state spaces, obtained from known invariants for the components of the design. Experimental results on benchmark circuits reveal that deriving the approximate reachability don't cares from the proofs of component invariants helps in reducing both the depth and breadth of the search.