FRAIG-BMC: Functional Reduction to Speed Up Bounded Model Checking

From bibtex.

Abstract

Bounded model checking (BMC) is a widely used technique for formal property verification (FPV), where the transition relation is repeatedly unrolled to increasing depths and encoded into Boolean satisfiability (SAT) queries. As the bound grows deeper, these SAT queries typically become more difficult to solve, posing scalability challenges. However, many FPV problems involve multiple copies of related circuits, creating opportunities to simplify the unrolled transition relation. Motivated by the functionally reduced and-inverter-graph (FRAIG) technique, we propose FRAIG-BMC, which incrementally identifies and merges functionally equivalent nodes during the unrolling process. By reducing redundancy, FRAIG-BMC improves the efficiency of SAT solving and accelerates property checking. Experiments demonstrate that FRAIG-BMC significantly speeds up BMC across a range of applications, including sequential equivalence checking, partial retention register detection, and information flow checking.