A SAT-based Algorithm of Sequential Depth Computation
Zhonglin Zhang, Pushan Tang · Jisuanji gongcheng · 2006
Bounded model checking is criticized because of its incompleteness in hardware verification. In order to conquer the problem of incompleteness, algorithms used to compute the diameter of the reachable states are proposed. This paper presents a new SAT-based algorithm which is different to other SAT-based algorithms. In order to alleviate the burden of the SAT-solver, it uses an explicit method to store the states. Finally, it reports promising experimental results on the ISCAS 89 benchmarks.