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

《对电路的等价性检验方法的探讨》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。

1、对电路的等价性检验方法的探讨摘要：等价性检验是目前电路设计验证中应用最为广泛的形式化方法。为了提高验证的效率,通常使用组合验证的方法来验证大型时序电路。大多数组合等价性检验方法都以二叉判决图(bdd)为主要推理引擎,可能导致内存爆炸题。基于增量的方法是利用两个电路内部的结构相似性,把要验证的问题分解为多个子任务、增量地完成验证。本文则在此基础上对电路的等价性检验方法作出一番探讨。关键词：等价性检验电路验证1、引言一般来说,形式化验证方法可以分为等价性检验(equivalencechecking)、模型检验(modelchecking)和定理证明(theoremprov

2、ing)方法。而等价性检验被广泛地应用到设计的各个阶段。它的基本原理是建立被比较的两个模型之间的关系。检验的依据是数学的定理和公理,以及设计实现所利用的标准的单元库的精确描述。等价性检验程序自动确定被比较的两个设计的关系,而不需要用户的输入,它的优点是使用简单,容易集成到设计流程中。等价性检验方法又包括基于符号和基于增量两种方法。基于符号的检验方法依赖于基于bdd(binarydecision对电路的等价性检验方法的探讨摘要：等价性检验是目前电路设计验证中应用最为广泛的形式化方法。为了提高验证的效率,通常使用组合验证的方法来验证大型时序电路。大多数组合等价性检验方法都

3、以二叉判决图(bdd)为主要推理引擎,可能导致内存爆炸题。基于增量的方法是利用两个电路内部的结构相似性,把要验证的问题分解为多个子任务、增量地完成验证。本文则在此基础上对电路的等价性检验方法作出一番探讨。关键词：等价性检验电路验证1、引言一般来说,形式化验证方法可以分为等价性检验(equivalencechecking)、模型检验(modelchecking)和定理证明(theoremproving)方法。而等价性检验被广泛地应用到设计的各个阶段。它的基本原理是建立被比较的两个模型之间的关系。检验的依据是数学的定理和公理,以及设计实现所利用的标准的单元库的精确描述。等

4、价性检验程序自动确定被比较的两个设计的关系,而不需要用户的输入,它的优点是使用简单,容易集成到设计流程中。等价性检验方法又包括基于符号和基于增量两种方法。基于符号的检验方法依赖于基于bdd(binarydecisiondiagram)遍历有限状态机(fsm)来实现等价性检验的。在基于增量的方法中,利用被验证的两个电路的结构相似性来检验所刻画的系统是否与实现一致,它被进一步划分为:基于替换的方法、基于学习的方法和基于变换的方法。2、等价性检验模型传统的组合电路功能等价性验证是通过构造两个电路的规范表示形式,如真值表或二叉判定图bdds,当且仅当它们的规范形式同构时,这两

5、个电路功能等价。为了验证两个时序电路的等价性,通常需要把它们当成有限状态机,并构造这两者的积自动机。brand将这种计算模型称为miter。它是通过把两个状态机相应的每一对原始输入联接到一起,同时把相应的每一对原始输出联接到一个异或门,而这些异或门就构成了积自动机的输出。如果对于每一个输入序列,积自动机的每个原始输出恒为0,那么这两个时序电路就是等价的。换句话说,就是对于任何输入向量和可达状态,积自动机的原始输出响应总是为0。通常,证明状态机等价性的第一步是从初始状态开始,计算所有可达状态。这就是典型的基于有限状态机遍历算法。尽管最近十多年里,由于bdd方法的研究进展

6、使得基于有限状态机遍历算法有了很大进步,但面对实际的大型设计仍然可能会因构造bdd的表示导致内存爆炸。3、brand的利用atpg的增量验证算法在设计周期中,经常利用两个电路的结构相似性来进行等价性检验。例如,对于检验某种设计性能优化是否与它的原始设计功能等价,或者比较晶体管级网表与门级网表的功能等价,brand的基于增量的检验算法能够验证大规模设计。在下面的讨论中,假设两个待检验的电路都只有一个单一的输出。这种方法很容易应用到多输出的电路。前面已经提到,证明两个电路等价就是检验在一个积自动机(miter)上没有输入向量使其输出为“1”。与符号验证方法不同,该方法不建

7、立bdd表达式,等价性检验被简单地表达成一种搜索问题。它搜索不同的向量,使两个待检验的电路产生对应的不同输出值。如果整个搜索空间穷举后,没有找到不同的向量,那么两个电路等价,否则,生成一个反例证明其不等价。因为一组不同的向量也就是对一个积自动机(miter)的输出g产生恒为“0”的测试向量,所以等价性检验就是简化对g产生恒为“0”的一组测试向量的过程。但是,直接应用atpg来检验输出等价对大型设计来说是非常费时的。而利用两个待检验的电路(cuvs)的结构相似性可以急剧减少设计的复杂性。定义1(信号对)令a1和a2是内部信号,如果a1和a2是来自两个不