Fine-grain abstraction and sequential do not cares for large scale model checking

Abstraction refinement is a key technique for applying model checking to the verification of real-world digital systems. In previous work, the abstraction granularity is often limited at the state variable level, which is too coarse for verifying industrial-scale designs. In this paper, we propose a finer grain abstraction in which intermediate variables are selectively inserted to partition large combinational logic cones into smaller pieces; these intermediate variables, together with the state variables, are then treated as "atoms" in abstraction refinement. With this fine-grain approach, refinement is conducted in two different directions, sequential and Boolean. We propose a SAT-based method for predicting the appropriate refinement direction, and apply greedy minimization in both directions to keep the refinement set small. We also explore the use of approximate reachable states of the remaining submodules to help verifying the abstract model. Experimental studies show that the proposed techniques significantly improve the performance of abstraction refinement, and therefore increase the model checker's ability to handle large designs.