摘要:传统的验证已经不适合对电路的验证,而形式验证技术却能够有效地缩短解决验证问题所要花费的时间,并且能够为产品的质量提供保证。本文根据上海屹澜信息科技有限公司提供的8位RISC core的RTL代码和网表的相关信息,并且将会在介绍形式验证概念的基础上,使用Synopsys公司的Formality工具来进行验证设计。最终验证报告显示总计300个相等可通过的比较点,其中有29个Port和271个DFF,不相等的比较点有0个,并且还有1个Port的检查点不参与验证。其验证结果表明8位RISC core的Reference design和Implentation design逻辑功能一致。
关键词:8位RISC;形式验证;数字后端;版图设计
目录
摘要
Abstract
第一章 绪 论-1
1.1 研究背景-1
1.2 研究意义-1
1.3 论文的主要工作-2
1.4 论文组织结构-2
第二章 Formality工具介绍-3
2.1 Formality的基本特点-3
2.2 Formality工具的应用-3
2.3 Formality工具的功能-4
2.4 Formality的一般验证流程-5
第三章 RISC的原理-6
3.1 RISC CPU简介-6
3.2 RISC的设计原理及结构-6
3.3 RISC的发展前景-8
第四章 8位RISC core的形式验证-9
4.1 验证前的准备工作-9
4.2 使用命令行界面对8位RISC core的验证-12
4.2.1 打开Formality的命令行界面-12
4.2.2 设置Reference Design-12
4.2.3 设置Implementation Design-13
4.2.4 保存及恢复所作的设置-14
4.2.5 进行验证-14
4.3 使用图形用户界面对8位RISC core的验证-15
4.3.1 打开图形GUI界面-15
4.3.2 读入Guidance Files-16
4.3.3 设置Reference design和implementation design-16
4.3.4 Match和验证-18
第五章 数字形式验证结果-20
5.1 对8位RISC core的形式验证结果-20
5.2 查看验证失败时不匹配处的详细信息-22
5.3 诊断程序-22
结束语-24
致谢-25
参考文献-26
附录-27
附录A RISC core芯片图-27
附录B RAM 16x128 FARM模块图-27
附录C sdnrq1.FRAM模块图-28
附录D RISC core电路图-28
附录E RISC core符号图-29
附录F Matching结果图-29
附录G 命令行界面验证结果图-30
附录H 图形界面验证结果图-30