一个基于可满足性算法的时序深度计算方法

摘要：

有界模型校验(Bounded Model Checking)由于验证的不完备性而经常受到验证人员的指责.为了解决这个问题,计算时序深度的算法被提出.该文算法基于可满足性算法引擎,与其它基于可满足性算法引擎的算法不同,为了减少可满足性算法引擎的负担,采用了状态空间显式存储的方法.ISCAS'89的实例很好证明了该算法的有效性.

关键词：形式验证、时序深度、可满足性问题

所属期刊栏目：32

分类号：TP301.6(计算技术、计算机技术)

资助基金：中国科学院资助项目90209002;国家科技攻关项目2002AAIZ1460

在线出版日期：2006-04-13（万方平台首次上网日期，不代表论文的发表时间）

页数：共4页

页码：226-228,231