2024年2月23日发(作者：)

计算机研究与发展JournalofComputerResearchandDevelopmentISSN100021239ΠCN1121777ΠTP43(6):974～979,2006龙芯2号微处理器的功能验证张　珩121,2　　沈海华1(中国科学院计算技术研究所计算机系统结构重点实验室　北京　100080)(中国科学院研究生院　北京　100049)(zhangheng@ict1ac1cn)FunctionVerificationofGodson22ProcessorZhangHeng1,2andShenHaihua11(KeyLaboratoryofComputerSystemandArchitecture,InstituteofComputingTechnology,ChineseAcademyofSciences,Bei2jing100080)(GraduateUniversityofChineseAcademyofSciences,Beijing100049)2Abstract　DevelopinganewleadingedgeGodson22processorisanimmenselycomplicatedundertaking1InthecaseofGodson22processor,themicro2architectureissignificantlymorecomplexthanthepreviousGod2son1processorandhowtoensurethefunctioncorrectnessisagreatchallengetoverificationparticipants1Simplearchitecturalleveltestsareinsufficienttogainconfidenceinthequalityofthedesign1Detailedplanmustbecombinedwithabroadcollectionofmethodsandtoolstoensurethatdesigndefectsaredetectedasearlyaspossible1DescribedinthispaperaretheverificationflowandmethodologyintheGodson22proces2sordesignpriortotapeout1Simulationisthedominantmethodinthedesign,andthestateofartformalmethodarealsousedtoverifysomepartsofthedesign1Keywords　functionverification;architecturevalidation;processordesign;simulation;formalverification摘　要　开发龙芯2号这样的高性能通用处理器是一项极其复杂的艰巨任务1龙芯2号处理器的设计规模和复杂度比龙芯1号增加了许多倍,如何保证设计的正确性是一个重大挑战1简单的系统级测试已经不能满足设计的需要,这就要求采用多种有效的、先进的验证方法和工具帮助设计者尽可能早的发现和改正设计错误1主要介绍了在龙芯2号处理器的设计开发过程中采用的功能验证流程和主要验证方法1模拟仿真是主要的验证手段,新的形式化验证方法也应用到了验证流程当中1关键词　功能验证;结构验证;处理器设计;模拟仿真;形式化验证中图法分类号　TP3021　引　　言随着集成电路制造工艺的快速发展,功能验证已经成为了ASIC设计流程的瓶颈1在一个完整的设计流程中通常会花费一半的资源(包括人力、时间等)在功能验证上[1,2]1这是因为验证的复杂度随着设计规模成指数地增长,而市场需求对设计周期的　收稿日期:2005-07-11;修回日期:2005-12-31要求又非常紧迫1龙芯2号是面向桌面应用的通用高性能处理器,设计规模达到6×106门,如何在相对较短的时间内确保其功能的正确性是验证人员所面临的一个巨大挑战1使用简单的、单一的验证方法已经满足不了设计验证的需求1在龙芯2号的设计验证中模拟仿真和形式化验证这两种方法得到了充分的利用1其中在系统级功能验证中主要使用的是模拟仿真的方法,而在模块级的验证中形式化方　基金项目:国家“九七三”重点基础研究发展规划基金项目(2005CB321600);国家“八六三”高技术研究发展计划基金项目(2005AA110010,2005AA119020)© 1994-2010 China Academic Journal Electronic Publishing House. All rights reserved.

