组合电路的形式验证.doc

 目 录摘要 1 关键词 1 Abstract 1 Key words 1 1 引言 1 1.1 日益复杂的硬件系统设计 1 1.2 研究背景和意义 1 1.3 设计缺陷的惨重代价 2 1.4 传统验证方法与其局限性 2 1.5 研究现状和典型形式验证工具 2 2 形式验证概述 3 2.1 形式验证分类 3 2.2 等价性检验 4 2.2.1 等价性检验技术 4 2.2.2 等价性检验模型 5 2.2.3 利用ATPG的增量验证算法 5 2.3 形式模型检查 5 2.4 定理证明 5 3 基于BDD的组合电路等价性检验方法 7 3.1 基于ROBDD的等价性检验方法 7 3.2 算法的具体描述 8 3.3 误判问题的处理 8 4 总结 9 致谢 10 参考文献 10 组合电路的形式验证 网络工程专业学生指导教师摘要：在方法验证算法，关键词：Formal Verification of Combinational Circuits Student Majoring in Network Engineering Cao Shuai Tutor Wu Junhua Abstract:With the increasing complexity and tight time-to-market schedules of today’s digital, verification is becoming more and more difficult. Checking the correctness of the design is one of the critical problems in designing a very large scale digital circuit. The traditional verification method can not solve and eliminate all the design error, using formal methods to guarantee the correctness of the digital circuit design is adopted more and more. This thesis describes the research significance, then introduced the Equivalence Checking, Formal Model Checking, Theory Prover and other formal verification method. In this part of the Equivalence Checking explored methods to verify the algorithm using ATPG and discussed the Equivalence Checking based on the Binary Decision Diagram. Key words：Formal Verification; Equivalence Checking; Formal Model Checking; Theory Prover; Binary Decision Diagram 引言 摩尔定律是由英特尔（Intel）创始人之一戈登·摩尔（Gordon Moore）提出来的。其内容为：当价格不变时，集成电路上可容纳的晶体管数目，约每隔18个月便会增加一倍，性能也将提升一倍。换言之，每一美元所能买到的电脑性能，将每隔18个月翻两倍以上。这一定律揭示了信息技术进步的速度。摩尔定律问世已40多年，人们不无惊奇地看到半导体芯片制造工艺水平以一种令人目眩的速度提高。Intel的微处理器芯片Pentium4的主频已高达2G（即12000M），2011年推出了含有10亿个晶体管、每秒可执行1千亿条指令的芯片。这种发展速度是否会无止境地持续下去是成为人们所思考的问题。从技术的角度看，随着硅片上线路密度的增加，其复杂性和差错率也将呈指数增长，同时也使全面而彻底的芯片测试几乎成为不可能。一旦芯片上线条的宽度达到纳米（10-9米）数量级时，相当于只有几个分子的大小，这种情况下材料的物理、化学性能将发生质的变化，致使采用现行工艺的半导体器件不能正常工作，摩尔定律也就要走到尽头。 仿真验证方法是指给定测试向量，检查被验证系统的实际输出是否符合期望输出，从而寻找设计中存在的缺陷。但是，对于复杂的系统，测试向量无法穷举状态空间的所有向量，因此无法确认系统设计是否完全正确。 测试是设计验证的另一个方法，是在对硬件系统的加工后实行的。但是，测试只能证明错误的存在而不能证明错误的不存在。