[讨论] 集成电路的逻辑等价性验证研究（浙大博士论文）

集成 电 路规模的快速增长使得验证的难度越来越大，传统的模拟和仿真不但需要花费大量的时间，而且不能保证完全的验证覆盖率，己经不能满足现时集成电路设计的要求。形式验证利用数学的方法隐式遍历所有可能的情况，能保证完全的验证覆盖率，所需要的验证时间也大幅减少，是克服验证瓶颈的可行途径。等价性验证作为一种实用化的形式验证方法，常被用于综合后和人工修改后电路的功能验证，本论文围绕等价性验证在以下三个方面展开了有价值的研究: 1. 在 验 证组合电路的等价性时，直接构建原始输出的BDD并进行比较的方法已经不再适用，需要发掘出两个待验证电路中等价的内部结点，利用这些结点组成割集，将原有的验证问题分割成一系列小而简单的子问题。针对割集在组合等价性验证中的运用，本文创新性地提出了结合通用割集和专用割集的验证方法，针对由割集引起的误判，本文提出了一种注重消除高层次结点间依赖关系的处理策略。基于ISCAS85电路的实验结果表明本文中的方法可以有效加快组合电路的等价性验证。 2. 在 验证时序电路的等价性时，'常需要通过前时间帧计算(pre-image computation)判断某个状态是否由初始状态可达，它占用了全部验证时间中的很大一部分，针对这种情况，本文创新性地提出了一种利用状态缓存的时序验证方法，将模拟过程中到达的状态缓存为[if达状态， 同时缓存验证过程中被确认为不可达的状态，利用它们避免重复的前时间帧计算，基于MCNC91的实验结果表明了本方法的有效性 3. 可 满足性问题是近十多年来的一个研究热点，它己经超越了单纯数学问题的范畴，被广泛应用于EDA设计的各个方面。基于SAT的等价性验证方法更适于发掘电路中的不等价结点，对于实际等价结点的验证，BDD在内存占用不是很高时具有更高的效率，本文提出了一种结合BDD和SAT 两种引擎的时序验证方法，首先运用BDD引擎对结点进行验证，如果验证过程中超过了设定的限制，再调用SAT 引擎，这样能充分发挥它们各自的优点，对IsCAS89 电路的实验结果表明，两种引擎的结合可以有效地减少验证所需的时间。

 

本帖最后由 paulhyde 于 2014-9-15 09:34 编辑