张　珩等:龙芯2号微处理器的功能验证975法使用得较多1这是因为形式化验证方法在处理龙芯2号全芯片级设计验证时,由于问题规模过于庞大,还不能有效地进行验证1但是在处理模块级的电路时形式化方法的优势就充分地体现出来1正是由于在验证中使用了多种新方法和新技术,对设计进行充分而严格的验证,才确保了龙芯2号处理器的一次流片成功12　验证方法学在大规模设计验证流程中人们通常会选择自底向上的方法,即先对模块级设计进行充分的测试然后再整合到系统级进行更加全面的功能验证1对于其中主要的功能模块更是要重点地验证,比如功能部件、访存队列等1Intel奔腾处理器的FDIV错误就是由浮点功能部件产生的[3]1形式化验证方法是模块级功能验证的最佳验证方法,这是因为形式化验证方法可以100%地证明设计的正确性,在发现错误时可以给出反例1在龙芯2号的模块级验证中就大量地使用了形式化验证方法,不仅使用了成熟的等价性检验工具,也使用了AirthSMV[4]对浮点加法部件进行验证1另外,基于断言(assertion)的功能验证方法也应用到了系统总线接口和二级Cache接口的验证中1形式化验证方法在处理大规模的设计时会遇到状态爆炸的问题,所以在系统级的功能验证中还是以模拟仿真为主1模拟仿真的层次如图1所示:编写的测试程序,主要针对一些测试死角(cornercases);第2是前期相似设计中积累下来的测试向量;第3是运行实际的应用程序(例如Linux操作系统,Spec2000测试程序等);最后是使用带约束的随机生成测试向量对设计进行验证1这些方法也在龙芯2号中得到了有效的应用1模拟仿真的验证方法不能证明整个系统没有错误1验证工作是否完成的一个重要标准就是看测试覆盖率的结果是否达到了设计要求1同时在整个验证流程中始终要对覆盖率数据进行分析,并以此来指导测试生成1模拟仿真另一个缺点是随着设计的增大,仿真速度会呈指数下降,因此如何在一定的时间内运行大量的测试向量成为主要矛盾1使用FPGA物理原型验证和仿真器加速模拟仿真是一个有效的解决方法13　龙芯2号的形式化验证近几年形式化验证方法成为人们研究的热点,这也使得形式化方法取得了长足的发展,处理设计的规模不断扩大,验证效率也不断提高,许多公司已经将形式化方法和工具应用到了产品设计流程中,比如Intel和IBM等1在龙芯2号中主要应用的是等价性检验和模型检验两种方法1其中主要的工作集中在开发了用于浮点加法部件的模型检验器ArithSMV1311　浮点加法部件的模型检验器———ArithSMVArithSMV系统的结构如图2所示,ArithSMV的算法核心由两个模块组成:条件模型检验模块和可满足性判定模块,它们分别实现基于决策图的条件模型检验和基于可满足性判定算法的模型检验1Fig11　Hierarchyofsimulation1图1　模拟仿真的层次　　在龙芯2号的设计初始阶段就开发了处理器结构设计规范(architecturespecification)———C模拟器1这是一个可执行的结构设计规范,在此基础上可以进行完整的功能测试和性能评估1由于其抽象级别高,所以可以验证得更加充分1同时由于其没有二意性,又可以作为RTL设计的参考模型1这也为后续的RTL设计和验证建立了良好基础1系统级RTL的模拟仿真方法已经比较成熟,主要分为测试生成、结果检测和覆盖率分析3个部分1测试向量主要来自以下4种方法[5,6]:首先是手工Fig12　TheframworkofArithSMV1图2　ArithSMV系统框图© 1994-2010 China Academic Journal Electronic Publishing House. All rights reserved.

976计算机研究与发展　2006,43(6)　　(1)条件模型检验模块条件模型检验模块验证带有一个或多个约束子条件的规范1该模块采用了动态模型检验方法,即在模型检验的过程中动态简化被验证系统和系统规范1采用该方法对模型检验过程中生成的所有函数一旦产生,应立即调用条件约束算法计算函数在给定条件下的简化结果,并将简化后的函数替换原函数用于后续验证过程1在实现上,对于系统中任何可产生决策图的位置系统都将调用基于预处理、条件过滤机制和多级约束机制的条件约束算法1(2)条件可满足性判定模块可满足性判定模块采用可满足性判定算法进行运算电路验证1该模块首先将被验证系统和设计规范转化为SAT问题,用E2CNF表示1然后采用可满足性判定工具对E2CNF表示的SAT问题进行可满足性判定:如果SAT问题可满足,说明存在一组变量赋值使系统规范不成立;如果SAT问题不可满足,则系统规范成立1ArithSMV系统的特征在于:①采用了基于3PHDD的模型检验方法,实现了3PHDD的加法、减法、乘法、整除、取模和幂函数等操作算法以及3PHDD的比较算法;②增加了对条件模型检验方法的支持,ArithSMV采用了基于条件预处理的条件约束算法,并且提供了对多级约束机制和条件过滤机制的支持;③集成了基于可满足性判定的验证方法,ArithSMV采用E2CNF表示布尔公式和数学公式,通过可满足性判定工具判定E2CNF是否可满足1该系统在龙芯2号的浮点加法部件验证中得到了应用,并在一个中间版本中发现了错误1312　等价性检验等价性检验主要应用于物理网表与RTL设计之间的功能一致性检查1物理网表可以是初步综合的中间结果,也可以是用于流片的最终结果1同时在物理设计ECO阶段会产生大量的中间结果(物理网表),等价性检验可以非常高效地检验这些中间结果的功能一致性14　基于仿真的龙芯2号验证411　应用程序与手工测试生成以实际的应用程序作为测试向量是处理器验证中被广泛使用的方法之一1在龙芯2号的测试过程中我们也使用了操作系统和大量的应用软件作为测试向量,例如Linux,Spec2000中的paranoia和dhrystone等1另外对于设计中cornercase的验证则需要人工编写专用的测试程序作为测试向量1在龙芯2号中的func程序就是由系统专家编写的针对多种cornercase的测试程序集合1412　可配置的随机指令测试(configurablerandomprogramgenerator)随机指令生成环境由5个部分组成:指令库、可配置的规范模型、参考指令集模拟器、指令生成引擎[7]和验证仿真环境,如图3所示1系统核心是可配置系统规范和测试指令生成引擎两个组要部分1系统指令库中定义了全部龙芯2号支持的指令集,包括自定义的扩展指令等1参考指令集模拟器会根据生成引擎生成的指令运行得出正确的结果1验证仿真环境是将生成的指令序列装载到相应的内存中,根据不同的测试对处理器进行初始化,同时将仿真过程中RTL设计产生的结果与参考指令集模拟器生成的正确结果进行比较,当有错误发生时给出提示信息并终止仿真进程1另外仿真验证环境会使用功能覆盖率模型,将仿真的覆盖率分析结果输出,用来指导后续的测试生成条件1Fig13　TheframeworkofCRPG1图3　CRPG系统结构图© 1994-2010 China Academic Journal Electronic Publishing House. All rights reserved.

