摘要:数字形式验证，使用等价性检查对寄存器传输级别源代码和综合后门级网表的功能等同性进行对比，确保逻辑综合期间原始HDL描述电路功能没有改变，保障设计的一致性。

课题使用synopsys公司形式验证工具formality实现了ORCA IP的数字形式验证。比对结果中1837个端点名称相一致，121处主模块输入和block-box输出相匹配。RTL中点10662个不匹配，综合后717个不匹配；RTL中主输入，模块输出232个不匹配，综合后32个不匹配；RTL中没使用的点261个不匹配，综合后0个不匹配。在验证结果中通过的比较点有527个，有28个失败的比较点，没有中止的比较点，而没有验证的比较点有1290个。整个形式验证满足晶门科技（中国）有限公司的总体验证要求。

关键词：数字电路设计；形式验证；linux；fomality

目录

摘要

ABSTRACT

第一章  绪论-1

1.1数字电路的发展-1

1.2微电子技术发展-1

1.3数字电路设计流程-2

1.3.1前端设计流程-2

1.3.2后端设计流程-3

第二章  开发环境-5

2.1Linux操作系统-5

2.1.1Linux的特点-5

2.1.2Linux树形目录结构-6

2.1.3Linux的文件系统-6

2.2Vi编辑器-6

2.2.1VI工作模式-7

2.2.2Vi使用注意事项-7

2.3Formality工具-7

2.4TCL语言-8

第三章  基本原理-10

3.1数字形式验证原理-10

3.1.1形式验证的优缺点-10

3.1.2形式验证的分类-11

3.2ORCA IP原理-12

3.2.1ORCA微处理器组成结构-12

3.2.2ORCA的框架设计-14

3.3SMIC 90nm工艺-15

3.3.1SMIC 90nm工艺的特点-15

3.3.290nm制造工艺对ORCA性能的影响-16

3.4等价性检验中的逻辑锥和比较点-16

第四章  项目实战-18

4.1Formality调用的指令输入-18

4.2基本formality脚本-18

4.3设计流程-19

4.3.1基本的TCL脚本的编写-19

4.3.2脚本运行流程-19

4.3.3Guidance-21

第五章  结果分析-22

5.1比较结果分析-22

5.2验证结果分析-22

结束语-24

致  谢-25

参考文献-26

附录-27

附录A数字电路设计流程-27

附录B形式验证比对流程-28

附录C形式验证TCL脚本-28

附录D比对结果-29

附录E验证结果-29