组合电路的形式验证

《组合电路的形式验证》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。

1、目录摘要1关键词1Abstract1Keywords11引言11.1日益复杂的硬件系统设计11.2研究背景和意义11.3设计缺陷的惨重代价21.4传统验证方法与其局限性21.5研究现状和典型形式验证工具22形式验证概述32.1形式验证分类32.2等价性检验42.2.1等价性检验技术42.2.2等价性检验模型52.2.3利用ATPG的增量验证算法52.3形式模型检查52.4定理证明53基于BDD的组合电路等价性检验方法73.1基于ROBDD的等价性检验方法73.2算法的具体描述83.3误判问题的处理84总结9致谢10参考文献10组合电路的形式验证

2、网络工程专业学生曹帅指导教师吴俊华摘要：随着集成电路的设计规模越来越大、复杂度越来越高，产品上市时间却越来越紧迫，集成电路的验证变得越来越困难。设计验证是检查大规模数字电路正确性中的关键环节之一。传统的验证手段难以解决和排除所有的设计错误，利用形式验证来保证数字电路设计的正确性的方法被越来越多的采用。首先说明了课题研究的意义，接着介绍了等价性检查、形式模型检查、定理证明等形式化验证方法。在等价性检验中探讨了利用自动测试向量产生的方法验证算法，讨论了基于二叉决策图的组合电路的等价性检查方法。关键词：形式验证等价性检查形式模型检查定理证明二叉决策图

3、FormalVerificationofCombinationalCircuitsStudentMajoringinNetworkEngineeringCaoShuaiTutorWuJunhuaAbstract:Withtheincreasingcomplexityandtighttime-to-marketschedulesoftoday’sdigital,verificationisbecomingmoreandmoredifficult.Checkingthecorrectnessofthedesignisoneofthecritical

4、problemsindesigningaverylargescaledigitalcircuit.Thetraditionalverificationmethodcannotsolveandeliminateallthedesignerror,usingformalmethodstoguaranteethecorrectnessofthedigitalcircuitdesignisadoptedmoreandmore.Thisthesisdescribestheresearchsignificance,thenintroducedtheEqui

5、valenceChecking,FormalModelChecking,TheoryProverandotherformalverificationmethod.InthispartoftheEquivalenceCheckingexploredmethodstoverifythealgorithmusingATPGanddiscussedtheEquivalenceCheckingbasedontheBinaryDecisionDiagram.Keywords：FormalVerification;EquivalenceChecking;Fo

6、rmalModelChecking;TheoryProver;BinaryDecisionDiagram1引言1.1日益复杂的硬件系统设计摩尔定律是由英特尔（Intel）创始人之一戈登·摩尔（GordonMoore）提出来的。其内容为：当价格不变时，集成电路上可容纳的晶体管数目，约每隔18个月便会增加一倍，性能也将提升一倍。换言之，每一美元所能买到的电脑性能，将每隔18个月翻两倍以上。这一定律揭示了信息技术进步的速度。摩尔定律问世已40多年，人们不无惊奇地看到半导体芯片制造工艺水平以一种令人目眩的速度提高。Intel的微处理器芯片Pentium

7、4的主频已高达2G（即12000M），2011年推出了含有10亿个晶体管、每秒可执行1千亿条指令的芯片。这种发展速度是否会无止境地持续下去是成为人们所思考的问题。从技术的角度看，随着硅片上线路密度的增加，其复杂性和差错率也将呈指数增长，同时也使全面而彻底的芯片测试几乎成为不可能。一旦芯片上线条的宽度达到纳米（10-9米）数量级时，相当于只有几个分子的大小，这种情况下材料的物理、化学性能将发生质的变化，致使采用现行工艺的半导体器件不能正常工作，摩尔定律也就要走到尽头。101.1研究背景和意义硬件系统要求很高的可靠性，随着系统规模的增大，出现错误的

8、概率也大大增加了，有些错误和缺陷所带来的后果是难以接受的。在大规模集成电路领域，验证技术的发展滞后于设计技术。设计验证是检查大规模集成电路正确性中的关