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

摘要

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