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