随着集成电路技术的飞速发展，电路的规模不断增大。电路验证领域正面临前所未有的挑战，如何快速并且完备地完成超大规模集成电路的设计验证，已经成为当前的研究热点。与传统的基于模拟的验证方法相比，形式化验证方法中的模型验证方法由于具有完备性的优点被广泛使用。为了扩大模型检验的验证范围，被称为有界模型检验的验证方法被提出。然而，有界模型检验算法最主要的缺点是验证的不完备性，即我们不知道验证所需的深度。为了克服有界模型检验算法的这个缺点，本文提出的时序深度计算的算法。该算法创新之处分为两点：(1)基于可满足算法引擎的后续状态的计算。由于本文在后续状态的计算中使用了可满足算法引擎，大大提高了后续状态的计算速度和计算的能力。并且我们计算的规模较小，每次运算后可满足问题的子句数目变化很小，因此一直可以保持比较快速和高效的计算。(2)基于高度平衡二叉搜索树的历史状态的存储方法。由于本文所提的算法需要大量的查找历史状态的操作，因此如何得到一个稳定的平均查找时间就成为了本算法的一个要点。因此本文使用了高度平衡二叉搜索树的算法，该算法在大量结点插入运算后，可以保持良好的搜索高度，使得搜索时间稳定在O(log2n)量级。此外，我们的提出的算法具有很强的灵活性。对于内部，程序可以调用不同的SATSolver来完成；对于外部，可以作为独立的软件使用，也可以作为一个模块被其他算法调用，比如用于时序电路的等价验证。