SAT-Based Verification Framework

Verifying modern designs requires robust and scalable approaches in order to meet more demanding time-to-market requirements. We present our SAT-based model checking platform VeriSol [53] based on robust and scalable algorithms (as discussed in Parts I-IV) that are tightly integrated for verifying large scale industry designs. We briefly discuss and analyze the strengths and weaknesses of various verification engines in VeriSol as each addresses the capacity and performance issues inherent in verifying large designs. Using several industry case studies, we describe the interplay of these engines highlighting their contribution at each step of verification. We also discuss the various modeling issues in handling complex features in real designs.