摘要： 有界模型校验(Bounded Model Checking)由于验证的不完备性而经常受到验证人员的指责。为了解决这个问题，计算时序深度的算法被提出。该文算法基于可满足性算法引擎，与其它基于可满足性算法引擎的算法不同，为了减少可满足性算法引擎的负担，采用了状态空间显式存储的方法。ISCAS’89 的实例很好证明了该算法的有效性。

关键词: 形式验证；时序深度；可满足性问题

Abstract: 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

Key words: Formal verification; Sequential depth; SAT