芯片设计的日趋复杂化和高速化，对设计自动化的理论和方法提出了新的要求。EDA研究是一个具有挑战性又有发展前景的领域，本论文研究的是EDA领域中超大规模集成电路的形式验证技术。 论文首先对形式验证中的等价性检测方法进行了深入的探讨。等价性检验是目前在工业实践中最广泛使用的形式方法，在进行组合电路等价性检测中本文提出了有序有限状态机的概念，并详细介绍了等价性检验算法的实现过程。通过对算法的理论性分析可知，算法的时间复杂度为多项式规模的，该算法对现有的等价性检验算法有一定的改进。它是一种电路描述的新的模型，通过这种新模型可以对组合电路的等价性检验进行方便、高效的验证。 然后论文进行了模型检验方法的研究，对当前的最新理论成果进行了初步的分析，并在符号模型检验平台SMV系统上进行了一些常见电路的验证。试验结果表明了这种技术的可行性和实用性。文章最后对形式验证的另一种技术——定理证明方法进行了相应的探讨。并针对理论验证的算法，提出了一种分解策略。分解的依据是命题演算系统的推理规则。利用这种策略，可以对大规模的电路构建逻辑命题，并用自动定理证明器进行验证。