可满足性问题算法研究以及在时序电路等价验证中的应用

【作者】 丁敏；

【导师】 唐璞山；

【作者基本信息】 复旦大学 ， 微电子与固体电子学， 2005， 博士

【摘要】 当今的VLSI芯片设计给验证带来巨大挑战。形式验证作为传统模拟验证的补充越来越受到重视。提高形式验证的验证规模和速度成为国际研究的热点。本文的研究工作针对这个趋势,可以分成两个部分: Ⅰ.可满足性算法的研究。本文的研究工作首先就从验证问题的基本理论问题—可满足性问题入手。选择目前可满足性问题中的主流算法—DPLL算法作为研究的主要对象。分析了DPLL算法流程中基本且重要的启发式优化策略。并在此基础上,针对高级推理过程,提出了具有动态删除策略的改进了的失败性文字检查(FLD)过程。具体贡献有:1)从对动态删除策略的定性分析和实验结果分析表明,本文提出的动态删除策略在大大降低原有FLD过程的计算时间同时,减小了实际的DPLL算法的搜索空间,因而提高了DPLL算法的总体运行速度;2)由于DPLL算法在当前可满足性问题中的垄断地位,任何优化策略都必须适合集成到该算法中。同其他的高级推理过程技术相比,经过本文改进后的FLD技术更适合结合到DPLL算法中。 Ⅱ.时序电路等价验证的研究。本文在对可满足性问题的研究基础上,着重研究将可满足性问题的算法作为验证引擎应用到时序电路等价验证中。本文先分析了传统的基于状态遍历算法及其优缺点,比较了两种主流引擎—BDD和SAT的优缺点,然后利用了模型检查中的基于数学归纳法思想,提出了单独使用可满足性算法作为引擎的基于时间帧展开的时序电路等价验证算法。该算法的特点有:1)由于我们的算法只使用到了可满足性算法引擎,因而和采用BDD引擎的算法不同,不存在内存增长过快的问题。并且本文在算法的构造和改进中提高了引擎在迭代使用时候的效率;2)我们的算法在结合了数学归纳法、不可满足子集提取和结构不动点计算这三种已有的技术基础后,更适合用于时序深度较深的逻辑层时序电路的等价验证。而且,在整合三种技术后,又提出了一些改进措施。从实验分析表明,这些改进措施在有效降低可满足性算法引擎的计算时间同时,也进一步减缓了内存的增长,优于单独使用数学归纳法的时序等价验证。更多还原

【Abstract】 The development of modern VLSI design challenges the verification process. As the complement to traditional simulation-based verification process, Formal Verification methods gain more momentum recently. Improving the scalability and speed of Formal Methods becomes hot spot in worldwide research. By following this trend, this thesis can be divided into two parts:I. The research of Satisfiability problem (SAT). As a fundamental problem of formal verification, SAT algorithms are our startup research. The mainstream algorithm - DPLL based algorithm is selected as our research object. After analyzing the basic heuristics used in DPLL and its advanced reasoning techniques, we presented a modified FLD procedure with our Dynamic Filtering heuristic. The main contributions are: 1) The presented Dynamic Filtering heuristic reduced the computational overhead of FLD and the space searched by DPLL procedure while improving the running speed of DPLL algorithm; 2) Since DPLL-based algorithms dominate this area, any heuristics used must be suitable to be integrated into this kind of algorithm. Compared with other advanced reasoning techniques, our modified FLD procedure is more suitable to be integrated into DPLL algorithm.II. The research of sequential equivalence checking problem. Based on the research of SAT algorithms, we pay more effort on using SAT algorithm as engine into the sequential equivalence checking. The traditional state-space traversal based algorithm is analyzed and two main engines - BDD and SAT are compared. Then, by exploiting the induction based algorithms of Model checking, a frame expansion based algorithm is presented that uses SAT as the only engine. The main characteristics are: 1) Our verification algorithm uses SAT algorithm as the only engine. In contrast to BDD-based algorithm, not only there is no memory explosion problem, but also it improves the iteration efficiency of the engine. 2) By integrated unsatisfiable core extraction, induction based verification and structural fixed-point calculation, our algorithm is more suitable for verifying circuits with long sequential depth. Using our modification techniques, the presented algorithm is superior to the induction-based algorithm.更多还原