一个基于可满足性算法的时序深度计算方法-复旦大学微电子学院.pdf

第32 卷 第2 期 计 算 机 工 程 2006 年1 月 Vol.32 № 2 Computer Engineering January 2006 ·工程应用技术与实现· 文章编号：1000—3428(2006)02—0226—03 文献标识码：A 中图分类号：TP301.6 一个基于可满足性算法的时序深度计算方法 张忠林，唐璞山 (复旦大学微电子系专用集成电路与系统国家重点实验室，上海200433) 摘 要：有界模型校验(Bounded Model Checking) 由于验证的不完备性而经常受到验证人员的指责。为了解决这个问题，计算时序深度的算 法被提出。该文算法基于可满足性算法引擎，与其它基于可满足性算法引擎的算法不同，为了减少可满足性算法引擎的负担，采用了状态 空间显式存储的方法。ISCAS’89 的实例很好证明了该算法的有效性。 关键词：形式验证；时序深度；可满足性问题 A SAT-based Algorithm of Sequential Depth Computation ZHANG Zhonglin, TANG Pushan (State Key Laboratory of ASIC System, Fudan University, Shanghai 200433) 【Abstract 】Bounded model checking is criticized because of its incompleteness in hardware verification. In order to conquer the problem of incompleteness, algorithms used to compute the diameter of the reachable states are proposed. This paper presents a new SAT-based algorithm which is different to other SAT-based algorithms. In order to alleviate the burden of the SAT-solver, it uses an explicit method to store the states. Finally, it reports promising experimental results on the ISCAS 89 benchmarks. 【Key words 】Formal verification; Sequential depth; SAT 1 概述 Formula) 。但是QBF 的计算有两个主要障碍。首先，量词和 目前，电子硬件系统已经广泛应用于各种关键领域。因 取反操作不能简单地用于可满足性算法引擎。其次，路径的 此可靠的硬件系统是至关重要的。在当今的硬件设计小组中 查询运算有遍历操作，过于费时。因此他们对QBF 进行了化 尽管有 70%~80 ％人从事验证工作，但是有错误的芯片还是 简，将 1 步QBF 运算变为2 步可满足性运算。虽然步骤增加 会被生产出来，并且直到用户遇到后才会被发现，从而导致 了，但由于运算变得更简单了，从实验结果来看，速度还是 重大的商业损失。 可接受的。该算法还有一个很大的缺点，当时序深度很深的 到目前为止，最常使用的验证方法还是基于信号模拟的