（计算机应用技术专业论文）基于有限环上多项式的数字电路形式验证方法.pdf

基于有限环上多项式的数字电路形式验证方法 摘要 随着集成电路的规模变得越来越大、功能越来越复杂，功能验证已经成为 设计流程的主要瓶颈。据统计，设计验证的时间已占到整个设计周期的一半以 上。传统的基于模拟的验证方法不但需要花费大量的时间，而且不能保证完全 的验证覆盖率，己经不能满足现时集成电路设计的要求。形式验证利用数学的 方法隐式遍历所有可能的情况，能保证完全的验证覆盖率，所需要的验证时间 也大幅减少，是克服验证瓶颈的可行途径。本文以有限环上多项式为基础模型， 围绕算术密集型设计( 例如数字信号处理( d s p ) 电路) 的等价性检验和定界 模型检验，进行了深入研究，取得了如下创新性成果： ( 1 ) 针对实现多项式运算的定点数据通路的逻辑门级与寄存器传输级 ( r 1 1 l ) 之间的等价性检验，提出一种将定点数据通路的位级描述抽象为字级 描述的方法。首先采用算术转换描述定点数据通路的逻辑门级功能，采用多项 式函数描述定点数据通路的r t l 功能，然后采用牛顿插值方法迭代地将算术转 换抽象为多项式函数，以实现定点数据通路的逻辑门级模型与r t l 模型之间的 等价性检验。实验结果表明，该方法的速度与已有方法相比对乘法器的验证平 均要快1 至2 倍，对一些实现多项式运算的定点数据通路的验证平均要快1 个 数量级。 ( 2 ) 针对定点数据通路的设计规范与r t l 实现或优化后的r t l 实现之间 的等价性检验，构建v a n i s h i n g 多项式环的理想的极小强g r ，b n e r 基，并在此基 础上提出一种高效的等价性检验算法。通过使用多项式函数建模定点数据通路 的设计规范和r t l 实现，将等价性检验问题转化为判断一个多项式函数是否为 v a n i s h i n g 多项式的问题，进而采用v a n i s h i n g 多项式环的理想的极小强g r 6 b n e r 基来有效地解决该问题。理论分析表明该算法的时间复杂度的上界比已有方法 的时间复杂度的上界小。实验结果表明，对一些实现多项式运算的定点数据通 路的等价性检验，该方法比已有方法平均要快2 倍。 ( 3 ) 针对d s p 电路的高层次设计验证的定界模型检验，提出一种基于有 限环上多项式理想的g r 6 b n e r 基的定界模型检验方法。通过使用有限环上多项 式等式建模高层次设计和待验证性质，将定界模型检验问题转化为定理证明问 哈尔滨- r 程入学博+ 学位论文 题，并采用有限环上多项式理想的g r 6 b n e r 基有效地解决该定理证明问题。实 验结果表明，与基于布尔可满足性( s 盯) 和基于线性规划的r t ls a t 的定界 模型检验方法相比，该方法对一些d s p 电路的验证平均要快1 倍到1 个数量级。 关键词：形式验证；等价性检验：定界模型检验：有限环上多项式；g r 6 b n e r 基：定点数据通路 基于有限环上多项式的数字电路形式验证方法 a b s t r a c t s i n c ei n t e g r a t e dc i r c u i t d e s i g n s a r e b e c o m i n gm o r ea n dm o r ec o m p l e x ， f u n c t i o n a lv a l i d a t i o nh a sb e e nt h em a i nb o t t l e n e c ko ft h ed e s i g nf l o w t h ed e s i g n t e a ms p e n d sm o r et h a n5 0 e f f o r to ft h e d e v e l o p m e n to n v e r i f i c a t i o n t h e t r a d i t i o n a ls i m u l a t i o nv e r i f i c a t i o nn o to n l yr e q u i r em u c ht i m e ，b u ta l s oc a n n o t g u a r a n t e e f u l lv e r i f i c a t i o n c o v e r a g e ，i n aw o r d , t h e yc a n n o t s a t i s f yt o d a y s r e q u i r e m e n ti nt h ev e r i f i c a t i o no fi n t e g r a t e dc i r c u i t s f o r m a lv e r i f i c a t i o ne n u m e r a t e s a l lp o s s i b l ec o n d i t i o n si m p l i c i t l yu s i n gm a t h e m a t i c a lm e t h o d s ，w h i c hc a ng u a r a n t e e f u l lv e r i f i c a t i o nc o v e r a g e ，i t st i m ei sr e d u c e dg r e a t l y ，t h e r e f o r ei ti saf e a s i b l ew a yt o o v e r c o m ev e r i f i c a t i o nb o t t l e n e c k b a s e do nt h et h e o r yo ff i n i t er i n gp o l y n o m i a l ，t h e m a i nf o c u so ft h i st h e s i si se q u i v a l e n c ec h e c k i n ga n db o u n d e dm o d e lc h e c k i n gf o r t h ea r i t h m e t i cd o m i n a n td e s i g n ( s u c ha st h ed i g i t a ls i g n a lp r o c e s s i n gs y s t e m ) t h ec o n t r i b u t i o n so ft h et h e s i sw e r ea sf o l l o w s ( 1 ) f o rt h ee q u i v a l e n c ec h e c k i n gb e t w e e nl o g i c a ll e v e la n dr e g i s t e rt r a n s f e r l e v e l ( r t l ) o ff i x e d p o i n td a t a p a t h s ，w h i c hi m p l e m e n tt h ep o l y n o m i a lc o m p u t a t i o n s ， a na p p r o a c ht h a tt h ew o r d l e v e ld e s c r i p t i o n sf o rt h e s ed a t a p a t h sw e r ea b s t r a c t e df r o m t h e i rb i t - l e v e ld e s c r i p t i o n sw a sp r o p o s e d f i r s t l y , a r i t h m e t i ct r a n s f o r m sw e r eu s e dt o d e s c r i b et h ef u n c t i o n so fl o g i c a lg a t e - l e v e lf o rf i x e d - p o i n td a t a p a t h s ，a n dp o l y n o m i a l f u n c t i o n sw e r eu s e dt od e s c r i b et h ef u n c t i o n so fr t l s e c o n d l y , t h en e w t o n i n t e r p o l a t i o nm e t h o dw a su s e dt oa b s t r a c tt h ea r i t h m e t i ct r a n s f o r m st op o l y n o m i a l f u n c t i o n s , a n dt h e nt h ee q u i v a l e n c ec h e c k i n gw a si m p l e m e n t e d e x p e r i m e n t a lr e s u l t s s h o w e dt h a tt h ep r o p o s e da l g o r i t h mw a so na v e r a g eo n et ot w of a c t o r sf a s t e rt h a nt h e e x i s t e n ta l g o r i t h mf o rm u l t i p l i e ra n do n em a g n i t u d ef a s t e rt h a nt h ee x i s t e n ta l g o r i t h m f o rs o m ef i x e d - p o i n td a t a p a t h s ( 2 ) f o rt h ee q u i v a l e n c ec h e c k i n g b e t w e e nt h e d e s i g ns p e c i f i c a t i o n so f f i x e d 。p o i n td a t a p a t ha n di t sr t li m p l e m e n t a t i o n so ri t so p t i m i z e dc o u n t e r p a r t ，b a s e d o nt h em i n i m a ls t r o n gg r t b n e rb a s i so ft h ei d e a lo fv a n i s h i n gp o l y n o m i a l s ，a n a l g o r i t h mo fe q u i v a l e n c ec h e c k i n gf o rf i x e d - p o i n ta r i t h m e t i cd a t a p a t h sw a sp r o p o s e d 哈尔浜- r 崔大学搏十学位论文 b ym o d e l i n gd e s i g ns p e c i f i c a t i o n sa n dr e g i s t e rt r a n s f e rl e v e li m p l e m e n t a t i o n sf o r f i x e d - p o i n td a t a p a t h sa sp o l y n o m i a lf u n c t i o n s ，t h ee q u i v a l e n c ec h e c k i n gw a sr e d u c e d t ov e r i f yw h e t h e rap o l y n o m i a lf u n c t i o ni sav a n i s h i n gp o l y n o m i a l ，w h i c hc a l lb e s o l v e db yt h em i n i m a ls t r o n gg r f b n e rb a s i so ft h ei d e a lo fv a n i s h i n gp o l y n o m i a l s e f f i c i e n t l y t h e o r e t i c a la n a l y s i s d e m o n s t r a t e dt h a tt h e u p p e r b o u n do ft i m e c o m p l e x i t yo f t h e p r o p o s e da l g o r i t h mw a sl o w e rt h a n t h ee x i s t e n t a l g o r i t h m e x p e r i m e n t a lr e s u l t ss h o w e dt h a tt h ep r o p o s e da l g o r i t h mw a st w i c ea sf a s ta st h e e x i s t e n ta l g o d t h mf o rs o m ef i x e d - p o i n td a t a p a t h s ( 3 ) f o rt h eb o u n d e dm o d e lc h e c k i n go fh i 曲一l e v e ld e s i g nv e r i f i c a t i o no f d i g i t a ls i g n a lp r o c e s s i n gc i r c u i t s ，ab o u n d e dm o d e lc h e c k i n gm e t h o du s i n gg r 6 b n e r b a s i so ff m i t er i n gp o l y n o m i a l sw a sp r o p o s e d b ym o d e l i n gh i g h l e v e ld e s i g n sa n d t a r g e t i n gp r o p e r t i e sa sf i n i t er i n gp o l y n o m i a le q u a t i o n s ，b o u n d e dm o d e lc h e c k i n g w a sr e d u c e dt ot h et a s ko ft h e o r e mp r o v i n g ，w h i c hc a l lb es o l v e db yg r 6 b n e rb a s i so f f i n i t er i n gp o l y n o m i a l se f f i c i e n t l y e x p e r i m e n t a lr e s u l t ss h o w e dt h a tt h ep r o p o s e d a p p r o a c hw a so na v e r a g eo n ef a c t o rt o o n em a g n i t u d ef a s t e rt h a nt h ep r o p e r t y c h e c k i n ga p p r o a c h e sb a s e do nb o o l e a ns a ta n dl p - b a s e dr t ls 灯f o rs o m ed s p c i r c u i t s k e y w o r d s ：f o r m a lv e r i f i c a t i o n ，e q u i v a l e n c ec h e c k i n g ，b o u n d e dm o d e lc h e c k i n g ， f i n i t er i n gp o l y n o m i a l ，g r 6 b n e rb a s i s ，f i x e d - p o i n td a t a p a t h 哈尔滨工程大学 学位论文原创性：声明 本人郑重声明：本论文的所有工作，是在导师的指导下， 由作者本人独立完成的。有关观点、方法、数据和文献的引用 已在文中指出，并与参考文献相对应。除文中己注明引用的内 容外，本论文不包含任何其他个人或集体已经公开发表的作品 成果。对本文的研究做出重要贡献的个人和集体，均已在文中 以明确方式标明。本人完全意识到本声明的法律结果由本人承 担。 日期： 作者( 签字) ：座专蹲 讪酃年i o 月一日 第1 章绪论 第1 章绪论 1 1 课题的背景及意义 自1 9 5 8 年第一块集成电路在美国德州仪器公司问世，电子工业进入了集 成电路时代。在接下来的半个世纪中，集成电路技术以惊人的速度发展起来。 从最初的小规模集成电路( s m a l ls c a l ei n t e g r a t i o n ，s s i ) ，经历了中规模集成电 路( m e d i u ms c a l ei n t e g r a t i o n ，m s i ) 、大规模集成电路( l a r g es c a l ei n t e g r a t i o n , l s i ) 、超大规模集成电路( v e r yl a r g es c a l ei n t e g r a t i o n , v 1 s i ) 、特大规模集成 电路( u l t r al a r g es c a l ei n t e g r a t i o n ，u l s i ) ，发展到目前的巨大规模集成电路 ( g i g a n t i cs c a l ei n t e g r a t i o n ，g s i ) 和片上系统( s y s t e mo nac h i p ，s o c ) 以及片 上网络( n e t w o r ko nc h i p ，n o c ) ，单个芯片集成的晶体管数目从最初的十几个 发展到目前的几亿个甚至几十亿、上百亿个。当前芯片的集成度和制造能力的 增长速度远远超过了芯片设计能力的增长速度，设计技术的发展落后于制造技 术的发展，使得集成电路的制造能力和设计能力之间有一条鸿沟。近些年来随 着电子设计自动化( e l e c t r o n i cd e s i g na u t o m a t i o n ，e d a ) 工具的发展，特别是 自动综合工具的发展，使得集成电路的设计能力有了空前的提高。数千万门的 设计规模综合工具完全能够胜任，真正制约集成电路设计能力进一步提高的 个重要因素是验证技术的相对滞后。 2 0 0 5 年度的国际半导体技术路线图( 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 p s e m i c o n d u c t o r ，i t r s ) 的报告中指出，验证已经成为集成电路设计所面临的重 大挑战之一【1j 。一方面，为了满足客户日益多样化的需求，芯片所要胜任的功 能同新月异，这就需要芯片的设计越来越复杂；另一方面，芯片设计制造商为 了获取利润最大化，必须达到早同上市的目标，这就迫使芯片的设计制造周期 尽可能的短。芯片的b 益复杂势必会给设计带来挑战，就有可能导致设计中的 错误。b e n t l e y 在2 0 0 1 年设计自动化会议( d e s i g n a u t o m a t i o nc o n f e r e n c e ，d a c ) 上报告，p e n t i u mi v 中被检测出的b u g 的数目，相比p e n f i u mp r o 增长了3 5 0 1 2 1 。 同时设计过程中任何细微的差错都可能会带来严重的后果，例如1 9 9 4 年i n t c l 开发的奔腾5 8 6 处理器由于在执行某个特定的浮点运算时出现错误，使i n t e l 哈尔滨丁程大学博十学位论文 不得不为此付出4 7 5 亿美元的巨额代价，召回了有缺陷的奔腾处理器，虽然这 种错误发生的几率虽然很小，2 7 0 0 0 年才可能出现一次，由此可见验证对于一 个成功的集成电路的设计是非常重要的。随着电路规模的不断增大，电路验证 的难度也随之增加，第三届v s i a ( v i r t u a ls o c k e ti n t e r f a c ea l l i a n c e ) 验证会议得 出的结论是“验证不仅仅是很难，而是非常，非常难 。2 0 0 3 年度的1 t r s 的 报告中指出，验证已经成为集成电路设计流程中开销最大的工作【3 1 。在目前集 成电路的工程项目中，验证工程师的数目超过了设计工程师，对于复杂的设计 更是达到了2 ：1 或者3 ：1 的比率，验证的时间占整个设计周期的5 0 - 一8 0 ， 因此设计的正确性验证成为设计的瓶颈1 4 , 5 j 。 造成这种局面的原因有两个：一是设计的规模呈指数增长。如果用设计中 的状态数目来衡量功能复杂度的话，则设计的功能复杂度随着设计规模又呈指 数增长。这对验证技术的处理能力提出了极大挑战。二是历史上设计流程中的 重点被放在了逻辑综合、布局布线以及测试产生等方面并取得了很多突破，而 对验证重视不够。这也导致验证成为目前的瓶颈。如果再不能在验证方面取得 大的突破，验证将成为半导体工艺继续前进重大的障碍，因此对集成电路的验 证技术进行研究是十分迫切和必要的。 集成电路设计采用自顶向下的设计方法，通常可以分成系统级、行为级寄 存器传输级( r e g i s t e rt r a n s f e rl e v e l ，r t l ) 、逻辑门级和版图级等，如图1 1 所示。集成电路的设计流程实际上是一个对设计模型逐步精化( r e f i n e ) 的过 程。在这个流程中设计验证就是要保证每个阶段实现的正确性，如功能、时序、 性能、功耗和可靠性等方面与设计规范的一致性1 6 l 。其中功能的正确性是最基 本的要求。在设计中，首先根据市场和客户的需求由芯片的设计人员做芯片的 系统规范( s p e c i f i c a t i o n ) ，这样的规范可以是由任意的形式语言来描述；其次 由设计人员将系统规范转化为初始的系统模型和期望的性质，其中初始的系统 模型可以使用m a t l a b 或s y s t e mc 描述，性质采用时态逻辑描述；然后采用高 级综合将初始的系统模型转化为r t l 结构( r t l 模型可以被迸一步的优化成 优化的r t l 模型) ，利用逻辑综合工具将寄存器传输级模型转换成门级模型， 再往底层进行物理设计直到版图，晟后阶段是芯片的加工，即基于芯片版图的 掩膜来制造出芯片的硅片并封装。在集成电路设计的每一步骤，都有可能引入 错误。因此芯片从其需求丌始，经过设计和生产，最终得到实际的芯片并投入 2 第1 章绪论 应用，其中的每一步都需要进行严格的验证或测试【7 】。 高抽象层次 - - i ： 编写 硼叫 l l i - l - - - 低抽象层次 图1 1 层次化电路设计 f i g 1 1h i e r a c h i c a lc i r c u i t sd e s i g n 为了确保电路功能的正确性，必须对各抽象层次的电路进行功能验证。集 成电路的功能验证基本可以划分为三类：模拟验证、形式验证和半形式化验证 f s e m i f o r m a lv e r i f i c a t i o n ) 。它们之间的主要区别在于模拟验证需要测试向量， 而形式验证不需要。模拟方法是面向输入的，因为设计者需要给定输入向量进 行测试，而形式验证是面向输出的，设计者需要提供待测试的输出特性。半形 式化验证结合了基于模拟的验证方法和形式化的验证方法。 传统的功能验证方法是模拟验证，它主要是通过对被验证电路施加验证激 励进行模拟，将得到的输出响应与预期的正确结果相比较，以此来发现其中的 错误。按照运行平台的不同，可以分为软件模拟( s i m u l a t i o n ) 和硬件仿真 ( e m u l a t i o n ) 。一般的模拟验证流程如图1 2 所示，其中激励生成与覆盖评估是 哈尔滨工程大学博士学位论文 模型检验中最核心和最关键的问题【8 9 】。 设计信息 规范信息 图1 2 模拟验证流程 f i g 1 2t h ef l o wf o rs i m u l a t i o nv e r i f i c a t i o n 模拟验证是目前工业上最常用的功能验证方法，但它有两个主要的缺陷。 首先由于指数级的时间复杂性，对于大型复杂的设计，不可能对整个输入向量 空间进行穷举的模拟。因此模拟验证能够发现错误的存在，但不能够保证错误 的不存在，即模拟验证难以保证测试的完全性。其次是难以定义合适的验证覆 盖率，而且验证者很难创建理想的测试激励，使之能够覆盖到所定义的各种评 估目标。 形式验证是用形式的方法来确立设计的实现满足规范的要求。所谓的实现 是指硬件在任何不同抽象层次的设计，例如系统级、r t l 、逻辑门级等，不仅仅 指最终的物理版图。所谓的规范是指设计所期望的并被认为是“正确”的属性， 通常用形式化的方法来描述。形式验证的任务是提供证明，以便确立实现满足 规范的要求，证明采取形式化的、数学的严格证明。与模拟验证方法不同，形 式验证方法是一种完全的方法，即相当于对设计或设计模块的整个输入空间进 行了穷举测试，从而能够证明设计实现是否与其规范功能一致。形式验证方法 主要包括：等价性检验、模型检验和定理证明【l l 1 2 l 。( 形式验证的详细介绍见 第2 章) 形式验证的好处是隐式地穷举了整个电路的输入变量空间，即它可以达到 1 0 0 的功能覆盖率，而且不需要产生测试激励。如果一个电路被证明是错误的， 那么形式验证算法将会给出一个反例，即提供一个原始输入激励，证明这个电 路与其规范关于这个激励的响应不同。模拟验证方法能够发现设计错误，但难 4 第1 苹绪论 以证明设计没有错误，然而形式验证却可以证明设计到底有还是没有错误。从 这种意义上说，形式验证是比模拟更严格、更完全的方法【1 2 】。 1 2 研究现状 随着集成电路设计的规模和复杂性日益增大，这使得设计模型必须面向更 高层次的设计、必须具有更好的强健性并且能够克服存储空间的爆炸问题。形 式验证在国内外主要现状为： ( 1 ) 基于可满足性( s a t i s f i a b i l i t y , s a t ) 问题【1 3 1 为引擎的验证方法研究以 及基于s a t 与二叉判决图( b i n a r y d e c i s i o nd i a g r a m ，b d d ) 或自动测试向量产 生( a u t o m a t i ct e s tp a t t e r ng e n e r a t i o n , a r p g ) 相结合的等价性验证和模型检验 的方法研究2 4 绷。基于s a t 为引擎的验证方法研究能够克服基于b d d 为引擎 的方法引起的存储空间爆炸问题，提高了验证电路的规模。但是由于s a t 本身 是一个n p 问题，求解s a t 问题需要频繁的程序调用。因此中科院、浙江大学 和复旦大学在合作承担的国家自然科学基金重点项目“从行为级到版图级的设 计验证与测试生成”中提出基于s a t 与b d d 或a t p g 相结合的验证方法。提 出了一系列的方法和策略，例如基于增量布尔可满足性的等价性检验方法、改 善的静态隐含策略、基于电路宽度的启发式策略等，试验结果显示在一定程度 上加快了验证速度、克服了存储空间爆炸问题并且能应用于较大规模电路的验 证i l s - 2 6 。基于s a t 与b d d 或a t p g 相结合的验证方法主要应用于逻辑门级电 路的验证，并不适合于高层次复杂的数据通路的验证。 ( 2 ) 基于混合约束s a t 验证方法研究 2 8 - 3 6 。由于r t l 电路不仅包含与、 或、非等对位级变量进行操作的基本门，而且还包含加法器、乘法器、比较器、 多路选择器等对字级变量或位字混合变量进行操作的复杂器件。在验证过程中 若将位变量集合和字变量集合分别看成是2 个域的s a t 问题，将位变量域的 s a t 问题用布尔s a t 求解器求解，而将字变量域的s a t 问题用线性规划 ( l i n e a rp r o g r a m m i n g ，l p ) 求解，在两个域的交界处，当某个位变量被赋值时， 就需要将该赋值的影响传播到字域中，这样就需要不断地在两个域间进行交替 的搜索并传播对变量赋值的决策结果，回溯成为一个必然的过程，会影响到求 解效率。文献 2 8 ，2 9 构造一个混合约束s a t 求解器，提出统一用l p 求解器来 求解同时包含位变量和字变量的混合约束问题。文献【3 0 】将性质检验问题转化 5 哈尔滨工程大学博士学位论文 i h- - - - - - 苗i ；暑鲁 为混合整数规划问题求解。文献【3 1 】提出的有限域约束求解器，是布尔约束求解 器的d p l l ，搜索过程针对r t l 电路的扩展。文献【3 2 】采用整数l p 来验证r t l 电路中的数据通路。文献 3 3 为r t l 电路中的多路选择器构造适用于混合整数 l p 求解的模型，r t l 电路的混合约束求解问题是目前在数字硬件的高层次验 证领域中受到极大关注的研究课题。他们的工作特点是无需在位一字两个域间进 行频繁的回溯操作，提高了混合约束的求解效率，能在较高层次上进行验证。 ( 3 ) 基于多项式的形式验证方法。在复杂i c 综合中，多年实践证明真正有 效的布尔函数的分解和替换方法是代数分解，而不是布尔分解，人们可以将逻 辑表达式看作代数多项式，并且多项式符号运算具有处理思想相对简单易实现 的优点，且具有形式上的正则性。国内外一些学者用多项式代数方法描述电路 行为，用字级多项式模型形式建立起高层数据通路的描述，进行了一些数据通 路分配和匹配工作瞰4 ，实现了基于符号代数的数据通路的有效综合算法1 4 2 - 5 7 1 。 他们的工作表明多项式表达式能实现电路数据行为的紧凑、正则、无二义性的 形式化描述，而且在支持单元匹配和部件重用方面也很有效，显示出多项式符 号代数在复杂芯片综合和验证方面的应用价值。文献 3 7 - 4 0 用多项式来描述组 合电路和时序电路，实现了基于多项式的组合和时序电路的验证和匹配。文献 5 8 1 提出了一个从元件的位级描述到字级线性多项式的抽象方法，应用于基于线性多 项式的验证和匹配。文献【5 9 】提出了个多项式抽象技术，有效地简化了功能可以 表示为一个多项式的时序设计块的验证任务。文献 6 0 基于代数基本定理和中国剩 余定理提出了一个有效的功能可以用多项式描述的时序设计的验证方法。文献 6 1 1 提出了一个基于吴方法的模型检验的框架，用多项式来表达r d i p k e 结构和c t l 公式，通过用吴方法计算特征多项式集来实现模型检验。文献 6 2 1 提出了一个关于 字级不连续函数的算术操作模型和r t l 设计模型的数学框架，其中字级不连续函 数的算术操作模型和r t l 设计模型是用多项式来表达的。文献f 6 3 】提出了一个在 行为级进行检验断言的方法，其中行为级的描述是转化成为一个多项式不等式集， 该方法能够有效的处理那些不能直接用整数非线性解决器或者s a t 解决器进行检 验的复杂描述。文献【删提出了一个多项式的描述模型w g l ( w e i g h t e d g e n e r a l i z e dl i s t ) ，应用于电路定时和功能验证。文献 6 5 7 0 】基于有限环代数和固 定字长多项式函数在r t l 上实现了数据通路的等价性验证和模拟验证。以上的工 作可以看出基于多项式的验证方法能够有效的应用于系统级、r t l 、逻辑级电路 6 第1 章绪论 的验证。 1 3 本文的工作 本文对形式验证中的等价性检验和模型检验方法进行了详细深入的探讨。 针对实现定点算术运算的电路，以有限环上多项式为形式验证引擎展开了下面 三方面的研究工作，如图1 3 所示，其中虚线框为本文所研究的内容。 图1 3 本文主要工作框架 f i g 1 3t h ef r a m e w o r ko f t h em a i nw o r k sf o rt h i st h e s i s ( 1 ) 针对定点数据通路的逻辑综合，如何证明其综合前的r t l 结构与综 合后的逻辑门级网表的等价性； ( 2 ) 针对定点数据通路的高级综合，如何证明其综合前后的定点系统模 型与r t l 实现或优化后的r t l 实现之间的等价性； ( 3 ) 针对定点数字信号处理( d i g i t a ld i g n a lp r o c e s s i n g ，d s p ) 电路的设计， 如何验证该电路的设计实现满足其相应的系统规范。 本文的主要贡献和创新点如下所述。 ( 1 ) 针对r t l 与逻辑门级的等价性验证，传统的方法是将r t l 电路采用 7 哈尔滨工程大学博士学位论文 商业的逻辑综合工具转化成逻辑门级，然后在逻辑门级进行等价性检验。本文 提出一种反向策略，将定点数据通路逻辑门级的描述( 算术转换) 抽象成字级 描述( 多项式函数) 。 ( 2 ) 构建v a n i s h i n g 多项式环的理想的极小强g r 6 b n e r 基，利用该g r 6 b n e r 基判决一个有限环上多项式是否为v a n i s h i n g 多项式，进而确定点数据通路的设 计规范与其相应的r t l 模型或优化后的r t l 模型之间的等价性。 ( 3 ) 对高层次电路实现中的器件和待验证的性质分别采用有限环上多项 式进行建模，将定界模型检验问题转化为定理证明问题，采用有限环上多项式 理想的g r o b n e r 基来解决该定理证明问题。 1 4 论文的组织结构 论文的组织结构如下： 第1 章绪论，介绍本文的研究背景和意义，概述了集成电路的功能验证方 法，进而分析目前形式验证中等价性检验和模型检验的研究现状，最后简介本 论文的研究内容和主要工作。 第2 章对集成电路的形式验证进行综述，介绍了形式验证的数学基础和形 式验证方法，其中数学基础主要介绍了基于判决图和s a t 的形式验证，形式验 证方法主要介绍了等价性检验、模型检验和定理证明方法。 第3 章首先介绍了算术转换和多项式函数的基本概念，在此基础上提出了 定点数据通路的算术转换描述到多项式函数描述的抽象方法，实现了定点数据 通路的位级描述与字级描述之间的等价性检验。 第4 章首先介绍v a n i s h i n g 多项式环的理想的基本概念，进而构建了 v a n i s h i n g 多项式环的理想的极小强g - r 6 b n e r 基。在此基础上提出了定点数据通 路的字级描述与字级描述之间等价性检验方法。 第5 章首先介绍了有限环上多项式理想的g r o b n e r 基的概念与算法，给出 了r t l 器件建模方法，进而提出了基于有限环上多项式理想的g r 6 b n e r 基的模 型检验方法。 最后，在结论部分对全文进行了总结，并探讨了今后的研究方向。 8 第2 章集成电路的形式验证综述 第2 章集成电路的形式验证综述 形式验证使用数学手段来严格证明设计的实现满足原始规范的属性。与模 拟验证的方法不同，形式验证方法是一种完全的方法，即相当于对设计或设计 模块的整个输入空间进行了穷举测试，从而能够证明设计实现是否与其规范功 能一致。本章从形式验证的数学基础和基本方法对形式验证方法做了总体的综 述。 2 1 形式验证的数学基础 从近十几年的文献报道来看，形式验证所基于的数学方法可以归结为：基 于正则的判决图( d e c i s i o nd i a g r a m , d d ) 表示方法和基于s a t 的方法等。 2 1 1 基于正则的判决图的形式验证 人们在形式验证算法设计实践中采用的判决图主要有b d d t i - 7 3 】、o f d d ( o r d e r e df u n c t i o n a ld e c i s i o nd i a g r a m ) 7 4 】、o k f d d ( o r d e rk r o n e c k e rf u n c t i o n a l d e c i s i o nd i a g r a m ) t 嘲、m t b d d ( m u l t i - t e r m i n a lb d d ) 1 7 6 1 、b m d ( b i n a r ym o m e m d i a g r a m ) 1 7 7 ，7 引、* b m d ( m u l t i p i l i c a t i v eb m d ) 【7 9 1 、k * b m d ( k r o n e c k e r * b m d ) s o l 、h d d ( h y b r i dd e c i s i o nd i a g r a m ) i s 】、* p h d d ( p o w e rh d d ) 8 2 , 8 3 】、e v b d d ( e d g e v 甜u e db d d ) 8 4 1 、f e v b d d ( f a c t o r e de v b d d ) 【8 5 】和t e d ( t a y l o r e x p a n s i o nd i a g r a m ) 8 6 , 8 7 】等。 其中b d d 、o f d d 和o k f d d 是位级d d ( d e c i s i o nd i a g r a m ) 表达厂：b ”一b 的函数( 其中b = f o ，l l 为布尔变量，聆n ) ；m t b d d 、b m d 、* b m d 、h d d 、 k 乖b m d 和p h i ) d 是字级d d ( w r o r d l e v e ld d ，w l d d ) 表达厂：b ”一z 的函 数8 8 - 9 0 l ；t e d 表达厂：z 一- - + z 的多项式。 2 1 1 1 位级d d 位级d d 嗍是指有一个根2 节点的有向无环图g ( 矿，e ) ，其中y 是g 中所 有根节点的集合，e 是g 中所有边的集合，它被用于表达变量矗= ( j c l ，屯，而) 的布尔函数f 。g 中的节点v 分为两类：非终端节点和终端终节点，非终端节 9 哈尔滨工程大学博士学位论文 点对应于t 中的某个变量，并且有两条分别由0 与1 标记的输出边，表示该节 点被赋值为0 或1 ，终端节点0 和1 分别对应于函数值为0 和l ，终端节点没有 后继。如果d d 中的每个变量在从根到终节点的每条路径上最多出现一次称d d 是自由的；如果d d 是自由的并且每个以相同的顺序出现在从根到终节点的每 条路径上称之为有序的。 位级d d 通过下列的分解方式表达布尔函数f ：b ”一b ， l 写；ov 。 s f = ；oo 而矗p d ( 2 - 1 ) l 。o i 磊 n d 式( 2 - 1 ) 中，l 。和。分别表示布尔函数厂关于的变量再= o 和毛= l 余因式， 屯= 。o 。，o 为异或运算。中变量的分解类型对应与一个分解类型 列表( d e c o m p o s i t i o n t y p el i 瓯d t l ) d = ( 吐，d 2 ，) ，其中z s ，p d ，n d ) ， s 为香农( s h a n n o n ) 分解，p d 为正极( p o s i t i v ed a v i o ) 分解，d 为负极( n e g a t i v e d a v i o ) 分解。 1b d d b d d 是由b r y a n t 于1 9 8 6 年提出的【7 ，b d d 是对每个变量迭代地进行香 农分解，即= i = 。vt ，。若一个b d d 是有序的并满足以下两个条件则称 为简化的有序b d d ( r e d u c e do r d e r e db d d ，r o b d d ) ： ( 1 ) 任意非终端节点的左、右孩子节点对应的布尔函数不相等： ( 2 ) 不存在两个表示相同变量的节点，使得它们具有同构子图。 如图2 1 所示为布尔函数厂= a bvc d 的r o b d d 表示，其中a ，b ，厂b 。 b d d 作为布尔函数的描述和运算工具已经广泛地应用到组合和时序电路 的等价性验证、符号模型检验、符号模拟验证、逻辑综合和测试中1 3 9 。大多数 基于b d d 的验证系统，像s m v 和s 已经成功地应用在控制密集型的系统中。 并且b d d 在逻辑级上进行组合逻辑单元的匹配是理想的。 1 0 第2 章集成电路的形式验证综述 回 图2 1 布尔函数f = a b v c d 的r o b d d 表示 f i g 2 1t h er o b d dr e p r e s e n t a t i o nf o rb o o l e a nf u n c t i o nf = a b vc d b d d 用在一些电路设计实例的验证过程中克服了状态爆炸问题，但是对于 一般电路随着输入个数的增加和功能复杂度的增加，b d d 的空间需求呈指数增 长，大大限制了它的应用，并且b d d 不能成功的应用于包含算术运算单元的 系统中。例如，b d d 表达乘法时需要的内存空间与输入变量呈指数级递增，因 此由于计算机内存的限制，超过1 8 1 8 位的乘法不能用b d d 表示【跖】。 划分r o b d d 通过引入中间变量来尝试控制