Functional Reduction to Speed Up Bounded Model Checking

TL;DR

Bounded model checking can struggle with deep bounds when verification targets include multiple copies of similar circuits. The paper presents FRAIG-BMC, which interleaves on-the-fly FRAIG-style functional reduction with BMC unrolling, using trivial simplification, structural hashing, and functional redundancy removal to shrink the CNF before SAT solving. Experimental results across SEC, PartRet, and IFC benchmarks show significant speedups and deeper bound exploration compared to standard BMC and baselines. The approach improves FPV scalability for replicated modules and complements existing BMC acceleration techniques by reducing redundancy during unrolling.

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

Figures (3)

• Figure 1: An illustration of integrating FRAIG in BMC unrolling
• Figure 2: Number of solved cases vs. runtime for PartRet
• Figure 3: Number of solved cases vs. runtime for IFC