论文部分内容阅读
随着集成电路技术和制造技术不断进步,电路的规模也不断增大,电路验证领域面临着前所未有的挑战。传统的基于模拟的验证方法不能满足电路复杂度增大的需要,具有完备性特点的形式化验证方法开始得到人们的关注,成为当前的研究热点。
本文研究工作是针对组合电路的等价验证展开的。由于近些年来,作为验证基本问题的可满足性问题(SAT)研究取得了重大进展,有效的SAT解算器诸如zChaff,BerkMin和C.SAT等已可解决很大规模SAT问题,并且作为一个优秀搜索引擎在电路验证问题方面有着广泛应用。本文分析了现有的电路可满足性验证工具的优缺点,针对验证中学习效率的瓶颈提出了改进的方法,能够更加合理地利用电路现有的信息。
本文主要的创新之处在于:(1)对待验证电路进行与/非图同构简化,合并待验证两电路的相似部分,以减小待验证电路产生的数据结构规模。(2)根据电路的拓扑结构,合理选择学习子句,避免重复无用的学习过程。(3)通过模拟蕴含学习,能够避免过深层次搜索,从而快速得到电路信息子句,以减少SAT推理的搜索空间。从实验分析表明,这些措施在有效地减少学习时间的同时,又保证了整体验证过程的完备性和高效率。