Accelerating High-level Bounded Model Checking

SAT-based bounded model checking (BMC) has been found promising in finding deep bugs in industry designs and scaling well with design sizes. However, it has limitations due to requirement of finite data paths, inefficient translations and loss of high-level design information during the BMC problem formulation. These shortcomings inherent in Boolean-level BMC can be avoided by using high-level BMC. We propose a novel framework for high-level BMC, which includes several techniques that extract high-level design information from EFSM models to make the verification model "BMC friendly", and use it on-the-fly to simplify the BMC problem instances. Such techniques overcome the inherent limitations of Boolean-level BMC, while allowing integration of state-of-the-art techniques for BMC. In our controlled experiments we found significant performance improvements achievable by the proposed techniques