对电路的等价性检验方法的探讨.doc

对电路的等价性检验方法的探讨摘要：等价性检验是目前电路设计验证中应用最为广泛的形式化方法。为了提高验证的效率,通常使用组合验证的方法来验证大型时序电路。大多数组合等价性检验方法都以二叉判决图(bdd)为主要推理引擎,可能导致内存爆炸题。基于增量的方法是利用两个电路内部的结构相似性,把要验证的问题分解为多个子任务、增量地完成验证。本文则在此基础上对电路的等价性检验方法作出一番探讨。关键词：等价性检验 电路 验证1、引言一般来说,形式化验证方法可以分为等价性检验(equivalence checking)、模型检验(model checking)和定理证明(theorem proving)方法。而等价性检验被广泛地应用到设计的各个阶段。它的基本原理是建立被比较的两个模型之间的关系。检验的依据是数学的定理和公理,以及设计实现所利用的标准的单元库的精确描述。等价性检验程序自动确定被比较的两个设计的关系,而不需要用户的输入,它的优点是使用简单,容易集成到设计流程中。等价性检验方法又包括基于符号和基于增量两种方法。基于符号的检验方法依赖于基于bdd(binary decision diagram)遍历有限状态机(fsm)来实现等价性检验的。在基于增量的方法中,利用被验证的两个电路的结构相似性来检验所刻画的系统是否与实现一致,它被进一步划分为:基于替换的方法、基于学习的方法和基于变换的方法。2、等价性检验模型传统的组合电路功能等价性验证是通过构造两个电路的规范表示形式,如真值表或二叉判定图bdds,当且仅当它们的规范形式同构时,这两个电路功能等价。为了验证两个时序电路的等价性,通常需要把它们当成有限状态机,并构造这两者的积自动机。brand将这种计算模型称为miter。它是通过把两个状态机相应的每一对原始输入联接到一起,同时把相应的每一对原始输出联接到一个异或门,而这些异或门就构成了积自动机的输出。如果对于每一个输入序列,积自动机的每个原始输出恒为0,那么这两个时序电路就是等价的。换句话说,就是对于任何输入向量和可达状态,积自动机的原始输出响应总是为0。通常,证明状态机等价性的第一步是从初始状态开始,计算所有可达状态。这就是典型的基于有限状态机遍历算法。尽管最近十多年里,由于bdd方法的研究进展使得基于有限状态机遍历算法有了很大进步,但面对实际的大型设计仍然可能会因构造bdd的表示导致内存爆炸。3、brand的利用atpg的增量验证算法在设计周期中,经常利用两个电路的结构相似性来进行等价性检验。例如,对于检验某种设计性能优化是否与它的原始设计功能等价,或者比较晶体管级网表与门级网表的功能等价,brand的基于增量的检验算法能够验证大规模设计。在下面的讨论中,假设两个待检验的电路都只有一个单一的输出。这种方法很容易应用到多输出的电路。前面已经提到,证明两个电路等价就是检验在一个积自动机(miter)上没有输入向量使其输出为“1”。与符号验证方法不同,该方法不建立bdd表达式,等价性检验被简单地表达成一种搜索问题。它搜索不同的向量,使两个待检验的电路产生对应的不同输出值。如果整个搜索空间穷举后,没有找到不同的向量,那么两个电路等价,否则,生成一个反例证明其不等价。因为一组不同的向量也就是对一个积自动机(miter)的输出g产生恒为“0”的测试向量,所以等价性检验就是简化对g产生恒为“0”的一组测试向量的过程。但是,直接应用atpg来检验输出等价对大型设计来说是非常费时的。而利用两个待检验的电路(cuvs)的结构相似性可以急剧减少设计的复杂性。定义1(信号对)令a1和a2是内部信号,如果a1和a2是来自两个不同的电路,那么(a1,a2)被称作信号对。例如:a1是c1中的信号,a2为c2中的信号,反之亦然。定义2(等价对)如果二值信号量a1和a2对于任何输入向量是相等的,那么(a1,a2)被称作等价(信号)对。定义3(可容许的对)如果a1是a2的可容许函数,即用信号a2替换信号a1不会改变积自动机(miter)的输出值,那么(a1,a2)被称作是可容许的(信号)对。反之亦然。如果电路中的大部分信号是等价的或者是可容许的,两个电路就被认为是相似的。全面的验证过程是利用这些内部的等价对或者可容许的对来验证两个电路是等价的。3.1 匹配候选对建立好积自动机后,候选等价对或可容许对首先通过随机模拟,名字信息或者用户刻画的信息得到。模拟大量随机向量后,如果应用每组输入向量后,a1和a2具有相同的值,那么,信号对(a1,a2)被认为是一个候选等价对。对于组合电路来说,随机模拟在匹配候选等价对时经常产生满意的结果。但是,不是等价对的候选可容许的对不能用这种方法来判定。候选可容许对可以通过匹配具有相同信号名的信号对和使用由用户刻画的外部信息来得到。如果名字信息和用户刻画的信息都没有得到,那么每个信号对都可以被认为是候选可容许对。在这种情况下,候选对的总数是n1n2,其中n1和n2分别是在c1和c2中的信号的个数。这个数据通常太大,可能使后来的处理非常昂贵。一个可供选择的方法是只关心候选等价对。许多电路能通过只确定等价信号对来有效地进行验证。3.2 对积自动机(miter)逐步剪枝一旦得到了候选等价对,紧接着是进行一系列逐步简化积自动机(miter)大小的操作。首先,候选等价对在电路的拓扑顺序的基础上按扇入优先的顺序进行排序(例如:一个信号排在它的迁移扇入信号之后)。排序之后,算法进入一个循环,其中每个循环选择一个候选对,并且检查目标对是否是可容许的对。检验可容许对是这个算法中最重要的一步。它通过使用(a)中给出的模型运行atpg来实现。在这个模型中,在目标对中的两个信号被连接到一个异或门上。该门的输出用f表示。然后替换第一个信号a1。如果信号f恒为0是不可测试的,那么用a2替换a1,而不改变函数o1和积自动机的输出g的值是安全的。如果证明候选对(a1,a2)的确是等价的,那么用用第二个信号a2替换第一个信号a1就化简了积自动机(miter)的结构。在基于增量的检验方法过程中,积自动机从其原始输入到原始输出逐步简化了,因此,随着算法的进行,计算的复杂度急剧下降。相似的过程通过布尔可满足性和最小化结构的方法已经应用到了向量测试中。3、3 检验原始输出的等价性当积自动机通过合并内部的可容许对之后,每个原始输出对的等价性通过运行atpg来检验。如果找到了测试向量v,那么v就是一个反例,它证明了两个待测试的电路是