Interpolation-sequence based model checking

Abstract—SAT-based model,checking,is the most,widely,used method,for verifying industrial designs against their specification. This is due,to its ability to handle,designs with thousands,of state elements,and more. The main,drawback,of using SAT-based model,checking,is its orientation towards,”bug-hunting” rather than,full verification of a given specification. Previous works demonstrated,how,Unbounded,Model Checking can be achieved using a SAT solver. In this work,we present a novel SAT-based approach,to full verification. The approach,combines,BMC with interpolation-sequence,in order to imitate BDD-based Symbolic Model Checking. We demonstrate,the usefulness of our method by applying,it to industrial-size hardware,designs from,Intel. Our method,compares,favorably with McMillan’s interpolation based model,checking,algorithm.