当今微电子学技术的发展，使得含有数千万元件的集成电路已经能够大批量地生产出来，真正的SoC(System on a Chip)正在成为现实。集成电路的设计能力滞后于集成电路的工艺水平。设计VLSI中的关键问题之一是如何检查设计的正确性，即设计验证。因为设计验证的复杂度随着芯片的规模呈指数增加，传统的验证手段，如模拟、测试和仿真技术，对于大型的系统都不是完全的。由于集成电路工艺的复杂性，它的试制费用相当昂贵。为解决设计验证这一难题，过去二十年中，人们发展了一种新方法——形式化验证(Formal Verification)方法。这是VLSI(Very Large Scale Integration)设计验证的一种有希望的方法。形式化验证意味着验证过程是数学化的，而不是如模拟技术那样，是试验性质的。数学化的验证克服了模拟的不足，因为它的覆盖是完全的，并且可以减少验证时间。形式化验证可以对电路描述进行自动化的验证，减少了验证的复杂度。 本文研究基于多项式符号代数理论的形式化验证方法。关于多项式符号代数理论在形式化验证方面的研究，人们给出了WGLs(Weighted Generalized Lists)和TEDs(Taylor Expansion Diagrams)两个多项式表示模型，并给出了相应的等价性验证算法。本文的主要工作如下。 1) 基于WGLs模型，给出了高层的数据通路的规格说明与相应的电路实现之间的等价性验证算法。由于WGLs不能应用于含有布尔变量和字级变量电路描述的表示，所以给出一个基于WGLs的新模型LWGLs(Labeled and Weighted Generalized Lists)。LWGLs可以应用于含有布尔变量和字级变量电路描述的表示，并应用于高层次电路描述与电路实现或不同的电路实现之间的等价性验证。 2) 改进了TEDs的加法和乘法的算法描述，并对算法的复杂度进行分析。为了对电路的逻辑行为和时序行为进行统一表示，给出了一个基于TEDs的新的模型，称为时序泰勒展开图(Timed Taylor Expansion Diagrams，TTEDs)。TTEDs在保持TEDs原有的电路表示的规范上引入了时序信息。 理论研究和实验结果验证了文中提出的模型和算法的有效性。