现今社会已是海量信息的世界，而支持处理这些信息的最主要物质基础是数字芯片。为了满足日益复杂的系统功能需求，数字电路的设计工作遇到了前所未有的挑战。在数字电路设计流程中，为确保数字电路功能的正确性与完整性，验证工作的重要作用越来越突显，特别是在设计过程中的早期阶段，对系统进行正确的功能验证对该系统的成功开发有着至关重要的意义。数字电路形式验证方法由于具有抽象级别高、建模能力强的特点，特别适合数字电路设计流程中的顶层设计的功能验证问题。目前业界常用的验证方法已经不能完全满足现代设计工作的需要，因此系统研究形式验证方法有其特有的现实意义。本文以多项式符号代数（Polynomial SymbolicAlgebra, PSA）理论为基础，针对于数字电路，研究适合算术密集型产品的形式验证方法。（1）为解决数字芯片设计中模型检验问题，提出基于多项式理论的定界模型检验方法。首先，给出基于多项式形式的电路功能的统一描述。为了能够采用多项式形式描述电路功能，本文在传统的电路控制逻辑描述方法的基础上，将其进一步扩展，将传统方法中的原子命题转化为多项式形式，将布尔特征函数转化为多项式集合的形式。这样，可以与电路数据通路部分建立统一的多项式描述形式。其次，通过建立高级语言的关系模型，给出了电路在高层次描述中目标性质的抽取方法，通过该方法形成待验证性质的多项式形式描述，从而形成了待验证性质与电路功能统一的多项式形式。基于以上两点，本文将定界模型检验问题转化为基于多项式理论的定理证明问题。并采用计算多项式集合良好三角列的方法解决定理证明问题。与传统方法相比，本文方法可在电路高级别抽象上直接进行定界模型检验。（2）为解决数字芯片的数据通路RTL级模型与优化后的RTL级描述之间的等价性检验问题，提出基于多项式理论的等价性验证方法。首先，证明了多项式集合零点集与数据通路等价的关系。将数据通路看作黑盒结构，只考虑输入/输出关系，因此，两个数据通路功能等价，可看作对同一组输入，两个数据通路有相同输出。为此，将多项式集合的解集合看作是多维空间中的点，通过多项式代数簇理论，将空间的点向平面投影，从代数的角度证明了数据通路等价与多项式集合零点集的关系。其次，给出判定多项式集合零点集相等的代数方法。采用多项式理想理论处理零点集等价判定问题，并利用理想良性基的可计算性给出了具体的判定过程。基于以上两点，本文提出验证高级别数据通路功能等价性的求解算法。（3）为提高数字芯片的验证速度，提出基于多项式理论的模块化验证方法。首先，采用模块化的形式描述电路的结构。其次，给出模块化的电路功能计算方法。从基本门电路或电路基本部件出发，从电路模块化的结构描述中获得各个部件的相互约束关系，并以多项式代数中的消元与扩张原理为基础，逐级递归地计算出每一个电路节点的多项式集合的消元理想的Gr bner基，最终获得电路的整体功能描述。基于以上两点，提出基于模块化思想的电路验证问题的代数求解算法。基于Maple等工具建立实验系统，针对上述算法进行了实验研究。实验结果表明，针对算术密集型电路，本文基于PSA的方法在验证效率上要优于传统方法。