（微电子学与固体电子学专业论文）时序电路的等价验证方法及其在FPGA中的应用.pdf

摘要 摘要 髓着集成电路设计水平的进步，电路规模日益增大，电路设计的时间越来越多的耗 费在电路的验证问题上。传统的基于模拟的验证逐渐不能满足验证的需要。形式验证 方法作为传统模拟验证方法的补充成为研究的热点。等价验证可以分为组合电路的等 价验证和时序电路的等价验证。组合电路的等价验证算法几前发展比较成熟，成为很 多时序电路验证算法的皋础。本文的研究t 作丰要集- lr 在时序电路的等价验证部分， 由婀部分组成： 第一部分是时序电路等价验证的研究。时序电路的等价验证通常使用的方法都是对 有限状态机进行遍历，利用电路中的组合部分，或是展开成时问帧的形式加以验证， 或是利片j 结构中的耗f 似性j t j n 定点迭代的方式进行验证，或是化作布尔表达式，h 可满 足性问题的算法进行验证。本文的算法将时序电路的时序行为川状态转换图的形式米 表示，对待验证电路的状态转化幽进行同构验证，从而验证两电路是否等价。丰要的 创新处在于：( 1 ) 不依赖于电路结构的相似性，可以验证结构不同。寄存器数n 不同 的电路；( 2 ) 采用图的方式表示时序电路的行为，而不依赖于状态编码或者是布尔表 达式；( 3 ) 速度优于传统的基于b d d 的状态遍历法以及结构不动点法。 第二部分是f p g a 中电路等价验证的研究。针对f p g a 流程的t 艺映射流程、和装 箱流程展开验证。对于经过t 艺映射的由l u t ( 1 0 0 ku pt a b l e ) 组成的电路和原始的 g a t el e v e l 的电路进行等价验证，以及对于经过装箱的由c l u s t e r 组成的电路和l u t 组 成的电路进行等价验证。采用寄存器匹配的方法将时序电路转化为组合电路后，j h c s a t 算法进行验证。 关键词：时序电路的等价验证、状态转换图、f p g a 摘要 a b s t r a c t w i t ht h ec h i pc o m p l e x i t yc o n s t a n t l yi n c r e a s i n g t h ed i f f i c u l t ya sw e l la st h ei m p o r t a n c e o ff u n c t i o n a lv e r i f i c a t i o nh a sb e e ni n c r e a s e d ，t h ev e r i f i c a t i o np r o b l e mc a nn o tb es a t i s f i e d b yt r a d i t i o n a is i m u l a t i o n b a s e dv e r i f i c a t i o nm e t h o d ，f o r m a iv e r i f i c a t i o nm e t h o da st h e c o m p l e m e n tt ot h et r a d i t i o n a lm e t h o db e c o m e st h eh o t s p o ti nr e c e n tr e s e a r c h e q u i v a l e n c e c h e c k i n g c a nb ed i v i d e di n t ot w od i r e c t i o n s ：c o m b i n a t i o n a le q u i v a l e n c ec h e c k i n ga n d s e q u e n t i a le q u i v a l e n c ec h e c k i n g t h ec o m b i n a t i o n a lp r o b l e mh a sa l r e a d yb e e ns o l v e d p e r f e c t l y , s os o m ec o m b i n a t i o n a ia l g o r i t h m sh a v eb e c o m et h eb a s e o ft h es e q u e n t i a l a l g o r i t h m m yr e s e a r c hf o c u s e so ns e q u e n t i a le q u i v a l e n c ec h e c k i n g ，a n dt h i sp a p e ri s c o m p o s e do f t w op a r t s ： t h ef i r s tp a r ti st h er e s e a r c ho nt h es t a t et r a n s f e rg r a p hb a s e ds e q u e n t i a le q u i v a l e n c e c h e c k i n g t h et r a d i t i o n a ls e q u e n t i a le q u i v a l e n c ec h e c k i n gm e t h o d su s e st h ec o m b i n a t i o n a l p a r tt ot r o v e lt h es t a t es p a c e ，l i k e ，e x p a n d i n gt h ec i r c u i ta st i m ef r a m e st od ot h ev e r i f i c a t i o n o ru s i n gt h ef i x e dp o i n ti t e r a t i v e l yt od ot h ev e r i f i c a t i o nb a s e do nt h es t r u c t u r es i m i l a r i t i e s , o rt u r nt h ec i r c u i t si n t ob o o l e a ne x p r e s s i o n su s i n gt h es a t i s f i a b i l i t ya l g o r i t h ma se n g i n ei n t o t h ev e r i f i c a t i o n t h i sp a p e ru s e st h es t a t et r a n s f e rg r a p ht or e p r e s e n t st h eb e h a v i o ro f s e q u e n t i a l c i r c u i t s t h es t a t ew a r t s f e rg r a p h s i s o m o r p h i s mi sc h e c k e dt os e et l l e c o r r e s p o n d i n gc i r c u i t s e q u i v a l e n c e i ft h et w os t a t et r a n s f e rg r a p h sa r ci s o m o r p h i c t h e s t a t e si nt w od i f f e r e n tg r a p h sc a nb em a t c h e da se q u a ls t a t ep a i r s t h ea l g o r i t h mp r e s e n t e d s t o r e st h es t a t et r a n s f e rg r a p ha ss t a t ep a i r s i fa l it h es t a t ep a i r ss t o r e da r ec h e c k e dt ob e e q u a l ，t h et w oc i r c u i t sh a v et h es a m es e q u e n t i a lb e h a v i o r t h em a i nc o n t r i b u t i o n sa r e ( 1 1 c a nb ea p p l yt ot h ec i r c u i t sw h i c hh a v ed i f f e r e n tn u m b e r so fl a t c h e s ；( 2 1d o e s n td e p e n do n s t r u c t u r es i m i l a r i t i e s ；( 3 ) h a sap r o m i s i n ge l a p s e dt i m ec o m p a r i n gt ot h ea l g o r i t h mb a s e do n b d da n df l a m ee x p a n s i o n t h es e c o n dp a r ti st h er e s e a r c ho nf p g av e r i f i c a t i o n t h ep r o g r a mv e r i f i e st h em a p p i n g p r o c e s sa n dt h ep a c k i n gp r o c e s so ft h ef p g af l o w t h og a t e _ l e v e ln e t l i s ti sm a p p e di n t o l u t ( 1 0 0 ku pt a b l e ) n e t l i s t , a n dt h el u tn e t l i s ti sp a c k e da sc l u s t e rn e t l i s t o u rp r o g r a m v e r i f i e sw h e t h e rt h eg a t ei1 u t _ e v e n e t l i s tt h eln e t l i s ta n dt h ec l u s t e rn e t l i s th a v et h es a m e b e h a v i o r t _ l l el a t c h m a p p i n ga l g o r i t h m i su s e dt o c h a n g et h es e q u e n t i a lc i r c u i t s i n t o c o m b i n a t i o n a jc i r c u i t s a n dt h e nt h ec o m b i n a t i o n a lc i r c u i t sa r ev e r i f i e db yc s a ta l g o r i t h m k e y w o r d ：s e q u e n t i a le q u i v a l e n c ec h e c k i n g ，s t a t et r a n s f e rg r a p h ，f p g a n 论文独创性声明 本论文是我个人在导师指导下进行的研究工作及取得的研究成果。论文中除 了特别加以标注和致谢的地方外，不包含其他人或其它机构已经发表或撰写过的 研究成果。其他同志对本研究的启发和所做的贡献均已在论文中作了明确的声明 并表示了谢意。 作者签名 论文使用授权声明 日期：1 2 ：! j 本人完全了解复旦大学有关保留、使用学位论文的规定，即：学校有权保留 送交论文的复印件，允许论文被查阅和借阅；学校可以公布论文的全部或部分内 容，可以采用影印、缩印或其它复制手段保存论文。保密的论文在解密后遵守此 规定。 作者签名：导师签名： 该教b 日期：1 2 ! ：! ! 第一章绍论 第一章绪论 1 1 集成电路的发展与设计验证 从1 9 4 7 年第个晶体管在贝尔实验室诞牛至今已有6 0 年。在这6 0 年一i i ，科技 日新月异，从只有几个晶体管的芯片到现在，随着深业微米技术的出现，集成电路的 规模已进入巨大规模集成阶段。根据摩尔定律，到2 0 0 9 年，每颗芯片上的晶体管数 将达到3 5 亿之多。 一方面晶体管尺寸的迅速减小快速提高了集成电路芯片的集成度。目前世界集成 电路生产的主流技术是9 0 n m ，正在向6 5 r i m 甚至4 5 n m 过渡。集成电路的技术进步将 继续遵循摩尔定律，每1 8 个月集成度提高倍，成本降低一半。摹于量子效廊的电 子器件、量子集成电路、量子计算机等，也正成为人们研究的热点，它们将带来更高 豹集成度。 另一方面，电路包含的功能也越来越多。从原先单一的数字功能到现在的数模混 合芯片，芯片的功能是越来越复杂。一块典型的片上系统芯片( s o c ) 中会包含有嵌 入式的c p u 、数字控制逻辑、存储器，模数数模转换器、射频电路等等。 随着电路规模的增大，电路功能复杂度的增加，电路性能要求的提高电路设计 中可能产牛错误的概率就大了。根据i n t e l 的报告。电路设计中的错误数n 是呈指数增 长的。由此可见，电路功能验证的重要性日益增加了。实际设计项口 ：i 的经验也证明 了这。点，在设计过程中，有一半的设计资源以及8 0 的时间是花费在电路的功能验 证中的。而国际半导体技术路线图组织( i t r s ，i n t e r n a t i o n a lt e c h n o l o g yr o a d m a pf o r s e m i c o n d u c t o r s ) 早在2 0 0 4 年对半导体产业的各项技术作预测时，就在v l s i 设计报 告中将设计验证作为影响设计的重要部分 i t r s 0 4 】。 1 2 本文的研究背景与内容 本文的研究针对电路的功能验证展开。功能验证的方法有三种：基于模拟的验证、 硬件仿真以及形式验证方法，如豳1 1 所示。 当前工业界普遍使_ h j 的验证方法是基于模拟的验证方法。需要不断的对电路建 模，然后根据不同的模型设计不同的测试向量去寻找设计错误。对于不同的电路需要 技术人员设计不同的具体的验证流程、建立不同的模型以及分析验证方案中模拟的覆 盖率。然而，这种验证方法缺点很多，一是验证的不完备性，模拟覆盖率对于大规模 的电路不可能达到百分之百；二是验证中需要耗费大量的时间，无形中提高产品的成 第一亭绍硷 本。硬件仿真的技术利川现场可编程门阵列( f p g a ) 芯片，将电路下找到芯片i 对 芯片的功能进行测试以达到对电路功能进行验证的几的。这利方法的优势在十验证时 间短，速度快；缺点就是成本高。 形式验证方法提出了种具有完备住的，成本低的解决方案，它形式化的证明 个设计的实现满足其规范，川来保证功能设计的质量和正确性。在过去的几i 年- l ， 人们提出了三类形式化的验证方法：等价性验证、模型验证和定理证明。等价性验证 川于验证两个结构化的描述等价，模型检测川于验证设计属性被满足，定理证明则是 一种数学验证方法，将验证问题川公理或形式理论描述，进行推理验证。本文的研究 集i ，在等价性验证上，验证经过某利改动或优化过的电路和原来的电路在逻辑功能是 否完全等价 圈1 1 功能验证的不同方法 由于在电路的设计过程，i 采川了层次性的设计方法，即从电路的规格描述到最后 的版图牛成，电路被分成了不同的抽象层次，每个抽象层次对系统的描述方式都不同。 如图i 一2 所示。首先，根据设计描述先将电路描述为行为级模式，对此进行结构综 合，转化为寄存器传输级的描述。寄存器传输级描述将电路描述为数据线和控制单元。 寄存器传输级的描述在进行逻辑综合之后，转化为门级的电路网表，最后步物理设 计将门级网表用器件实现。于是对于不同的描述层次。我们也就需要不同的验证方式。 一般来说，抽象层次越高，验证越困难。现在物理版图级的验证都已有非常成熟的工 具。而到门级的验证，技术就没有那么成熟，目前现有的针对门级的验证下具也主要 是针对组合电路的，例如f o r m a l i t y 。对于时序电路，目前还没有成熟的算法。本文的 研究工作重点就放在研究一种时序电路的验证算法，可以对进行大幅度优化前后的电 路进行验证。 在当前t 业界激烈的竞争。 i 为了降低产品的成本，缩短产d 6 的上市时问，并且有 功能可变性，获得了越来越广泛的应j 1 j o个电子系统在可编程逻辑器件上进行实现 需要对硬件资源进行合理的配置，正确的配置信息是由可编程逻辑器件配套的软件系 第一亭绪沦 统根据川户的设计输入来实现的。那么由于在对f p g a i 的硬件资源进行配置的时候 有人t 干预，我们就要对得到的配置信息进行验证，看映射到f p g at i ，的电路是否与 映射之前的电路功能等价。 图1 2 数字集成电路的层次化设计 这就是本文的另一个研究重点，时序电路的等价验证在f p g a 电路验证i f 的应用。 1 3 国内外的研究进展 针对时序电路的等价验证，国内外已有大量的研究成果。对时序电路的验证与组 合电路的验证的最大区别就在于要对状态进行遍历，对每个状态下的电路功能以及状 态之问的转换关系进行验证。时序电路的验证可以看作是在每一个特定状态之下，对 代表该状态的电路功能的组合逻辑迸行验证的过程。组合电路的验证现有的比较快的 算法都离不开对电路节点的逻辑函数的计算。从状态遍历的方式来区分，主要有以下 两种方法，它们采闩j 的计算逻辑函数的方法也有所不同： ( 1 ) 基于结构推理的方法 这种方法利用时序电路的内部结点函数之间的逻辑关系来隐含的表示可达状态。 用逻辑关系的变化来表示状态之阅豹转换关系。这类方法利用结构相似性豹功能蕴涵 来简化验证问题，可以验证规模较大的时序电路，但是只是在待验证的电路结构仍保 持大部分相似性的情况下才可n 现这类方法的优势。这类方法识别潜在结构相似性的 常川方法有随机模拟、a t p g 方法以及基于可满足性问题解决器( s a t i s f i a b l i t yp r o b l e m s o l v e r ) 的推理方法。例如 d s t 0 9 7 rj r b u 9 8 都是属于这类方法。 第一亭绢论 ( 2 ) 皋十有限状态遍历的方法 这类方法通常是直接计算出电路所有的可达状态。冉验证在此可达状态下，待验 证的电路是否功能等价。这类方法建立的模型比较简睁，往证明小规模电路的时候速 度较快，t 开是非常耗费内存。此类方法大部分都是笨于r o b d d ( r e d u c e d o r d e r e d b i n a r yd e c i s i o nd i a g r a m ) 的方法。摹于r o b d d 这类验证方法将待验证的两个电路的逻 辑函数表示成两个范式，然后按照相同的输入变量序分别构造这两个输入函数的 r o b d d ，判断它们是否同构。这种方法占取内存空问大，容易造成内存爆炸。例如 j j t 0 9 0 就是利 u b d d 对状态空问进行遍历的。 对于状态编码柏同的时序电路可以采川匹配触发器的算法【b u j r 9 8 】，将时序电路 转换称为组合电路来验证。在后面对f p g a 的验证一i 我们就采川了这种方法。转换的 组合电路的验证已有成熟的算法。我们可以将组合电路农示为逻辑函数进行运算。几 前有两种方法可以进行运： ( 1 ) 有序二分决策图r o b d d ( r e d u c e do r d e r e db i n a r yd e c i s i o nd i a g r a m ) 为了验证两个电路的相应初始输出是等价的，必须按照相同的输入变量序分别构造 这两个输出函数的r o b d d ，然后判断它们是否同构。这种方法输入变量排序非常敏 感，常遇到内存爆炸的问题。 ( 2 ) 可满足问题解决器( s a t i s f i a b i l i t yp r o b l e ms o l v e r ) 将两待验证电路用特定格式的布尔函数表示，解决器判断是否可以找出组赋值可 以使表达式的值为真。速度快，占内存相对较少。后面我们对组合电路进行的验证采 刖的是s a t 解决器的变形c s a l 。 1 4 本文的主要贡献 本文的丰要贡献在两方面，+ 。部分是时序电路的等价验证算法的研究，另部分 是时序电路的验证在f p g a 上的应用。 第一部分时序电路的等价验证算法采用的是基于状态转换图的算法，提出一种基 于状态转换图的时序电路等价验证算法。算法通过验证两时序电路的状态转换图是否 同构，得到两电路是否等价的信息。若两状态转换图同构，则两图中的状态可一一匹 配为等价状态对，本算法将状态转换图存储为待验证等价状态对的形式，若所有待验 证等价状态对均为等价，则两时序电路等价，反之，则不等价。本文算法对i s c a s 8 9 测试电路进行验证，与基于b d d 方法的s i s 系统和基于对阔帧展开算法相比，均有较 好的结果。 第二部分是时序电路验证在f p g a 上的廊州。本文对f p g a 的硬件资源配置的主 要流程的配置信息进行验证。丰要分为三个部分：丁二艺映射部分，装箱部分和布局布 线的部分。工艺映射得到的配置信息是电路的查找表l u t ( 1 0 0 ku pt a b l e ) 形式的逻辑网 第一奄绪论 农，于是我们将之前门级网农和此时的l u t 逻辑网农进行功能验证：装箱得到的配置 信息是电路的c l u s t e r 的形式网表，将此网表与l u t 网衷进行功能验证。该验证t 具完全使川本实验窜研究现有的算法米实现，验证速度与美国加利福尼q f 大学伯克莱 开发的软件m v s i s 相、。 1 5 论文的组织结构 本文第章为绪论，介绍时序电路的等价验证在国内外的研究进展和自己丁作 的贡献；第二章介绍电路模型和状态遍历；第三章介绍已有的国内外的等价验证算法； 第四章介绍我们提出的笨于状态转换图的时序电路的等价验证算法，同时给出实验结 果；第五章介绍对f p g a 提出并实现的验证t 具。并给出实验结果；第六章为总结。 第：诱时序电路等价骑讦的丛木问题和概念 第二章时序电路等价验证的基本问题和概念 2 1 引言 本章介绍在后面验证算法中会涉及到的重要的概念。首先在2 2 节q - 介绍时序电路 等价验证要解决的基本问题以及它涉及到的时序电路的基本概念；接着，在2 3 节巾 我们以方便验证，简化问题为口的，对电路建模，并介绍摹本的验证模型。在2 4 节 中介绍时序电路等价验证最摹本的手段，状态空闯的遍历以及不同的遍历方法。最后 在2 5 节中会给出在状态遍历巾会涉及到的布尔代数和有序二分决策图的简单介绍。 那么，我们先介绍时序电路等价验证的基本f j 题。 2 2 时序电路等价验证的基本问题 由于现在集成电路的规模不断的增大，在设计过程中都采用层次化设计方法。在不 同层次的设计过程q ，电路会被描述成不同层次的逻辑，同层次的逻辑也会根据电路 性能的要求经过不同的优化。不同层次的逻辑之间的转换，逻辑优化的过程都可能会 引入错误，那么我们就要对经过优化的电路网表进行功能验证，看优化前后的电路网 表是否具有相同的电路功能。 电路的功能验证指验证两个电路逻辑描述的是否是相同的电路功能，等价验证是 它的一种。对于不同的电路，等价验证的方法也不同。根据电路是否具有记忆功能， 我们可将电路分为组合逻辑电路和时序逻辑电路，将等价验证的方法分为组合电路的 等价验证和时序电路的等价验证。 定义l 组合逻辑电路：输出只与当前的输入有关，不具有记忆功能的电路称为组 合逻辑电路，简称组合电路。图2 - - i 是组合电路的基本结构。其中，x = ，t ，k ) 代表输入序列，y = ，儿，以) 代表输出序列。中间的部分就是决定输入输出关系的 组合逻辑。 x l x 2 x n 组合逻辑 y 1 y 2 y n 图2 1 组合电路的基本结构 定义2 时序逻辑电路：具有记忆功能，输出不仅与当前的输入有关，还取决于之 6 第：簪时序电路等价骑“的丛本问题和概念 前的输入值的电路称为时序逻辑电路，简称时序电路。刳2 2 是时序电路的基本结 构。 y i y 2 y m 警l 亨2 gk 圈2 2 时序电路的基本结构 时序电路t i ，有由时钟控制的记忆单死触发器。根据触发器是否由同。时钟控制，时 序电路可分为同步时序电路和异步时序电路。本文的验证算法都是针对同步时序电路 的。 组合电路的等价验证就是验证在所有可能的输入下，输出是否都相同。通常是将电 路抽象成为布尔函数，再对布尔函数进行处理比较。通常使用的对布尔函数进行计算 的方法有两种，一种是二分决策图b d d ，另一。种是可满足住问题解决器s a t - s o l v e r 。 在后面的对f p g a 进行的验证过程中，会涉及到利用s a t 对组合电路进行验证的相关 算法。 而时序电路的等价验证则是在记忆单元形成的每一个状态下，验证对于所有的输入 序列，输出是否相同。可以看出，时序电路的等价验证实际上是在每一个状态下，进 行组合逻辑的等价验证。那么，如果我们可以将两待验证时序电路中表示状态的触发 器匹配起来，就可以将时序电路的验证转化为两组合电路的验证。在f p g a 等价验证 中，我们正是用的这种算法处理时序电路等价验证的。在第三章1 j 会介绍前人关于这 方面已有的研究成果，然后在第五章中会看到这种算法的具体应用。 对于时序电路来说，在不同的状态下，输入输出之间的逻辑关系也不同。那么如果 采用布尔函数的方法对时序电路进行等价验证，就要对不同状态下的组合逻辑计算布 尔函数。某些算法利用不同状态下逻辑的结构相似性解决验证问题，某些算法则利用 待验证两电路状态变量之间的关联性解决验证问题。这些验证算法都会在第三章。 介绍。 “也孙甜鸵敝 第：币时序电路等价骑i f 的丛木阿题和概念 2 3 时序电路等价验证的电路模型 这里我们介绍在后面的算法研究- i - 会常常涉及到的些摹本的在时序电路的等价 验证q - 会j l 】到的电路模型以及电路验证模型。 本文研究的时序电路指的是触发嚣由网外部对钏，控制，所有的触发器会在同r 时刻翻转的同步时序电路。同步时序电路的状态在两次时钊- 沿触发问隔期问保持不 变，所以将两次时钟沿触发问隔时问作为时序电路的定时单位，把某个问隔时刻称为 “当前时刻”，将下个问隔时刻称为“下。时亥”。触发嚣的输出逻辑组合被称为时 序电路的状态。在当前时刻电路的状态被称为“当前状态”，下时刻电路的状态被 称为“下一状态”。图2 2 中的时序电路表示。个具有n 个输入，m 个输出，k 个记忆 单元的时序电路。时序电路通常建模为有限状态机f s m ( f i n i t es t a t em a c h i n e ) 。 定义3 有限状态机：有限状态机_ i j 一个六元组m - - ( i , s ，玩无d s o ) 来表示时序电 路，其中i 农示输入集合， o ，矿，刀n ，n 表示电路输入的个数；s 表示状态集合， s 0 ，l n q n ，其- i tq 是状态变量的个数： j 表示传输函数；五表示输出函数；o 表示输出集合，o o l ”，棚e n ，m 是电路输出的个数；s o 表示初始状态集合。 其中传输函数和输出函数分别代表了状态转换与输入之间的逻辑关系以及输出与 状态之间的逻辑关系，具体定义如下。 定义4 传输函数：在某状态下，给出一个输入激励i ，状态翻转，得到下一一状态。 描述这个状态之间的转换关系的函数称为传输函数。它可以描述为j ：s x i 专s 。 定义5 输出函数：描述在当前状态下，输出的逻辑函数的函数称为输出函数。它 可以描述为五：s 专o 。 那么验证两个时序电路是否等价就可以抽象成为验证两个有限状态机是否等价， 为了方便验证，我们将两个待验证状态机转换成为乘积电路( p r o d u c tm a c h i n e ) 。 定义6 乘积电路：将待验证两电路相应的输入端口连接起来，相应的输出端口用 异或门连接起米。此时的输入端对两电路同时输入相同的向量，异或门的输出则表明 了相同输出端口的值是否相同。将所有异或门的输出端作为个或门的输入，而这个 或门的输出则成为整个电路的初始输出端口。这样形成的新电路称为乘积电路。如图 2 - 3 所示。 可以看出要证明电路a 、b 是否等价，只要直到是否有一组输入可以使乘积电路的 输出为1 即可。在后面利用s a t 对电路进行验证的算法都会利用到这个验证模型。将 验证两电路是否等价的问题转化为是否能找到一组赋值使。个布尔函数值为l 的问 题。 通常的时序电路等价验证方法是通过对电路的可达状态空间进行遍历来实现的， 即遍历有限状态机中的集合s ，现在我们有了乘积电路这个概念，那么验证两时序电 第一帝时序电路等价验仆的基本问题和概念 路的等价就要对它们的乘移 电路进行可达状态空间遍历。对于状态编码相同的待验证 电路，可达状态空问相同，于是可以将时序电路“1 作组合电路米验证。相关算法会在 第三章t i 给出。下面我们先介绍对可达状态空问的定义，以及时它遍历的方法。 图2 3 乘积电路的结构图 2 4 可达状态空间的遍历 在时序电路等价验证的摹本问题- f t 我们提到，时序电路的等价验证就是在每个 状态下进行组合逻辑的验证。其实，并不是所有的状态都会在电路的实际工作中出现 的。于是，我们就有了可达状态这个概念。 定义7 可达状态：在时序电路中，由电路给出的初始状态开始，根据电路的传输 函数，触发器变量随着输入激励变化而变化，产生的所有的触发器变量的取值组合称 为电路在某初始状态下的可达状态。 定义8 不可达状态：同理，由初始状态开始，根据电路的传输函数，无法取得的 触发器变量的取值组合称为在某初始状态下的不可达状态。可达状态集合和不可达状 态集合的并集就是整个状态空间。 根据传输函数，我们可以得到由某初始状态起的可达状态空间。这个可达状态 空间就描述了该电路的时序行为。状态之间的转换关系可以用状态转换图来表示，这 也是对时序电路的另利建模方法。 定义9 状态转换图：对于给定有限状态机m ，定义有向边标记的幽为该有限状态 机的状态转换图g = 暇e l a b e l ) 。其中s 表示有限状态机的状态集合，在图g 中表示 为图的顶点，一个顶点代表某一个状态；e 表示状态之间的转换关系，在图g 中表示 为有向边e e ，一个有向边表示在其起始点表示的可达状态s 下通过某一输入激励 ，i ，有限状态杌到达其终点所表示的可达状态t 。有向边上用l a b e l 标记状态转换的 条件及输出y e 0 ，格式为l a b e l 0 ) ；w 1 ) ，。标记l a b e l 同时表示了传输函数占0 ，w ) = f 和 输出函数a ( s 。w ) = y 的意义。 图2 4 是状态转换图的一个示例，简单起见没有对状态编码。根据可达状态的定 义我们可以看出，若以瓯为初始状态求得的可达状态空间应该是 瓯，s ，最，岛 ，由于 从& 任何一4 组输入向量都不会使状态翻转至墨，所以此时墨为不可达状态。若以墨为 9 第：亭时序电路等价验计的丛小问题和概念 初始状态，可以看到幽- l 一所有的状态都是可达状态，可达状态空问与状态空问相等， 可达状态空问为 s o ，s ，是，s ，墨) 。 图2 4 状态转换图示例 对时序电路的验证离不开对状态空间的遍历。遍历状态空问算法的效率直接影响 到整个验证算法的效率。这坐介绍几利懒本的遍历状态空间的算法，不同的分类方法 着眼点不同。若是根据是对可达状态空问进行遍历还是不可达状态空问进行遍历，可 以分为前向可达状态遍历和反向状态遍历两种方法。若是根据状态遍历的结果，则可 以分为确切可达状态遍历和大约可达状态遍历。下面我们将分别介绍这两种类别的算 法。 2 4 1 前向可达状态遍历和反向可达状态遍历 前向可达状态遍历的思想就是，从初始状态集合出发，不断通过传输函数计算当 前状态下能够到达的下一个状态，直到遍历完毕整个可达状态空间。验证在每一个状 态下乘积电路的输出值，看电路是否等价。通常使用的是广度优先的遍历方法。设有 初始状态& ，置代表状态集合，表示在第i 次迭代计算得到的当前所有可达状态的集 合。于是有初始状态集合r = s o ) 。在每一次根据传输函数进行的迭代运算之后，可 达状态集合叶i 的状态数目都会增加，直到某一次迭代运算之后，可达状态数日不会再 增加，即在某第k 次迭代后，有r = r 卅 表明可达状态空间已被完全遍历。广度优 先遍历的计算就是将现有状态集合中当前状态的所有下一状态全部计算出来。对于圈 2 - - 4 而言，k = 2 。日= s o ，s i ，是) ，r = s o ，s ，是，墨) 反向状态遍历同前向状态遍历不同的是，它的初始集合是所有使电路输出不相等 的状态集合。然后从这个集合出发，反向运用传输函数计算“前一个”状态集合。判 断集合内是否包含初始状态。如果包含，则表明使电路输出不相等的状态是可达状态， 因此电路是不等价的。反之，则表明所有使电路不等价的状态都是不可达状态，电路 等价。若图2 - - 4 是一个乘积电路的状态转换图，其初始状态为最，那么初始集合就 是r = 饯，s ) 。从这个集合出发，经过步迭代就可以到达初始状态。那么此乘积电 路所代表的两个待验证电路不等价。 1 0 第：帝时序电路等价验证的丛水问题和概念 显然，前向和反向算法是瓦补的算法，个计算的是可达状态空问，个计算的 是不可达状态空问。算法的效率对于不同的具体的实例也不同，要看实例的可达状态 空间大还是不可达状态空问大。本文采川的是前向可达状态遍历的方法。 2 4 。2 确切可达状态遍历和大约可达状态遍历 确切可达状态遍历的思想与前向可达状态遍历的思想柏同，都是从初始状态集合 触发确切的计算出每个可达状态。 大约可达状态遍历【g s g 0 9 8 】【h c h 0 9 6 】的提出是由于电路规模的不断增加使得对 有限状态机状态的遍历越来越困难，于是就提出将。个大的有限状态机分割成几个规 模大小适中的有限状态机进行状态遍历，最后再将状态汇合起来。由于在将有限状态 机分割的时候不可避免的减弱了被分割成的小规模的有限状态机之间的约束，那么这 样做的代价就是使这个可达状态集合不那么精确，也就是说求得的状态集合中存在不 可达状态。这样导致的问题就是，使用这个不精确的状态集合进行验证，验证结果不 一定准确。如果验证结果是两电路等价，那么既然在相对弱的约束条件下两电路都是 等价的，加强约束即将状态集合精确到可达状态集合后，辑电路应该仍然是等价的， 即若验证结果等价则两电路等价；反过来，如果验证结果是两电路不等价，那么我们 并不能判断不等价因素是由可达状态引入的还是由不可达状态引入的，于是此时我们 不能判断两电路是否等价，即若验证结果不等价贼不能翔断两电路是否等价。 大约状态遍历的方法实际上是在精确度和效率之间做了一个平衡。相关算法都在寻 找- t e l , 可以往短时间内计算出最贴近可达状态空问的方法。也就是尽量减少冗余的不 可达状态的加入。大部分的算法采取的都是将状态变量分别计算，减弱状态变量之问 的约束关系，再适当加入补充变量重新加大对状态变量的约束，减少不可达状态出现 的方法。同时，将有限状态机分割的算法也很重要，如果被分割成的小规模有限状态 机之间的约束本来在原有的有限状态机内时的约束就较弱，那么它后续引入的不可达 状态就越少；反之，引入的不可达状态越多，就会使得后面验证的结果精确度很低。 对于本文的工作来说，是希望完成一种算法可以明确的给出两电路是否等价的结 果的，所以本文采用的是确切可达状态遍历的方法。无论是哪种状态遍历的方法都会 涉及到对状态传输函数的求解，由于状态传输函数也是布尔函数，那我们先简单介绍 一下利- 皋本的处理布尔函数的引擎r o b d d 。 2 5r o b d d 的相关基本概念 在实际的验证工作中有不同的方法来表达一个布尔函数。根据表达方式可以将表 达式分为划范性( c a n o n i c a l ) 和非规范性( n o n - c a n o n i c a l ) 。二分决策剧( b d d , b i n a r y 第 市h f 序电路等价骑i 的丛木问题和概念 d e c i s i o nd i a g r a m ) 【r e b r 8 6 】f s a k e 7 8 在定的约束条件下就是布尔函数规范性的表 达方式。b d d 根据变量排序可以分成很多种，在这里我们对时序电路等价验证t i 最 常川到的有序二分决策幽r o b d d ( r e d u c e do r d e r e db d d ) 幽r e b r 9 5 进行介绍，它 是具有统变量排序基于香农( s h a n n o n ) 分解的b d d 图。其余类型的b d di 整i 具有 与它类似的对衣尔逻辑操作的支持，区别只是对不同类型的布尔函数的农示时b d d 图的大小不同。 定义1 0 二分决策图b d d ( b i n a r yd e c i s i o nd i a g r a m ) ：对于表达式以的二分决策 图是一个具有一个根缔点的有向不循环图g = ( 矿，e ，i r l d e x , v a l u e ) ，其i i 的结点v 包含 两种类型的结点：内部结点和终止结点。内部结点v 含有一个类似标铝的变量 i n d e x ( v ) 以和两个子结点，d w ( v ) ，h i g h ( v ) v 。终止结点j i j 个布尔常量 v a l u e ( v ) o 1 标记，而且没有向外输出的边。 定义1 1 有序二分决策图r o b d d ( r e d u c e do r d e r e db i n a r yd e c i s i o nd i a g r a m ) ： 我们称个二分决策图是有序的，如果对图l f l 任意的边e d g e ( u ，v ) e ，都存在某r 。线 性的顺序 是两个有向图，若在矿与v 之间存在双射函数g ，使得昱与对一切阮p v ，帮，v ，若 e ，则必有 e ，且在各自的图中有相同的重数；若 舞e ，则 仨e ，那么我 们称图g 与g 同构。 在算法中我们试图将状态转换图的状态一一匹配起来。任两个状态都可称为状态 对，但是在算法中我们寻找的状态对是符合定条件的待验证状态对： 定义1 3 待验证状态对：设岛和8 2 分别是待验证电路m 和m ：的状态，若它们在 第网亭丛f 状奎转换幽的时序电路等价验“算江 相同的输入序列下的输出序列相等，则称s l 和s 2 是待验证状态对。 例如在例4 一i l i ，电路( a ) 状态转换幽- l - 的0 0 0 状态与电路( b ) 状态转换幽，l - 的0 0 0 状态，它们在输入l 下输出均为0 ，输入0 下输出均为1 ，那么称0 0 0 和0 0 0 为待验证状态对。 ( i ) 状态转换图a ( i i ) 状态转换图b 图4 1 状态转换图示侧 定义1 4 下一状态对：设丑和s ，分别是待验证电路m 和m ，的待验证状态对，它 们在柏同的输入下的下状态分别是s 3 和甄，则称s 3 和s 4 是 和5 2 的下状态对。 同理，我们也就有了上一状态对的概念，若此时屯和毛是待验证状态对，则我们 称& 和j ，是s 3 和的上一状态对。 待验证状态对符合一定条件后，我们可以判断其为等价状态对： 定义1 5 等价状态对：设s 。和岛分别是待验证电路m 和鸩中的状态，当且仅当 对于所有的输入序列，丑和s ，的输出序列均相等，并且下一状态对也为等价状态对时， 最和岛可称作为等价状态对。 根据定义1 5 ，我们知道若两状态为等价状态对，那么它们的下一状态对应该也是 等价状态对。于是若两待验证电路的初始状态对是等价状态对，那么由此初始状态对 可达的状态对应该都是等价状态对，那么这两个待验证电路等价。由此，我们得到推 论： 推论时序电路的等价：设s ? 和5 ：分别是两个待验证电路m 和m ：的初始状态，那 么当且仪当j ? 和霹是等价状态对时，两待验证电路等价。 4 3 基于状态转换图的时序电路等价验证的算法思想 根据上述推论，从初始状态开始对电路的状态转换图进行验证。本文算法先只考 虑待验证的电路给出初始状态集合的情况，即先将两个初始状态集合中的初始状态- 一 第四章丛十状态转换幽的时序电路等价验h f 饽江 匹配起米，形成。个初始状态对集合，然后对每个初始状态埘所形成的可达状态 空问验证。 已知电路的初始状态，时序电路的时序行为就可以川由在该初始状态下的可达状 态组成的状态转换图来表示。若在一个状态转换幽i ，任取。个顶点都可以在另。个状 态转换魁i | | 找到等价的顶点，那么根据两个有向图同构的定义1 2 ，我们可以称这两个 时序电路所对应的状态转换图同构，也就是说这两个状态圈代表的电路等价。而在两 个状态幽r l 等价的两个顶点根据定义1 5 就是等价状态对 s y h u 9 8 1 。根据这个有向幽 同构的思想我们就有了本文的算法思想。试幽将两电路的状态转换图的状态匹配 起米，形成待验证状态对，并通过验证待验证状态对是否是等价对来验证电路是否等 价。 在将时序电路转化为状态转换图之后，我们先要将两个状态转换圈化简为最简形 式。若两待验证电路等价，那么这两个电路所对应的最简的状态转换豳必然状态数相 等，状态转换关系数也相等。而且两个卧f i 的状态和状态转换关系均能匹配。那 么若对状态转换幽不进行简化，会出现多个状态和同。个状态匹配的情况，如果待验 证电路是等价的，则这多个状态必然可化简为。个状态。所以本文算法先验证这与同 一个状态匹配的多个状态是否是同一个状态，若是，则再将其与另一个状态图巾的状 态匹配为待验证