随着集成电路的设计规模越大越大、复杂度越来越高，产品上市时间却越来越紧迫，集成电路的验证变得越来越困难。2003年度的国际半导体技术发展报告(International Technology Roadmap for Semi-conductor，ITRS2003)指出，验证已经成为集成电路设计流程中最大瓶颈。传统的模拟验证因其测试周期长、不能完全覆盖，已经不适合当前对集成电路的验证。过去二十年中，人们发展了一种新方法—形式化验证(Formal Verification)方法。这是VLSI(Very Large Scale Integration)设计验证的一种有希望的方法。形式验证意味着验证过程是数学化的，而不是如模拟技术那样，是试验性质的。数学化的验证克服了模拟的不足，因为它的覆盖是完全的。形式验证可以对电路描述进行自动化的验证，减少了验证的复杂度。形式验证作为传统基于模拟的验证方法的补充，日益引起人们的关注。它的特点是使用严格的数学推理来证明一个系统满足全部或部分规范。本文研究基于BDD及布尔可满足(SAT)算法的形式化验证方法。本文针对布尔可满足性SAT算法中存在的搜索空间大且复杂度高等问题，对SAT算法进行了相应的改进，并提出了一种新的SAT的全局搜索算法—DC&DS算法。其搜索空间比现有的布尔可满足性算法搜索空间都低得多，从而大大提高了算法的效率。并将该算法应用到结合BDD和SAT算法的形式验证中，并且进行了实验分析。理论研究和实验结果验证了文中提出的新算法的有效性。