Enhancing SAT-based sequential depth computation by pruning search space

The sequential depth determines the completeness of bounded model checking in design verification. Recently, a SATbased method is proposed to compute the sequential depth of a design by searching the state space. Unfortunately, it suffers from the search space explosion due to the exponential growth of design complexity. To alleviate the impact of state space explosion, we propose a search space reduction method. We collect the learned states and consider them constraints for further path searching. Furthermore, we propose a heuristic to guide the SAT-solver to efficiently find a shortest path. The experimental results show that as compared to another method which also enhances the previous SAT-based method using a branch-and-bound strategy, our approach obtains more improvements. Categories and Subject Descriptors B.6.3 [Logic Design]: Design Aids—verification General Terms Algorithms, Verification Keywords Satisfiability(SAT), sequential depth

• Type: Conference
• Year: 2009
• Where: GLVLSI
• Authors: Yung-Chih Chen, Chun-Yao Wang
• Keywords: GLVLSI 2009, Sequential Depth, Space Explosion, State Space, VLSI