张　珩等:龙芯2号微处理器的功能验证977　　可配置的规范模型是由形式化的测试约束规则和翻译器组成,其中翻译器将约束规则转化为测试生成引擎的内部数据结构1规范模型定义了指令生成的约束条件,为了用户能够编写出清晰简单的生成约束条件,该规范模型将众多的约束归纳为4种基本的约束规则:①指令约束规则;②指令组和指令序列约束规则;③寄存器和访存约束规则;④初始化约束规则1测试生成引擎会根据测试规范模型生成相应的指令序列1在生成序列过程中需要处理许多问题,包括TLB换页机制、对存储空间的遍历、转移分支指令的处理、例外的生成等1在处理存储空间的遍历时我们使用了弹性边界算法,取得了非常好的效果1在实际的验证过程中CRPG对模拟仿真验证效率的提升作用非常明显,图4说明对代码覆盖率的提高效率要高于一般的模拟仿真验证1age)、条件分支的执行情况(conditioncoverage)、信号翻转执行情况(togglecoverage)和状态机执行情况(FSM)等1由于与具体设计思想联系不紧密,代码覆盖率较容易检测,几个主要的商用EDA工具软件都提供了对代码覆盖率监测的支持1基于功能的覆盖率分析则着眼于设计的功能和整体结构,常被用来监测设计者最为关注的主要设计功能和结构1由于与具体设计联系紧密,基于功能的覆盖率分析要求有详细的说明文档来描述待测的功能点,因此功能覆盖率模型也可以看做是验证计划文档另一种描述方式1随着现代设计的规模越来越大,功能覆盖率监测的工作量逐渐加大,描述功能覆盖率模型通常采用HVL(hardwareverificationlanguage)1功能覆盖率检测的全过程如下:①抽象出具体设计中待检验的功能点;②运用相关测试向量进行仿真验证,并采集覆盖率数据;③根据覆盖率检测结果调整测试向量;④覆盖率是否达到要求,如果不满足则重复②,③,直到得到预期的覆盖率检测结果1覆盖率分析在以下方面可以提高验证的质量和效率:①检测出不合法的事件,从而帮助发现设计中的缺陷;②覆盖率结果可以告诉验证人员验证程序中的状态信息,从而帮助发现验证的漏洞,例如,某块区域没有被覆盖到;③验证测试向量是否已经重复,没有新的进程被覆盖;④帮助验证程序更直接驱动测试生成程序产生测试向量,测试没有被覆盖到的区域,填补验证的漏洞1龙芯2号的覆盖率分析包括两部分:①代码覆盖率的检测由商业EDA软件支持,表1列出了几个测试程序针对不同模块的代码覆盖率;②功能覆盖率则手工完成,需要根据被测设计的特点建立覆盖Table1　SomeResultsofCodeCoverageFig14　Linecoverage1图4　行代码覆盖率比较413　验证覆盖率基于仿真的验证方法面临两大困难:①难以监测验证进程;②难以判断验证质量1换句话说,基于测试向量模拟仿真的验证方法,无论采用的测试向量来自真实应用还是随机测试产生器,都无法证明整个系统没有错误1验证工作是否完成的一个重要指标就是看覆盖率的结果是否达到了预期的要求1在整个验证流程中始终保持对覆盖率数据进行监测和分析并以此来指导测试向量的生成和整个仿真过程1覆盖率分析大致分两种:一种是基于代码的覆盖率分析,另一种是基于功能的覆盖率分析1基于代码的覆盖率主要是测试执行语句的情况(linecover2表1　多个程序的代码覆盖率ModuleDecoderRoqueueGRFRProgrammFunc99989697Linux95899054Paranoia94868090%Dhrystone95909490© 1994-2010 China Academic Journal Electronic Publishing House. All rights reserved.

978计算机研究与发展　2006,43(6)率模型,进行模拟真实系统环境的功能仿真,应尽可能地模拟出实际中会遇到各种情况,使得被测代码全部功能被执行,从而解决逻辑上的错误1414　基于断言的验证基于断言的验证方法被越来越多地应用到处理器的设计验证中1使用断言描述设计的功能属性,然后在仿真过程中检测这些断言属性是否被触发1断言属性即可以作为结果检测器也可以作为功能覆盖率模型使用1在龙芯2号中开发了针对系统总线接口和二级Cache接口的接口协议检测器(protocolchecker),提高了验证效率1调试能力,很好地填补了FPGA物理原型验证速度快、难调试和软件模拟器调试能力强但速度慢两种仿真层次之间的空白1Table2　ResultsofSimulationAcceleration表2　使用仿真器加速的运行时间比较SimulationModeSimulation(VCS)Acceleration(VStation)ProgramFunc2895489Linux226931890Whetd365772146sStream3261436896　总结和未来工作5　仿真加速对于现今大规模的ASIC设计和SoC来说,使用软件模拟器进行RTL仿真的运行速度慢是主要瓶颈,而且很难再有本质的突破,这就需要通过硬件加速的方法来提高仿真速度1使用硬件加速仿真的方法有很多,主要的方法包括物理原型验证(prototyping)、ICE(in2circuitemulator)方式和仿真器的仿真加速1目前龙芯2号的设计验证中使用了物理原型系统验证方法,首先将设计经过分片、综合、布局布线后烧入到FPGA中,再将FPGA通过子卡集成到系统开发板上运行实际的操作系统和大量的应用软件,这种方法完全不需要软件的参与进行模拟,所以可以取得最大的模拟仿真速度1该方法的优点是快速的运行速度,可以在较短的时间内测试大量的测试向量;工作在实际的目标系统中,测试环境更加真实,可同时进行系统的验证;可以在进行硬件设计的同时进行系统的软件开发1但是这种方法的一个主要缺点是发现错误后,调试非常困难,只能依靠逻辑分析仪和示波器等工具,可观测信号的时间窗口范围也很小,对设计内部的信号观测困难,分析一个错误要花费很多时间1如果将一个在FPGA上发现的错误在软件模拟器上重现,需要相当长的时间1在FPGA上运行一秒钟的向量在软件模拟器上要运行正是由于使用了上述多种验证方法和技术,从而保证了龙芯2号处理器的一次流片成功1随着龙芯系列处理器的发展,如何确保更大规模设计的功能正确性,仍然是一个需要深入研究解决的难题1在模块级验证中更多地引入形式化方法,开发出用于其他功能部件的功能更强大效率更高的模型检验器是未来研究的重点;同时在系统级的指令测试生成中使用自动的覆盖率驱动测试生成,进一步提高验证的效率、降低人工的工作强度也是今后的努力方向1参1考文献F1Casaubieilh,etal1FunctionalverificationmethodologyofChameleonprocessor1The33rdDesignAutomationConference,LasVegas,19962A1Aharon,D1Goodman,M1Levinger,etal1TestprogramgenerationforfunctionalverificationofPowerPCprocessorsinIBM1The32ndDesignAutomationConference,SanFrancisco,19953H1P1Sharangpani,M1L1Barton1StatisticalAnalysisofFloat2ingPointFlawinthePentiumProcessor1SantaClara:IntelCor2poration,19944WangHaixia1Reserchonfromalmethodsinarithmeticcircuitver2ification:[Ph1D1dissertation]1Beijing:InstituteofComputingTechnology,CAS,2004几个小时或十几个小时1所以要求有一种方法即能够提供很高的仿真速度又能提供很好的调试环境1硬件仿真加速器就是惟一的选择1目前有两种硬件仿真加速器:基于处理器阵列的仿真加速器和基于FPGA的仿真加速器1龙芯2号选择的是基于FP2GA的仿真加速解决方案1表2给出了使用仿真器5J1Monaco,D1Holloway,R1Raina1FunctionalverificationmethodologyforthePowerPC604microprocessor1The33rdDe2signAutomationConference,LasVegas,199667M1Kantrowitz,L1M1Noack1I’mdonesimulating;Nowwhat?The33rdDesignAutomationConference,LasVegas,1996ShenHaihua,MaLin,ZhangHeng1CRPG:Aconfigurableran2domtest2programgeneratorformicroprocessors1ISCAS’05,Kobe,Japan,2005进行仿真加速的效果1该仿真加速器可以提供20～50倍仿真加速,同时也提供了近似于软件模拟器的© 1994-2010 China Academic Journal Electronic Publishing House. All rights reserved.

张　珩等:龙芯2号微处理器的功能验证ZhangHeng,bornin19731ReceivedhisB1A’sdegreeinmechanicalengineeringfromtheSoutheastUniversity,Nanjing,China,in19951ReceivedhisM1S’sdegreeincom2putersciencefromtheUniversityofScienceandTechnologyofAnshan,China,in20001Since2001,hehasbeenaPh1D1candidateintheInstituteofComputingTechnology,theChineseAcademyofSciences,Beijing,China1Hiscurrentresearchinterestsincludecomputerarchitectureandprocessordesign,verificationandtest1979ShenHaihua,bornin19711AnassociateprofessorintheInstituteofComputingTechnology,theChineseAcademyofSci2ences1ShereceivedherPh1D1degreeincomputerscienceandengineeringfromTs2inghuaUniversity1Hermainresearchinterestsincludecomput2erarchitecture,processordesignandverification1沈海华,1971年生,毕业于清华大学计算机科学与技术系计算机体系结构专业,获博士学位1现为中国科学院计算技术研究所副研究员,主要研究方向为计算机体系结构、微处理器设计与验证(shenhh@ict1ac1cn)1张珩,1973年生,博士研究生,主要研究方向为计算机体系结构、微处理器设计、功能验证与测试1ResearchBackgroundTheimportanceofmicroprocessordesignverificationiswidelyacknowledged1HowtopromotetheverificationtaskandbebugsfreepriortosiliconisacriticalprobleminGodson22design1ThereareabouttenpeopleintheGodson22grouptostudytheverifica2tionmethodologyandtechnology1OurworkissupportedbytheNationalScienceFoundationofChina(60325205),863Hi2TechRe2searchandDevelopmentProgramofChina(2002AA110010),andtheKnowledgeInnovationEngineeringProjectofChineseAcade2myofSciences(KGCX2-109)1《计算机科学技术学报》(JCST)简讯2005年,JCST已改为210×285大16开本,平均每期144页1版面的增加,信息量随之增大,在一定程度上满足了读者和作者的需求1此外,2005年起,本刊每期都有专题栏目和综述文章,敬请大家关注1近期发表文章和专题预告如下:・“ProgressinComputationalComplexityTheory”byProf1Jin2YiCaiofUniversityofWisconsinandProf1HongZhuofFudanUniversity・“RecentAdvancesinEvolutionaryComputation”byDr1YongXuandProf1XinYaoofTheUniversityofBirmingham・SpecialIssueonDataManagementeditedbyProf1ShanWangRenminUniversityandProf1Jian2ZhongLiofHarbinInstituteofTechnology・SpecialIssueonDigitalAudioΠVideoTechnologyinChina—EmergingChinaAVSVideoCodingStandardeditedbyProfessorsFengWuofMicrosoftResearchAsiaandHuifangSunofUniversityofMitsubishiElectricResearch本刊的审稿周期约三个月至半年,录用率为10%～15%1自2000年JCST被SCI收录以来,在本刊发表的文章100%被SCI的WebofScience,ResearchAlert,CompuMathCitationIndex收录;同时,在本刊发表的文章95%以上被Ei的Compendex收录1欢迎大家踊跃投稿与订阅1本刊的邮发代号:225781CCF会员和个人订户可以在编辑部优惠订阅,详情请见JCST网站,网址:http:∥jcst1ict1ac1cn1编辑部联系地址:北京2704信箱《JCST》编辑部,邮编:100080电话:　　E2mail:jcst@ict1ac1cn© 1994-2010 China Academic Journal Electronic Publishing House. All rights reserved.