Exploiting Target Enlargement and Dynamic Abstraction within Mixed BDD and SAT Invariant Checking

We experimentally test our methodology within an industrial environment, the Intel BOolean VErifierBOVE. Preliminary results on standard benchmarks (the ISCAS'89, ISCAS'89-addendum, and VIS suites), and industrial ones (the IBM Formal Verification Benchmark Library) are provided. Results show interesting improvements over state-of-the-art techniques: We could decrease CPU time up to a 5x factor, when performing verification with the same depth, or we could increase the verification depth up to 30%, when performing verification within the same time limit.