集成电路的逻辑等价性验证研究

bekindasd

摘要：集成电路规模的快速增长使得验证的难度越来越大，传统的模拟和仿真不但需要花费大量的时间，而且不能保证完全的验证覆盖率，已经不能满足现时集成电路设计的要求。形式验证利用数学的方法隐式遍历所有可能的情况，能保证完全的验证覆盖率，所需要的验证时间也大幅减少，是克服验证瓶颈的可行途径。
关键词：集成电路;形式验证;等价性验证;二叉判定图;可满足性问题

集成电路设计是一项十分复杂的工程，任何微小的失误都可能造成巨大的损失。1994年Intel公司的Pentium芯片在上市后被发现存在浮点除法错误，虽然这种错误发生的概率只有几亿分之一，但它仍给Intel公司造成了4.75亿美元的经济损失和难以估量的形象损失。1996年6月4日，欧洲航天局研制的阿里亚娜五型火箭在发射后不到40秒就爆炸坠毁，事后调查发现，错误发生于当一个很大的64位浮点数转换为16位带符号整数时出现异常，细微的错误导致数十年的努力毁于一旦。
1 ^8 B# n8 {1 s& ~8 v) C
% s) K" s/ x% p& C9 O# k
7 h/ c6 c& n$ o0 _
集成电路的逻辑等价性验证研究.pdf (3.18 MB, 下载次数: 0)

2021-1-15 10:33 上传

点击文件名下载附件
下载积分: 威望 -5

' J2 m& G  {0 U1 j
8 }  M! l$ o0 r$ T6 E2 K- G
) B4 F) Z# t2 b6 L
; F* ?, |  ]- y9 o( J5 @, b

starskyuu

集成电路设计是一项复杂的工程，过程也很艰巨