Functional Reduction to Speed Up Bounded Model Checking

TL;DR

This paper introduces FRAIG-BMC, a novel method that reduces redundancy in bounded model checking by merging functionally equivalent nodes, significantly improving SAT solving efficiency and speeding up formal property verification.

Contribution

It presents FRAIG-BMC, a technique that incrementally merges functionally equivalent nodes during BMC to enhance scalability and efficiency.

Findings

FRAIG-BMC significantly speeds up BMC in various applications.

Redundancy reduction improves SAT solver performance.

Method accelerates formal property verification processes.

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. Howevefor, 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