Effective Heuristics for Counterexample-Guided Abstraction Refinement

Verification of complex system-on-a-chip (SoC) designs becomes a critical problem in practice. We consider using model checking to verify the correctness of such systems. We study the state separation problem in the framework of counterexample-guided abstraction refinement. We present two fast heuristics to solve this problem. To the best of our knowledge, our work is the first study on the effectiveness of greedy heuristics for this problem. In comparison with the latest work using the decision tree learning (DTL) solver, the proposed method performs about three orders of magnitude faster and the size of the separation set is 70% smaller on average.