随着集成电路的设计规模越来越大、复杂度越来越高,产品上市时间却越来越紧迫,集成电路的验证变得越来越困难。2003年度的国际半导体技术发展报告(International Technology Roadmap for Semi-conductor, ITRS2003)指出,验证已经成为集成电路设计流程中最大瓶颈。传统的模拟验证因其测试周期长、不能完全覆盖,已经不适合当前对集成电路的验证。形式验证作为传统基于模拟的验证方法的补充,日益引起人们的关注。它的特点是使用严格的数学推理来证明一个系统满足全部或部分规范。 本论文在较为全面、深入地研究和总结国内外形式验证技术研究成果的基础上,对组合电路及时序电路验证上分别进行算法研究、设计和实现,取得了较为理想的结果。主要内容包括: 组合电路验证是数字集成电路形式化设计验证的重用方面。论文给出了一种使用布尔可满足性SAT的新颖组合电路等价性验证技术。算法是在联接电路(Miter)中进行推理来简化验证问题,推理中使用了与/非图结构简化、二叉决策图BDD扩展、隐含学习多种方法,最后使用有效SAT解算器zChaff解决验证任务。该算法综合了BDD和SAT的优点,限制BDD构建大小避免了内存爆炸,推理简化减小了SAT搜索空间。 针对利用BDD验证常常出现内存爆炸这一问题,我们注意到在实际的设计流程中,对设计的电路修改优化只是涉及部分电路结构的变化,因此参考电路与实现电路之间存在大量的等价节(即结构相似性)。由于这一特点,本文提出一个高效的割集算法。该算法结合静态割集验证多对节点时的高效性,利用动态在割集验证一对节点时有效性,扬长补短,提高算法的鲁棒性。 时序电路验证比组合电路更复杂,尤其是状态变量多的电路。一种有效的方法是通过锁存器匹配,将部分时序电路验证转化为组合电路验证问题,降低验证的复杂度。本文提出了一种结合多种方法的新颖锁存器匹配算法。算法结合任意