节点文献
用形式方法验证通用CPU设计
Formal Verification of General Purpose CPU Designs
【Author】 Guanghui Li Ming Shao Xiaowei Li ( Department of Information, Zhejiang Forestry College, Hangzhou 311300) ( Institute of Computing Technology, Chinese Academy of Sciences, Beijing 100080)
【机构】 浙江林学院信息系;
【摘要】 随着集成电路设计复杂性的日益增加,功能验证已成为整个设计流程的瓶颈。传统的模拟验证方法需要大量的时间,而且不能获得完全的覆盖率;形式验证方法是模拟方法的重要补充,它无需产生测试激励,不仅能够缩短设计周期,而且能够达到完全的功能覆盖率。本文介绍了目前应用最广泛的一种形式验证方法——等价性检验在一款通用CPU设计验证中的应用, 包括RTL设计与门级网表、门级网表与门级网表、RTL设计与RTL设计之间的功能等价性验证.文章着重讨论了快速完成验证任务的方案,以及验证过程中一些常见问题的解决办法。
【Abstract】 With the increasing complexity of integrated circuits designs, functional verification has become the bottle-neck of design flow. The traditional simulation based validation is very time-consuming, and is quite ad-hoc and not complete. An alternative technique is formal verification, which needs no test vector, and can reduce the design cycle with full functional coverage. In this paper, we introduce one most popular formal verification method--equivalence checking for verification of a general purpose CPU design, including proving the equivalence of two designs in different levels of abstraction (e.g. RTL to gates, gates to gates, RTL to RTL). We discuss the scheme of fast finishing this verification task, and some techniques to solve some common problems.
【Key words】 formal verification; simulation; equivalence checking; compare point matching;
- 【会议录名称】 第十届全国容错计算学术会议论文集
- 【会议名称】第十届全国容错计算学术会议
- 【会议时间】2003-09
- 【会议地点】中国北京
- 【分类号】TP332
- 【主办单位】中国计算机学会容错计算专业委员会