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

• 作者: 唐璞山 张忠林
• 来源期刊: 计算机工程
• 学科: 工学
• 关键词: 形式验证 时序深度 可满足性问题
• 年，卷（期）: 2006,（2）
• 所属期刊栏目: 工程应用技术与实现
• 页码范围: 226-228,231
• 页数: 4页
• 分类号: TP301.6
• 字数: 4961字
• 语种: 中文
• DOI: 10.3969/j.issn.1000-3428.2006.02.081

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	唐璞山	复旦大学微电子系专用集成电路与系统国家重点实验室	36	143	7.0	9.0
2	张忠林	复旦大学微电子系专用集成电路与系统国家重点实验室	4	36	3.0	4.0