（微电子学与固体电子学专业论文）soc顶层验证平台和优化验证方法研究.pdf

摘要 摘要 随着集成电路技术的快速发展，工艺特征尺寸不断减小，产品的性能不 断提高，在单一芯片上实现全部系统功能的s o c 设计技术也已经逐渐走向成 熟。通过仿真建模实现s o c 设计和验证是目前的主流方法，随着s o c 设计规 模的增加，顶层建模与验证问题日益成为设计者关注的焦点。本文研究了s o c 顶层建模与验证的方法以及相关配置环境的实现技术，并对口有限状态机和 s o c 有限状态机优化验证问题进行了分析讨论，此外本文还研究了操作级验 证方法中功能覆盖率的优化问题。 本论文首先对如何构建多层次混合语言s o c 建模和验证平台进行了讨 论，分析了新型建模和验证语言s y s t e m c 的使用方法和特点，讨论了其通道 建模方法在s o c 顶层建模和验证方面的优势。本论文完成了多层次混合语言 s o c 平台配置环境的构建工作，讨论了平台环境的划分方法及其实现过程。 实际仿真结果说明s y s t e m c 语言作为一种新型硬件设计语言，在多层次混合 语言s o c 平台中可以与其他硬件设计语言( h d l ) 混合使用，进而实现对系统 的预设计和预验证。 本论文对有限状态机验证问题进行了研究。论文使用图论方法首先分析 了在坤有限状态机对应的有向图中构建e u l e r 路径的方法及其适用的情况， 同时提出了一种使用数学规划方法优化解决该问题方法。该优化方法针对初 始结点是出度点的i p 有限状态机特点提出并且经过了理论证明。同时对于i p 有限状态机验证来说，该优化方法简单实用、易于实现。 在构建e u l e r 路径对i p 有限状态机优化验证问题讨论的基础上，本论文 进一步研究了在有限状态机中构建e u l e r 回路的方法及其适用的情况。构造 e u l e r 回路的方法适用于初始结点是入度点和平衡点的i p 有限状态机，同时 该方法也解决了s o c 有限状态机优化验证问题。本论文提出了一种利用i p 有限状态机优化验证结果来对s o c 有限状态机进行优化验证的方法。该优化 方法可用于指导s o c 设计过程中对i p 有限状态机和s o c 有限状态机的设计 和验证，同时也可以作为分析有限状态机问题的e d a 工具的一个组成部分。 本论文最后通过研究操作级设计和验证方法的技术特点，提出了一种适 用于提高操作级功能覆盖率精度的优化方法。该优化方法对于t l m 模型的 功能覆盖率优化计算针对性强、易于使用。同时该方法适于在操作级s o c 设 哈尔滨工业大学工学博士学位论文 计中可以作为验证策略的组成部分辅助验证工程师设计随机测试集和计算功 能覆盖率。 关键词s o c ：建模；验证；图论：数学规划；功能覆盖率 一i i a b s t r a c t a b s t r a c t a si cd e s i g nd e v e l o p sf a s t e ra n df a s t e r , t h ef e a t u r es i z eh a sb e e nr e d u c e d a n dt h ep e r f o r m a n c ei si n c r e a s e d ，t h en e wc o n c e p ts e e ( s y s t e mo nac h i p ) h a s o p e n e d u pn e wp o s s i b i l i t i e s f o rt h e d e s i g n e r s t o d a y , t h el a r g e s c a l eo fi c p r o d u c t s i s r e a c h i n gi n t o t h et e n so fm i l l i o n so fg a t e s ，i ti s v e r yd i f f i c u l t t o c o m p l e t e t h e d e s i g n f r o m t o p t od o w n + t h ei m p a c to fs o ct e c h n o l o g yh a s g e n e r a t e dp o w e r f u lf o r c e st h a ta r er e s h a p i n gt h es t r u c t u r eo f t h es e m i c o n d u c t o r i n d u s t r i e s t h es e em o d e l i n ga n dv e r i f i c a t i o ni s s u e sa r es t u d i e di nt h i sp a p e r , a n dt h et l mf u n c t i o n a lv e r i f i c a t i o nc o v e r a g ei s s u ei sa l s oa n a l y z e d t h e i n c r e a s i n g i n t e r e s ti nm u l t i l e v e l m i x l a n g u a g e s o cm o d e l i n ga n d v e r i f i c a t i o np l a t f o r mh a sg e n e r a t e dan e e df o re f f i c i e n ta n dr e c o n f i g u r a b l es o c e n v i r o n m e n t t h ep r o b l e ma s s o c i a t e sw i t ht h e e wh a r d w a r ed e s i g n l a n g u a g e s y s t e m cd e s i g nm e t h o da n dt h es o cc o n f i g u r a t i o ne n v i r o n m e n t ，s y s t e m ca n d h d l ( v e r i l o go rv h d l ) c a n b eu s e dt od e s i g nv a r i o u sa b s t r a c t i o nl e v e l s i nt h i s p a p e r , a n s o ce n v i r o n m e n tw h i c hi ss u i t e df o rm u l t i 1 e v e l m i x 1 a n g u a g e s i m u l a t i o na n dv e r i f i c a t i o ni sp r e s e n t e da n dd i s c u s s e d t h er e l a t i o n s h i pb e t w e e nf s mv e r i f i c a t i o na n df u n c t i o n a lv e r i f i c a t i o n ，a n d t h eb a c k g r o u n di n f o r m a t i o na b o u tf s m w e i g h t e dd i g r a p ha r ei n t r o d u c e dt h e n i t i sk n o w nt h a tt h eb a s i cp r o b l e mo fh a r d w a r ev e r i f i c a t i o ni st od e t e r m i n ew h e t h e r ad e s i g nm e e t saf i n i t es t a t em a c h i n es p e c i f i c a t i o n an o wa p p r o a c hb a s e do n d i g r a p ht h e o r ya n dm a t h e m a t i c a lp r o g r a m m i n g ，w h o s et a r g e ti st ov e i l f ya l lt h e s t a t et r a n s i t i o n si nt h eo p t i m i z e dt i m e ，i sp r e s e n t e di nt h i sp a p e r t h eo p t i m i z e d m e t h o dh a st w op a r t s ，o n ei sf o ri pf s mv e r i f i c a t i o na n dt h eo t h e ri sf o rs o c f s m h o wt ob u i l de u l e rp a t ha n de u l e rt o u ra r ea n a l y z e da n dp r o v e n a n dt h e v e r i f i c a t i o np a t hc a nb eu s e dt ov e r i f yt h ef s m t h ef s m v e r i f i c a t i o np a t hc a n b eg e n e r a t e da u t o m a t i c a l l yb yt h i sa p p r o a c ha n dt h i sm e t h o dh a sb e e na p p l i e di n t h ec + s o cv e r i f i c a t i o ne n v i r o n m e n t t h ee x p e r i m e n t a lr e s u l ts h o w st h em e t h o d c a na c c e l e r a t et h ev e i l f i c a t i o np r o c e s se m c l e a t l y f o rh a r d w a r ed e s i g n ，s i m u l a t i o ni ss t i l lt h ep r i m a r y a p p r o a c hf o rf u n c t i o n a l v e r i f i c a t i o no fc i r c u i t d e s c r i p t i o n sw r i t t e n i nh a r d w a r ed e s i g n l a n g u a g e t h e 一i 一 哈尔滨工业大学工学博士学位论文 c o v e r a g em e t r i c sm e a s u r et h ep r o c e s so f v a l i d a t i o na n di n d i c a t et h eu n e x p l o r e d p a n so ft h ed e s i g n t h i sp a p e rd e s c r i b e sac o v e r a g e d i r e c t e dm e t h o dt h a t i s s u i t a b l et ot r a n s a c t i o nl e v e lv e r i f i c a t i o n t h ea d p r o a c hi sb a s e do nr a n d o mt e s t g e n e r a t i o n ，a n dt h ec o v e r a g ei si n c r e a s e db yu s i n gf a u l ti n s e a i o nm e t h o d u s i n g c a s es t u d i e s ，w es h o wh o wt oe s t a b l i s ht h et e s t b e c ha n dh o wt h i sa p p r o a c hw a s u s e dt oi m p r o v et h e q u a l i t yo f t r a n s a c t i o nl e v e lf u n c t i o n a lv e r i f i c a t i o n k e yw o r d ss o c ；m o d e l i n g ；v e r i f i c a t i o n ；g r a p ht h e o r y ；f u n c t i o n a l c o v e r a g e m a t h e m a t i c a l p r o g r a m m i n g 一一 蔡1 章缍论 烹苎! ! ! 竺燃苎! = ! ! 烹竺= = = = 懋= = = = 竺烹兰! ! ! = 黑竺! ! ! ! 繁竺竺詈拦i i i i i ii i i i 篇竺= = ! = = ! = = 黑 1 1 课题的目的和意义 第1 章绪论 超大规模集成窀鼹( v l s i ) 技术豹不断发鼹使褥以予万计数晶钵管集成予 单个芯片成为璐实，消费类电子的强勘增长对新产品从开发别推向市场的压 力不断增加，以集成不同i p ( i n t e l l e c t u a lp r o p e r t y ) 功能模块于个芯片为设计 愚路的s o c ( s y s t e mo nac h i p ，片上系统) 设计方法正建在这种情况下应运面 生的【l “】。片上系统能够将数字电路和模拟电路集成猩单个芯片上，进而实 疆藩号鹣采集、存褚、处理等余嚣系统功憨。s o c 设计蔹赣予辩已有瓣搂决 的复用( r e u s e ) 进行设计。这与传统设计方法存在薏明鼹区别。片上系统在速 壤、功怒帮成零等方嚣较多芯片组成翡系统其有明曼缆势，霹以预见片上系 统在集成电路设计技术中将占据越来越蓬要的地位 如s 1 。 由于逻辑综合和自动布局布线等相关e d a 工具的使用，i c ( i n t e g r a t e d c i r c u i t ) 设计中只要代码设计阶段实现的功能准确无误、合乎规范的要求，整 个i c 设计流程就会顺利进行。从设计层次上看，用于实现功能设计的代码设 计阶段是从规范协议到产品实现的转换过程，在设计层次中属于顶层( t o p l e v e l ) 设计。在设计过程中，完成设计之后要对所实现的设计进行确认，这一 步骤被称为验证。相关资料显示目前的顶层设计的功能验证工作在整个s o c 设计中的比重已经超过了7 0 ，同时设计资源的主要部分也已经放在了设计 验证工作上【6 1 ，由此可见顶层验证的重要性。 s o c 的顶层设计用于实现系统的原始模型，因此也被称为系统级设计。 系统设计一般使用c c + + 来实现，系统级实现之后是r t l ( r e g i s t e rt r a n s f e r l e v e l ，寄存器传输级) 设计阶段，为了方便问题的讨论，在本论文中顶层设计 泛指实现功能设计的阶段( 包括c c + + 设计阶段和r t l 设计阶段) 。系统级设 计包括了建模和验证两个部分，两者彼此独立又紧密联系，本论文对建模方 法的研究是进行验证的基础工作。系统级建模有助于设计者更好地理解和修 改设计规范，同时依据实现的系统级建模，可以进行预验证为后续的验证工 作打下基础。对于系统级建模来说不仅要具有灵活和高效的应用特性，更重 要的是系统级建模本身要具有良好的可实现性，显然系统级建模是否快速、 洽拳滨王堑大学工学薄学位论文 高效是其核心问题。 对于系统级验证来说，根本任务是确保系统级建模符合设计规范的要求， 其核心问题涉及到如何构建验证平台、采用的验证策略、验证评估标准等等 诸多细节。关于验证问题的最典型案例莫过于1 9 9 4 年i n t e l 微处理器浮点问 题，为了平息这场风波i n t e l 公司花费了近5 亿美圆。p e n t i u mb u g 的影响是 如此之深刻，以至于一种新型的验证技术形式验证方法因此得以迅速被 推动和发展，i n t e l 公司在其随后的微处理器设计中不断使用各种验证技术以 保证其设计实现的正确性【9 “”。 由于s o c 设计规模及复杂度的不断增加，目前设计中越来越关注于系统 级建模与验证问题，各大e d a 供应商及s o c 设计公司一方面在寻找更好的 建模形式，另一方面在寻求更佳的验证方法。s o c 系统级建模与验证是当前 设计的热点和难点问题，本论文正是在这种背景下提出的。 本论文通过对s o c 系统级设计建模与验证方法的研究，讨论了多层次混 合语言s o c 平台建模技术和配置环境的实现方法，并对有限状态机优化验证、 操作级验证方法中功能覆盖率优化等相关问题进行了研究。 1 2s o c 建模与验证概述 圈1 - 1s o c 的设计流程与验证流程 f i g u r e1 - lt h ed e s i g nf l o wa n d v e r i f i c a t i o nf l o wo fs o c s o c 建模是建立s o c 模型的过程，建立的模型用于反映最终设计产品的 相关属性。从上个世纪8 0 年代开始，集成电路的设计开始由c a d 辅助电子 电路的设计仿真开始向使用硬件设计语言( h d l ，h a r d w a r ed e s i g nl a n g u a g e ) 过渡【l ”，由于v l s i 设计的不断发展，硬件设计语言也在不断更新和调整。 可以说s o c 建模和验证方法与硬件设计语言是紧密联系在一起的。根据设计 一一 第l 章绪论 流程的不同，s o c 建模也有不同的描述层次。与设计流程相对应的是验证流 程，j a n i c kb e r g e r o n 在 6 】中将验证定义为“确认一个设计正确性的过程”， v s i 组织在虚拟器件设计方法中也将v c 的设计流程细化为建模与验证交互 的过程i “】，总结起来s o c 的建模和验证流程如图l - 1 所示。 1 2 1s o c 建模方法概述 s o c 建模方法可分为两类：第一类方法是由传统瀑布式建模方法 ( w a t e r f a l l ) 过渡到新型的螺旋式( s p i r a d 建模方法，第二类方法是从传统自顶向 下式建模方法过渡到自顶向下与自底向上相结合的建模方法。 1 2 1 1 从瀑布式过渡到螺旋式的建模方法传统的集成电路瀑布式建模过程 中，建模步骤呈阶梯状，一个设计阶段接着一个设计阶段进行，如图1 2 所 示，瀑布式建模流程适用于标准尺寸为o 5 z m 的1 0 万门级的设计1 1 j 。瀑布式 建模流程的缺点在于，因为相应阶段的设计的团队彼此独立，设计环节的切 换缺乏足够的沟通，因此会出现后续设计团队让已经完成设计的团队修改设 计的情况，比如综合团队告知代码实现团队为满足时序要求代码需要修改， 代码实现团队告知顶层建模团队算法没有实现完全等等。 囝1 2 传统瀑布式建模流程 f i g u r ei - 2t r a d i t i o n a lw a t e r f a l ld e s i g nf l o w 晗尔演工娃大学工学博士学位论文 i i 随着复杂度增加，设计尺寸不断缩小，产品进入市场的时间压力在上升， 芯片设计者面临着修改建模流程以适应s o c 设计的实际情况。对于比传统设 计更加复杂的s o c 设计来说，需要对软硬件进行同时开发以保证系统功能的 正确性，物理级设计的相关问题也必须在设计阶段的早期进行考虑，因此传 统的瀑布式建模方法不再适合，建模方法也转向螺旋式建模方法。螺旋式建 模方法如图1 3 所示，与传统瀑布式建模方法比较，螺旋式方法在并行设计、 验证等方面更加适应于s o c 设计流程，具有更高的效率。 s y s t e md e s i g na n d v e r i f i c a t i o n ph0sical f t 0 m i n g j i h a r d w a r e i s o f t y f a r e 1 p h y d c a l t i m i n g e 【a r d w a r es o f t 、r a r e s p e c i f i c a t i o n ： s p e c i f i z a t l o m s p e c i f i c a t i o ns p e c i f i c a t i o n a l e a p o , 、x e r l o d m h m 。 g o r i t h m c a p p l i c a t i o n c l o c kn t ed e s i g uc c l o c kf i “t u e n c y c d e v e l o p m e n t l n i l c r o p r o l o e l ) e d e 、e l o p m e n t d e c o m p o s h i o n p r e l h n m a r 5 c b l o c kt i m i n g b l o c ks e l e c f i o t u ： c a p p l i c a t i o n f l o o r p l a n s p e c i f i c a t i o nd e s i s tp r o t o t y p et e s t i n g u p d a t e df l o o t _ p l a n sc b l o c ks y n t h e s i s c b l o c kv e r i f i c m i o nc a p p l i c a t i o n p l a c e m e n td e x , 。e l o p n l e l l t u p d a t e df l o o r p l a r r sc c t o p l e v e lh d lc a p p l i c a t i o n t r i a lp h l c e n i e n t c = t o p - l e v e l c 二 t o p e v e 】 c a p p l i c a t i o n w n t h e s i s v e n n c a t l 0 1 1t e s t m 2 图1 - 3 螺旋式s o c 建模流程 f i g u r ei - 3s p i r a ls o cd e s i g nf l o w 对于一个要实现的设计来说，采用螺旋式建模方法，工程师可以同步开 发子模块的相关协议和算法、设计系统级验证集、对芯片设计时间进行预估 等等。 1 2 1 2 从自顶向下建模方法过渡到自顶向下与自底向上相结合的建模方法 第二类建模方法包含两种建模设计方法，一是自底向上的方法，一是自顶向 d 籀1 章缮论 i i h i i l i ii m i i 下的方法。传统的手工设计电路时，整个建模设计过程从最底层设计开始， 首先完成逻辑电路设计实现各个独立功能模块，再将这些功能模块连接起来 组装成为一个硬件系统【”l 。自底向上建模方法的缺点在于难以对整个系统进 行规划，当系统整体完成之后，如果需要改进的话，其设计改动就比较困难， 因此这种方法难于适应s o c 的建模设计，自底向上的建模设计方法如图1 - 4 ( a ) 所示。自顶向下的建模方法类似于瀑布式建模方法，其设计按照不同的设计 抽象层次进行划分，但与瀑布式建模方法的区别之处在于该方法以对设计的 模块化分解开始，以对各个模块的集成和验证结束，自顶向下的建模设计方 法如图1 4 ( b ) 所示。采用自顶向下的建模设计方法易于控制整个系统的设计 过程，可以合理调整设计方案，对系统的性能参数进行不断的细化和优化。 文章 1 6 认为自顶向下的建模方法可以整体考虑s o c 软、硬件系统设计 的要求，把系统需求、芯片体系结构、算法模型、软件结构等紧密结合起来， 对于s o c 设计是非常合适的。 ( a )( b ) 图1 4 自底向上及自顶向下建模流程 ( a ) 自底向上建模流程( b ) 自顶向下设计流程 f i g u r e1 - 4b o r o m - u pa n dt o p - d o w nd e s i g nf l o w s ( a ) b o t t o m 。u pd m o d e l i n gd e s i g nf l o w ( b ) t o p - d o w nm o d e l i n gd e s i g nf l o w 自顶向下建模设计方法的主要步骤一般包括下列内容： ( 1 ) 系统总体方案设计：芯片系统功能、指标定义、需求分析、产品市场 定位，软硬件划分、指标分解等整体方案论证： ( 2 ) 软、硬件方案设计：确定软、硬件体系结构，模块功能的详细描述及 一，一 蛤尔滨工业大学王学 毒士学位论文 技术指标疆求，时序及接口定义等工作： ( 3 ) 模头竣诗开发：宠残疆彳串模获静嚣发，行燕窝辩詹售囊测试，瘸层硬 件驱动程j 葶编写，算法设计及仿真，协议和应用软件的设计与歼发。对于复 杂豹功能模块，霹进一莎触分子模块。程算法仿真时，缀提系统指标的要求 可采用硬件加速方法等； f 4 ) 软、硬件协同仿真测试：主要测试系统方案和软、硬件模块设计功能 的正确性； ( 5 ) 样机平台的测试：主要是自建或专用的验证平台，测试整个设计的功 能、性能指标是否达到要求。 对于实际的建模设计而言，自项向下的方法是有一定困难的，因为在设 计中往往存在一时难于实现的设计模块，这样整个设计过程就会拖延。此时， 先完成较低层次的设计，最后考虑系统级设计往往更为合理，因此采用自顶 向下与自底向上相结合的方法是实际设计中首选的建模方法。 1 2 2s o c 验证方法概述 根据i e e e 的定义，验k 正( v e r i f i c a t i o n ) 的含义是：“通过对客观凭证的检 查和认定，从而确认所规定的要求被实现了”，简单来说验证就是要证明“所 设计即是所要求”。由图1 1 可以看到，验证在s o c 设计中是一个实际的过 程，通过这一过程，设计者可以确认所进行的设计是符合相应的规范要求 3 6 、3 8 1 。s o c 设计中的验证可以按照设计流程划分成三卜部分：功能验证 ( f u n c t i o n a lv e r i f i c a t i o n ) 、时序验证( t i m i n gv e r i f i c a t i o n ) 和版图验证( 1 a y o u t v e r i f i c a t i o n ) 。 1 2 2 1 功能验证作为对设计规范的确认过程，功能验证是验证流程中的第 一个环节，也是目前s o c 设计面临的瓶颈之一【6 “。功能验证是随着集成电 路设计规模的增加而日益受到i c 业界重视的，功能验证占据了越来越多的产 品开发时间，同时也占用了越来越多的软硬件资源。 功能验证是确认一个设计从规范到建模正确实现的第一步，这一验证步 骤对应的是顶层建模。顶层建模实现了设计者对规范的理解，功能验证则用 于检验这种理解的正确性。功能验证对于设计理解的确认是其与时序验证和 版图验证最显著的不同。功能验证的根本问题是如何完全验证( c o m p l e t e v e r i f i c a t i o n ) ，这也是目前所有关于功能验证的方法围绕的中心话题，但是完 全验证的目标对于一个大规模设计来说是一个几乎无法实现的目标。 一o 一 第1 苹绪论 功能验证过程中使用大量的测试巢以确认褶应的功能，这些测试集会占 用相当的仿真时间，如架测试过程中如现问题，排错和纠错也将耗费肘日。 就外如何合理安摊验 芷髅次，使用适当静验诞策略狃方法氇都是功能验证萄 临的实际问题。验证覆菔率被用于衡量验证的效果，目前一般使用的覆盖率 撩标包括路径覆盖率、条件覆盏率、功憩覆盏率等等 】。 1 2 , 2 2 时序验诚和版图验证集成电路设计必须满足定的时序关系，经过 练合褥至逻辑电路之嚣黉要验谖孵彦关系，这一般被秣为时黪验证，也被稼 为时序分析( t i m i n ga n a l y s i s ) 。 电路中的延迟与时序验证密切相关，传统芯片设计中只考虑门本身的延 迟，互连引起的延迟可以忽略不计，但是随着s o c 设计的发展，晶体管尺寸 不断降低，门的速度越来越快，i s i s 0 电路性能提高的主要因素不再是开关速 度，而是互连延迟。时钟频率越高，互连线作为扇出负载引起的延迟在整个 时序预算中所占的比例越大，精确地计算这部分延迟对于时序验证来说至关 重要f 3 9 】。 目前可以使用相应的e d a 工具进行时序验证工作，e d a 工具中的时序 验证中采用静态时序分析技术，这是一种穷尽分柝方法，可用以衡量电路性 能【4 。它提取整个电路的所有时序路径，通过计算信号在路径上的延迟传播 找出违背时序约束的错误，这种方法主要检查建立时间和保持时间是否满足 要求，而它们又分别是通过对最大路径延迟和最小路径延迟的分析得到的。 静态时序分析的方法不依赖于激励，而且可以穷尽所有路径，其优点在于运 行速度很快，占用内存少【3 9 , 4 1 】。 版图设计是i c 设计中的重要环节，在这一过程中每个元件的电路将转换 成集合表示，同时元件间连接的线网也被转换成集合连线图形【4 2 1 。与电路设 汁不同，版图设计必须考虑具体的工艺实现，因此存放版图的库必须是工艺 库或附在别的工艺库上的库。 版图验证一般包括设计规则检查( d e s i g n r u l e sc h e c k ，d r c ) 、电学规则检 查( e l e c t r i c a lr u l e sc h e c k ，e r c ) 、版图，逻辑图对比, ( 1 a y o u tv e r s u ss c h e m a t i c ，l v s ) 等等。设计规则检查( d r c ) 是一种针对几何结构的检查，用于确保在某一特 定工艺条件下版图的正确实现。d r c 过程需要考虑i c 制造过程中不同工艺 过程引起的几何尺寸偏差，对于版图采取适当的胀缩运算。d r c 过程可以检 查版图图形的大小及各种图形之间的位置关系，对于不满足规则的图形进行 报错。电学规则检查( e r c ) 用于检查违反电性规则的错误，能够查找出诸如 短路存在的确切位置。一般其查找的错误可以分为两类，一是与工艺无关的 一7 晗象滨王监大学王学撰譬位论文 错误，如短路、开路、节点悬空：二是岛工艺有关的错误，如错误的器件类 瑟、错误熬注入类型、镶溪魏懿藤编曩簿等。凝霉，逻搬爨黯毙( l v s ) 耀弓= 硷 瓷版图与门级电路网表愚否规则致，尽管d r c 也悬对规则的检查，但是 虫子d r c 只针对尺寸攮则检查，无法与门缎愈鼹比较，l v s 步骤俣诞了舨 圈与门缀电路的致性。借助e d a 工具可以节省大量的人工验证版图时间， 但是版图验证也肖脱离计算机需隳人工检查的项目，如压点检囊、特殊器件 捡庭、抗嗓音捡淼等等l s 2 0 * 。 1 3s o c 顶层建模与验证 1 3 is o c 顶层建模方法 顶层建模包括三个方面的内容：整体模块划分、关键模块细化、代码实 现及仿真。其中代码实现及仿真是顶层建模的主要环节【l ”。按照s o c 顶层建 模使用的语言类型，可以将其分成三类：完全使用h d l 建模、使用高级语 言和h d l 混合建模、使用新型硬件语言建模。 1 31 1 完全使用h d l 建模完全使用硬件描述语言进行建模是早期s o c 设 计采用的方法，由于当时i c 设计的规模不是很大，对于设计的移植性、复用 性以及仿真的速度要求不是很高，一些i c 设计公司从模块的设计，到最终验 证平台的建立，完全使用h d l 来完成 1 5 , 1 8 】。目前很少有人会采用这种建模 方式进行s o c 建模，因为这种建模方法的扩展性能较差，仿真运行的效率也 较低，无法满足现在的建模设计要求【阳q2 1 。s o c 建模设计的复用特性要求设 计要具有良好的扩展性和移植性，即在s o c 平台中可以方便地增加或减少设 计需要或不需要的i p 模块。对于完全使用硬件描述语言实现的设计来说，增 加或者去除某个模块就意味着对与此模块相关联的h d l 代码的繁琐修改， 这一点不利于口模块的复用和移植。同时由于建模全部是h d l 代码描述， 对于大型的s o c 建模来说，其仿真时间上的耗用也是相当巨大的。 对于小型的s o c 设计建模来说，完全使用h d l 建模的方法还是可以使 用的，因为这种方法可以由硬件设计工程师自行完成，也便于其维护。 1 3 1 2 高级语言和h d l 混合建模如今被广泛使用的s o c 建模方法是由高 级语言( 如c ，c + + ) 与h d l 一起进行建模的方法，即s o c 建模的一部分是硬 件描述语言h d l ( v e r i l o gh d l 或v h d l ) 来完成，一部分使用c c + + 等高级 语言作为h d l 的替代模型【2 ”】。 一8 一 第1 掌绪论 不论是v e r i l o gh d l 还是v h d l ，其对予设计的实现方法较高级语言蠢 吉复杂狠多。如果要建模的设计模块w 以使用c 等离级语裔来替代的原有 h d l 代码的模戮，这种可替代模型既肖原h d l 代码模块豹功能又包含足够 静时序信息，而置可苏侠速仿真的话，那么个设计璜器静建模速度无疑会 相应提高，这正是高级语言被引入建模设计的原因。为了将离级语言引入设 诗建模，各大嚣蛰a 供应褒为v e r i l o g 蘩囊器增搬了p l i ( p r o g r a m m i n g l a n g u a g ei n t e r f a c e ) 功能，为v h d l 仿真器增加了f l i ( f o r e i g nl a n g u a g e i n t e r f a c e ) 功缝，这些增加鲍功懿为c 秘j a v a 等舞级语骞进入颚层设谤建攘环 节提供了方便之门2 5 2 6 。 引入高级语言建模可以在算法级上首先对模块进行设计，同时快速验证 模块功能的j 下确性，这不仅有利于对此后开始的h d l 代码的编程工作的理 解与验证，同时为进行与硬件相关的软件设计工作提供了可以依据的环境。 此外，高级语言建模还具有仿真速度快，便于修改调试等优点。目前c 和 c + + 语言被成功引入系统级建模设计，近年来关于s o c 设计建模的 文章中，频繁提及使用c 或者c + + 建模的实际意义及其应用 2 7 - 2 9 j 。做好c 或c + + 的系统级建模设计，这是今后段时期的s o c 设计方向之一。 高级语言与h d l 混合建模的优势不仅在于其建模速度和仿真速度更快， 还因为混合建模方法中使用了设计工程师比较熟悉的h d l 和c 等语言，这 使得建模设计更易于完成。 1 3 1 3 使用新型硬件语言建模鉴于传统使用的v e r i l o gh d l 和v h d l 两种 主要硬件描述语言在s o c 顶层建模中的局限性，在通过引入高级语言进入硬 件设计之后，业界也同样在寻求新的方式来实现顶层建模。尽管通过使用应 用程序接口( a p i ) 可以将高级语言引入h d l 建模环境，但是由于存在转换过 程，建模的体化受到影响，而且高级语言的效率优势会受到不同程度的影 响，新型硬件语言正是在这样的背景下产生的。此外，由于功能验证问题的 日益突出还要求新型硬件语言能够面向验证设计。目前用于顶层建模的新型 硬件描述语言可以分为两类：一是由v e r i l o gh d l 和v h d l 这样的传统硬件 设计语言派生出来的，一是由a c + + 设计语言改造得到的硬件描述语言。 由传统硬件设计语言派生的新型语言的典型代表是a c e e l l e r a 标准组织 推广的s y s t e m v e r i l o g 硬件描述语言。s y s t e m v e r i l o g 是v e r i l o g 语言的高层次 扩展，这些扩展部分增强了v e r i l o g 的设计与验证能力，比如：c 语言的数据 类型、结构体、合并和未合并数组、接口、声明等。s y s t e m v e r i l o g 语言被看 作是c ，c + + ，s u p e r l o g 和v e r i l o g 的混合体，它极大地扩展了抽象结构层次 一9 一 晗尔滨工鼗穴学工学博士学位论文 i i h i i i i i 的设计建模熊力，把建模和验证融为一体p 0 - - 3 ”。 掰一种新型硬彳串语言怒由c c + + 设计谣言改造得到的。c 语宙作为目前 最为完善的一种设计语言始终得到i c 设计人士的青昧，人们希望可以对c 语言进行有效的改进，便之能够用予s o c 的各阶段设诗。嚣此许多i c 开发 商都自行改造和使用自己改造的c 环境，其中得到日、- 7 - ( h i t a c h i ) 等公司支持 匏s p e c c 【鄞l 楚较必成功熬一耱，整怒麓监赛羲广泛支持魏怒s y s t e m c 弘喇l 。 s y s t e m c 是熬于c + + 开发的种新溅硬件描述语言，适用于不同抽象层次的 建摸掇述。s y s t e m c 痰一组描述类毂头文转巍一个包含谤粪谈熬连接库组成， 在用户的描述程序中必须包括相应的头文件，然后可以用通常的a n s ic 十+ 编译器编译该程序。 眈较s y s t e m v e r i t o g 和s y s t e m c 两种语言特点，萁运用的设计层次是不 同的。s y s t e m c 一般被用来实现虚拟原型和软硬件协同设计，s y s t e m v e r i l o g 一般程r t l 设诗中蠢更爵瀚应爱，受逶予实现建搂察验谖f 与h d l 实蕊豹 r t l 级设计致) 。此外这两种语言比较来说，s y s t e m c 的开源性质是其快速 发震完善的一个重要溺素。以本论文疆究颈层建模和验证 、薅题的需要，我 3 选择了s y s t e m c 进行相关的研究工作。 i 3 2s o c 顶层验证方法 s o c 顶层验证是对设计的功能验证，s o c 功能验证方法可以分为两类： 一是基于形式技术的验证方法( f o r m a lm e t h o d ) ，一是基于仿真的验证方法 ( s i m u l a t i o n b a s e d ) 。 1 3 2 1 基于形式技术的验证方法早期的形式化方法始于上个世纪6 0 年代 末7 0 年代初，用于研究计算机的程序设计问题，进行程序证明，这样的研究 与同时期出现的软件危机是有密切联系的 4 5 嘶】。上个世纪8 0 年代中后期， 形式化方法被弓f 入硬件设计研究中，用于对硬件设计进行准确描述及正确性 证明 4 8 5 0 。1 9 9 4 年的p e n t i u m 微处理器浮点问题之后，i n t e l 公司成立了形式 验证部门以加强对设计中潜在错误的查找能力，也正是从这一事件之后，硬 件的形式验证方法得以迅速发展【5 ”。形式验证方法的原理是使用数学方法形 式化地证明设计实现部分是否满足规范的描述要求。形式验证一般可以分为 布尔式等价性检查( b o o l e a ne q u i v a l e n c ec h e c k i n g ) ，模型检查( m o d e lc h e c k i n g ) 以及定理证明( t h e o r e mp r o v i n g ) 。硬件验证中的形式方法的主要思想是，将设 计( 设计规范或者设计代码) 转换成为种规范形式，当对某一设计进行验证 一1 0 第1 章绪论 霹，跑较该设诗与英曩振设诗瓣娥莲形式憩虿等徐，经誉使震骢羧范形凌毽 括b d d 、a t p g 和s a t l 5 扣5 3 1 。 布尔式等价性捡套用予判断两个组合魄路在绘定输入鲍情况下功能是否 相等，对于肖着多鼷次数据炎型的i c 设计来说，布尔等价性检查藏有实际的 意义。比如对一个设计的r t l 代码进行修改之后，希望判断修改后的设计与 原竣计蔗否功能一致；或者在对r t l 代蕊避行综合之螽，希望了解综合麓豹 网表是否与原r t l 代码功能相同等等【7 1 。布尔式等价性检查已经成为业界验 迂设诗孛赘一拿关键耀萤，穗关豹e d a 王吴氇基经禳当戏熟弼，务夫e d a 供应商都有自己的相应产晶，如c a d e n c e 公司的i n c i s i v ec o n f o r m a l a s i c p ，s y s n o p s y s 公司戆f o r m a l i t y 粒e s p 筘】以及m e n t o r 公司豹 f o r m a l p r o p ”。一般来说，等价性检查用于判断综含盾两表的正确憔f 酊。 模型检查用于判断具有有限状态集合的系统是否有其规范规定属性，可 以用来检查一个设计的有限状态机是否存在不可达或孤立( i s o l a t e d ) 状态等等 【”。但是由于形式化方法与仿真方法的不同，形式方法中有限状态机验证方 法不能应用于仿真方法。形式方法的描述实现通常使用计算时钟树逻辑 ( c o m p u t a t i o nt r e el o g i c ) 以及线性时序逻辑( l i n e a rt e m p