设计大规模数字电路中的关键问题之一是如何检查设计的正确性，即设计验证。但是，设计验证的复杂度随着芯片的规模增大呈指数增加。传统的验证手段难以排除所有的设计错误，人们转而求助于各种形式验证方法来保证设计在各种可能输入组合下的正确性。 形式验证是EDA领域的关键技术，在电路设计中越来越显示出重要性。本文首先介绍了EDA的发展，并说明了课题的研究意义，接着对形式验证方法做了简要的综述，介绍了等价性检验、模型检验和定理证明等形式化验证方法，本文主要内容论述改进后的形式验证方法。 等价性检验是形式验证的一个重要方法，但在等价性检验中，一般验证只考虑了底层的信息，本文把高层的规格说明信息用在组合电路的等价性检验中。多项式是表示电路的一种有效方法，但对于包含分支的电路，多项式表示的阶次一般比较高。本文给出了一种含有分支电路的多项式表示的有效方法，并把无关项子集考虑进来，以简化多项式阶的求解。在此基础上，给出一个基于多项式表示的等价性检验方法。 随着集成电路规模的扩大，越来越多的复杂设计适合采用基于IP核的设计。由于知识产权的保护，包含黑盒的设计验证是一项非常重要的任务。文献中这方面的方法基本上是基于BDD思想的，本文给出了一种基于多项式表示的特征函数验证方法，对包含黑盒的组合电路能进行有效的验证。