摘要:传统的验证已经不适合对电路的验证，而形式验证技术却能够有效地缩短解决验证问题所要花费的时间，并且能够为产品的质量提供保证。本文根据上海屹澜信息科技有限公司提供的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