最新大规模集成电路验证Whyverificationandtools教学课件.ppt

大规模集成电路验证Whyverificationandtools验证部分的授课内容除VLSI设计之外的全部内容均是验证设计 vs.验证(design vs.Verification)验证 vs.测试 (Verification vs.Test)投片前验证 vs.投片后验证(Pre-Silicon vs.Post-Silicon)Verfication,Validation,Testing参考资料课程教材集成电路计算机辅助设计与验证实践/算法Hardware Design Verification:Simulation and Formal Method-Based Approaches.Prentice Hall PTR.ISBN:0131433474全面的功能验证：完整的工业流程 Comprehensive Functional Verification:The Complete Industry CycleProceedings:DAC,DATE,HLDVT,ITCVerification vs.TestingVerification检验设计的正确性主要方法为模拟、硬件仿真和形式化方法在设备制造之前多次重复，但对一个设计仅一次完整正确验证为设计的质量负责Testing检测生产结果的正确性分两个步骤：设计期间产生测试；生产后应用测试对生产出来的每个产品均完成一次测试对器件的质量负责Why we need VerificationExample 1 1980北美防空司令部误报遭受导弹袭击检测反馈电路故障检测反馈软件对故障未处理，直接报告预警Possible World War IIIExample 2 1996年阿丽亚娜5火箭爆炸64位双精度浮点操作转换为16位整数时产生的例外重新设计的计算节点板完全重用阿丽亚娜4软件代价$800M 4颗Cluster卫星Why we need VerficationExample 3 Intel Pentium处理器FDIV除法错误Pentium处理器在双精度运算时有时会返回单精度的结果代价$400M 所有产品召回如何展开验证设计的每个步骤都对应着验证只有描述转换的过程就对应着验证系统级设计RTL设计概念设计逻辑综合可测性设计物 理设计signoff投片系统级模拟功能模拟验证概念检测 验证计划网表模拟 反 标模拟 一致性检查一致性检查门级模拟 物 理验证超 标量？Pipeline,FP,L2C 多核？异构？综 合后结果功能、时序正确性增加DFT MBIS是否影响功能是否符合设计和工艺规则DRC LVS Antenna 主要的验证方法Functional verificationSimulationHardware emulationFormal methodsArithmetic verificationProperty checkingEquivalence checkingTheorem proverLanguage containmentSymbolic model checkingSymbolic trajectory evaluation两种主要的验证方法基于模拟的方法，适用于所有设计层次circuit simulation(e.g.Spice)switch and transistor level simulation(e.g.Cos-mos)gate level simulation(e.g.IUS/VCS)register transfer level simulation(e.g.IUS/VCS)behavioral or system level simulation(e.g.Ptolemy,PD).Architecture or conception(e.g.systemC,PD)形式化方法理论上最佳的验证方法，数学方法受限于问题规模模拟验证与形式化验证模式模拟验证平均对待每一种可能和输入时间受限可能不完备输入驱动形式化验证将系统和属性分类分隔子系统内必定完备输出驱动模拟验证的主要流程模拟方法：正确的输入得到正确的输出根据设计描述获得验证计划，构造激励，预测预测结果构建测试平台TestBench实例化待测设计DUT用激励驱动DUT运行检查DUT是否获得正确结果模拟运行，反馈设计修改回归测试，固定设计版本形式化验证的流程从设计中获得待验证特性抽象或者描述特性特性检查或者等价性检查可能的人工指导或模拟增加、修订或删除限定条件调试调整设计或抽象描述模拟验证方法最常用的验证方法，输入驱动Input vectorDirected伪随机模拟器事件驱动基于周期的硬件模拟器：使用硬件对电路建模0010100101010001110101001110101010100000000011101011011011110111Simulation-based Verification Execute the system in parallel with a reference modelwith respect to some input sequences.test suiteas exhaustive as possible模拟Find bugs by executing the implementation and checking its behavior四要素：circuit,test pattern,reference output,comparison mechanismRequirementsSimulateRTL ModelGate-levelModelSynthesizeSimulateTest BenchASIC or FPGAPlace&RouteTimingModelSimulate“Youcanprovethepresenceofbugs,butyoucannotprovetheirabsence.”如果找到一个 不一致，就可以证明设计有错不能证明没 有不一致(没人可以证明UFO不存在)基于形式方法的验证形 式验证等价性检查模型检验定 理证 明等价性检查Compare two models Mathematically prove that the origin and output are logically equivalent and the transformation preserved its functionalityIt can compare two netlists to ensure that some netlist post-processing,such as scan-chain insertion,clock-tree synthesis,or manual modification,did not change the functionality of the circuit.等价性检查：两个实现是否等价为 缩小搜索空间，用户可以定义等价点两种方法SAT：系统搜索输入空间将两种电路转化为唯一表示，并进行比较常用场合：Scan insertion前 后Layout与RTL的 一致性ECO前 后模型检验Look for generic problems or violation of user-defined rules about the behavior of the design.Assertions or characteristics of a design are formally proven or disproved.All state machines in a design could be checked for unreachable or isolated states.To determine if deadlock conditions can occur模型检验System A mathematical model MDesired behavior A formal specification The system has the required behaviorM satisfies Model checking模型检验形式地证明设计的断言和特征，如状态机是否可达、是否死锁、接口的断言搜索整个状态空间，找到属性不满足的点，如果找到，则失败隐式枚举状态空间：符号遍历算法，一次访问一组点，提高效率Unbound propertyBound property两种方法的比较SimulationSimulate the design with test stimuli and check the resultsInput output compare expected resultOnly a small part of the space can be exploredHard to tell if testing is sufficientFormalProving facts about the designModel checking,Equivalence checkingExpected behavior property proveTime and space issuesHard to tell if properties are complete例 1：4位加法器adder4ba3:0b3:0sum3:0c_out44c_in4module adder4b(sum,c_out,a,b,c_in);input 3:0 a,b;inputc_in;output3:0 sum;outputc_out;assign c_out,sum=a+b+c_in;endmoduleSimulation Exampleadder4b(DUT)a3:0b3:0sum3:0c_out44c_in4t_adder4bTestbenchtimescale 1ns/1ns /time_unit/time_precisionmodule t_adder4b;reg8:0 stim;/inputs to DUT are regswire3:0 S;/outputs of DUT are wires wire C4;/instantiate DUTadder4b(S,C4,stim8:5,stim4:1,stim0);/stimulus generationinitial begin stim=9b000000000;/at 0 ns#10 stim=9b111100001;/at 10 ns#10 stim=9b000011111;/at 20 ns#10 stim=9b111100010;/at 30 ns#10 stim=9b000111110;/at 40 ns#10$stop;/at 50 ns stops simulationendendmodulesee“response”to each of these input vectorsUUTBehav.Verilog:“do this once”timing control for simulationTestbench RequirementsInstantiate the Design Under Test(DUT)Provide input to that unitUsually a number of different input combinations!Watch the“results”(outputs of DUT)Can watch Wave windowCan print out information to the screen or to a filetimescale 1ns/1ns /time_unit/time_precisionmodule t_adder4b;reg8:0 stim;/inputs to DUT are regswire3:0 S;/outputs of DUT are wires wire C4;/instantiate DUTadder4b(S,C4,stim8:5,stim4:1,stim0);/monitor statementinitial$monitor($time,C4,S,stim8:5,stim4:1,stim0);/stimulus generationinitial begin stim=9b000000000;/at 0 ns#10 stim=9b111100001;/at 10 ns#10 stim=9b000011111;/at 20 ns#10 stim=9b111100010;/at 30 ns#10 stim=9b000111110;/at 40 ns#10$stop;/at 50 ns stops simulationendendmoduleExhaustive Simulation综综 合后合后module adder4b(sum,c_out,a,b,c_in);output 3:0 sum;input 3:0 a,b;input c_in;output c_out;wire carry1,carry2,carry3;ADD32 U1_0 (.A(a0),.B(b0),.CI(c_in),.CO(carry1),.S(sum0);ADD32 U1_1 (.A(a1),.B(b1),.CI(carry1),.CO(carry2),.S(sum1);ADD32 U1_2 (.A(a2),.B(b2),.CI(carry2),.CO(carry3),.S(sum2);ADD32 U1_3 (.A(a3),.B(b3),.CI(carry3),.CO(c_out),.S(sum3);endmodulemodule ADD32(A,B,CI,CO,S);input A,B,CI;output CO,S;and(net_1,CI,B);and(net_2,CI,A);and(net_3,B,A);or(CO,net_1,net_2,net_3);xor(S,CI,B,A);endmodule如何验证综合后网表的正确性？Consistency:same testbench at each level of abstractionBehavioralGate-level Design(Post-layout)Gate-level Design(Pre-layout)RTL DesignTestbenchSimulation方法 1：Gate-level simulationGiven two designs,prove that for all possible input stimuli their corresponding outputs are equivalentDesign ADesign B=?InputYes/NoProduct Machine 方法 2：Equivalence Checking例 2：交 通灯控制器Guarantee no collisions：It is never possible that all traffic lights are greenGuarantee eventual serviceEventually,each traffic light will become greenESNVerilog programmodule main(N_SENSE,S_SENSE,E_SENSE,N_GO,S_GO,E_GO);input N_SENSE,S_SENSE,E_SENSE;output N_GO,S_GO,E_GO;reg NS_LOCK,EW_LOCK,N_REQ,S_REQ,E_REQ;/*set request bits when sense is high*/always begin if(!N_REQ&N_SENSE)N_REQ=1;end always begin if(!S_REQ&S_SENSE)S_REQ=1;end always begin if(!E_REQ&E_SENSE)E_REQ=1;end /*controller for North light*/always begin if(N_REQ)begin wait(!EW_LOCK);NS_LOCK=1;N_GO=1;wait(!N_SENSE);if(!S_GO)NS_LOCK=0;N_GO=0;N_REQ=0;end end/*South light is similar.*/*Controller for East light*/always begin if(E_REQ)begin EW_LOCK=1;wait(!NS_LOCK);E_GO=1;wait(!E_SENSE);EW_LOCK=0;E_GO=0;E_REQ=0;end end 如何验证？方法方法2：模型检验模型检验Traffic LightControllerDesign“It is never possible to have a green light for both N-S and E-W.”ModelCheckerTrueFalse+Counterexample方法1：模 拟Safety(no collisions)AG (E_Go(N_Go|S_Go);LivenessAG(N_Go N_Sense AF N_Go);AG(S_Go S_Sense AF S_Go);AG(E_Go E_Sense AF E_Go);Fairness constraintsinfinitely often (N_Go N_Sense);infinitely often (S_Go S_Sense);infinitely often (E_Go E_Sense);All properties verifiedGuarantee no collisionsGuarantee service assuming fairnessComputational resources used:57 states searched0.1 CPU seconds可以通过并行、抽象和自动化减 少验证时间并行：采用更多的资源，设计实现与验证并行；验证编码与调试并行抽象：不关心低层次细节，事务级、总线周期级自动化：需要标准化的过程；目前没有通用的标准化方法；有些验证过程可自动化2/10/03ECE 426-Lecture 549另 一种 分类方法Black boxVerify using module I/O ports onlyNo knowledge of implementationNo access to internalsWhite boxVerify using module I/O ports and internalsFull knowledge of implementationFull access to internals during simulationGray boxVerify using module I/O ports onlyFull knowledge of implementationNo access to internals during simulation5 验证的代价Verification is a necessary evil.时间长，代价大验证本身不能盈利卖的是设计，而不是验证Verification is a process that is never truly complete.Verification can only show the presence of errors,not their absence.It costs more and more to find fewer and fewer errors.Question:how much is enough?验证何时终止？Emotionally,or Intuitively;Out of money?Exhausted?Competitions product is there.Software people are happy with your hardware.There have been no bugs reported for two weeks.More rigorous criteria;All tests passedTest Plan CoverageFunctional CoverageCode CoverageBug Rates have flattened toward bottom.Part.2 Testbench Simulator使用模拟工具Lint工具语法检查基于事件的模拟工具基于周期的模拟工具基于硬件原型的模拟工具检查与调试Linter 工具1/8发现共同的编程错误快速静态的RTL代码检查参数和功能调用间不匹配的类型，参数数目不匹配在执行程序前发现错误静态工具53int my_func(addr_ptr,ration)int *addr_ptr;float ration;return(*addr_ptr)+;main()int my_addr;my_func(my_addr);Linter 工具2/8:举例Lint输出Src.c(3):warning:argument ration unused in function my_funcSrc.c(11):warning:my_addr may be used before set to invocation environment54 int my_func(addr_ptr)int*addr_ptr;return(*addr_ptr)+;main()int my_addr;my_func(&my_addr);return 0;Linter 工具3/855Linter 工具4/8：局限性只能发现特定类型的问题，不能发现所有问题只能发现代码结构方面的问题，不能发现算法和数据流的问题拼写检查：不能查出用错的词过于严格，可能报一些并不存在的问题错误信息的过滤可以在写完代码后立即运行lint工具56Linter 工具5/8Verilog源代码的 lintVerilog更象汇编和 basic语 言，无类型语言，可以对任意寄存器赋任意值Verilog的 linter可以发现公共的问题。57Linter 工具6/8问题 宽度不匹配，verilog 0扩展58Linter 工具7/859Linter 工具8/8：实例60部分硬件仿真器与形式化验证工具ProDesign公司的CHIPitEve公司的ZeBuCadence公司的Incisive Verification、Incisive Formal Verifier、Xtreme IIICHIPitProdesign是德国的一家公司 原型验证系统 CHIPit Platinum Edition V4 CHIPitCHIPit Platinum Edition V4是一个针对大规模芯片设计而开发的原型验证系统。最大配备21个FPGA芯片验证规模可达2000万至3000万，系统速度最高可达200Mhz。CHIPit主要功能和特点 1.适合大规模设计的架构 多层板体系架构和3-D Switching互连技术 2.支持多种验证模式 原型系统验证，模拟加速 3.便利的调试工具 FPGA探针制作方便,Readback功能,VCD 文件供波形浏览器查看 CHIPit4.原型验证流程自动化管理5.其它特点系统时钟可方便地通过软件进行配置；具有JTAG、PCI、PCIX、PCI-Express、USB、DVI、Ethernet等系统接口；配备板上memory或SSRAM、SDRAM、DDR SDRAM、DDR2 SDRAM等memory扩展子板；可通过Ethernet或者CF卡来配置系统。CHIPit与Hardi的比较 FPGA之间的互连 技术软件设置时钟频率和进行复位 Readback功能访问所有的寄存器 支持transation验证模式 集成了项目管理、综合、布线、延时分析、下载、调试、仿真、Co-simulation等软件环境 CHIPit和Hardi的互连接口相同，可以通过电缆连接CHIPit和Hardi。CHIPit缺点CHIPit的电压统一为3.3V，增加了子板设计难度和成本，引入了电平转换的延时。CHIPit的CO-Simulation功能是2006年底才新增加的功能，缺乏现成的Transactor，其CO-Simulation的能力还有待验证。CHIPit无法对BlockRam中的数据进行读取。ZeBuEve是法国的一家公司硬件加速器方面的产品主要有Hammer和ZeBu两个系列Hammer是基于处理器的硬件加速器ZeBu是基于FPGA的硬件加速器。ZeBu第三代产品是ZeBu-UF，最大支持600万门；第四代产品是ZeBu-XXL，最大支持1亿门 最新产品Zebu-Server/Blade，200M*10ZeBu-UFZeBu-UF是基于Xilinx V4LX系列构建的一块PCI扩展卡 最大支持600万门，最高速度可达200MHz ZeBu-UF1.验证模式ZeBu-UF能支持多种验证模式基于信号级的C/C+/SysemC基于事务级的C/C+/SysemC/SystemVerilog基于测试向量的模拟加速基于STB的在线仿真基于DirectICE的在线仿真、以及基于SmartICE的在线仿真 ZeBu-UF2.调试能力动态探针和静态探针两种调试手段动态探针对模拟速度的影响较大 对于在线仿真，ZeBu还提供了类似逻辑分析仪的HW trigger来控制时钟和trace memory。ZeBu-UF3.较丰富的Transactor和存储器模型 TransactorUART、LCD、PCI Express、Ethernet、AHB、USB、Firewire、JTAG等等SDR、DDR、DDR2、DIMM SDR/DDR/DDR2、Flash ZeBu-UF软件资源综合时需要调用Synplify，并有自己的编译工具对综合后的网表进行优化ZeBu的编译器会自动对设计进行划分，并完成相应的综合、映射和布局布线 ZeBu实用评测ZeBu的加速性能易用性调试能力 ZeBu实用评测ZeBu-UF2，最大支持300万门HOST采用Xeon 3G的CPU，内存4G，IDE硬盘。测试对象为L2C与MI联合测试环境的FPGA版本，外围测试环境包括测试激励和DDR2模型。DUT规模小于100万门，因此不必进行FPGA划分。ZeBu实用评测1.ZeBu-UF2插入HOST的PCI插槽所遇到的问题2.统一设计顶层问题3.IDDR与ODDR问题4.IDELAY问题5.LUT4问题:对于所有由FPGA内部器件实现的延迟功能，ZeBu都不支持 6.DDR2模型问题ZeBu实用评测测试结果0300us300us1000usL2C与MI运行在HOST上5m17mL2C与MI运行在ZeBu-UF2上2.5m12m加速比50%29%ZeBu实用评测测试结果CO-Simulation过程中动态探针对模拟速度有较大的影响。加入动态探针的CO-Simulation模拟速度甚至比只在HOST上运行且记录波形的模拟速度还要慢 XtremeIIICadence公司的硬件加速器PalladiumXtreme两个系列 XtremeIIIXtreme III最大支持7200万门 400kHz-800kHz板上存储器容量为18GB最多能支持最多能支持12个用户同时使用个用户同时使用 XtremeIII1.验证模式支持多种验证模式包括基于信号级的模拟加速基于事务级的SystemC/C/C+/e模拟加速基于断言的模拟加速,不支持基于PSL的模拟加 速，但Palladium III支持各种在线仿真 XtremeIII2.调试能力 相对较强readmemh和writememh查看和修改存储器单元；printf（）或$display（）语句实时输出消息snapshot Hot-Swap功能 XtremeIII3.软件资源与Cadence软件验证环境集成在一起，能利用SimVision查看波形，进行事务和断言调试、具有软硬件联合调试功能和覆盖率统计功能 4.TBA VIP提供了较为丰富的基于事务加速的验证IP，包括PCI Express、Ethernet、AMBA、AHB、AXI等等 与与ZeBu的比较的比较1.都不能处理使用都不能处理使用FPGA中的器件来实现逻辑功能中的器件来实现逻辑功能2.ASIC的的 库库 单单 元元 模模 拟拟 模模 型型 一一 般般 都都 会会 使使 用用 UDP，Xtreme III能能自自动动将将UDP映映射射为为硬硬件件，从从而而使使得得加加速速ASIC库单元成为可能，而库单元成为可能，而ZeBu不具备此功能不具备此功能 3.Xtreme III支持通过层次方式直接访问位于加速器的DUT中的信号，而ZeBu不具备此功能 与与ZeBu的比较的比较4.Xtreme III能通过能通过Hot-Swap功能方便查错和执行不功能方便查错和执行不能被加速的激励，而能被加速的激励，而ZeBu不具备此功能。不具备此功能。5.Xtreme III能将断言映射为硬件，从而能进行基于能将断言映射为硬件，从而能进行基于断言的加速，而断言的加速，而ZeBu不具备此功能。不具备此功能。6.ZeBu-UF2支持支持STB，但要求测试激励必须是可综合，但要求测试激励必须是可综合的的,Xtreme III允许测试激励不一定都是可综合,也能加速IFV断言断言:监测设计中正确行为或错误行为的验证对象监测设计中正确行为或错误行为的验证对象。断言将设计要求转换成了验证对象，从而可以用模拟器或形式化验证工具，评测设计要求是否被满足 IFV断言可分为三种，断言可分为三种，第一种为第一种为Assertion，用于描述设计所期望的正确行，用于描述设计所期望的正确行为；为；第二种为第二种为Constraint，用于描述设计所处环境的行，用于描述设计所处环境的行为；为；第三种为第三种为Cover，用于描述设计及其所处环境应该，用于描述设计及其所处环境应该会到达的状态会到达的状态。IFV形式化验证的结果形式化验证的结果FailPassExplored IFV与模拟相比与模拟相比形式化验证不需要编写测试激励，只要断言编写完整，形式化验证不需要编写测试激励，只要断言编写完整，就能完全验证设计的正确性就能完全验证设计的正确性它还能发现模拟所不容易查出的错误它还能发现模拟所不容易查出的错误形式化验证的有效性依赖于断言形式化验证的有效性依赖于断言 适合进行模块级的验证和对控制逻辑进行验证，否则可能会因状态空间过大而无法在规定时间内完成验证。IFV支持支持PSL和和SVA两种断言两种断言SVA是是SystemVerilog的断言，比较适合用的断言，比较适合用Verilog编写的编写的RTL代码，代码，SVA是免费的，而是免费的，而PSL需要购买。需要购买。SVA的不太适合验证异步时钟接口的不太适合验证异步时钟接口PSL比较适合用比较适合用VHDL编写的编写的RTL代码。代码。PSL的断言可以用于验证异步时钟接口。的断言可以用于验证异步时钟接口。PSL的断言功能比的断言功能比SVA要强，例如，要强，例如，PSL支持具有支持具有Liveness功能的断言，但功能的断言，但SVA不支持不支持 IFV提供了一些形式化验证IP（FVIP）目前Cadence公司提供的FVIP有OCP2.0、AHB和AXI IFV与0in比较在验证失败需要给出出错波形进行调试时，0-IN需要testbench通过模拟的方式生成波形，而IFV不需要testbench而快速生成波形。0-IN对VHDL的支持处于Beta阶段，并且也不支持混合语言，但IFV完全支持VHDL，且也支持混合语言。Cadence在中国具有训练有素的形式化验证方面的工程师，而Mentor没有。IFV支持在断言中直接使用层次化信号名，而0-IN不支持。IncisiveVerificationCadence公司推出的一整套验证解决方案 验证自动化验证自动化的流程 它的基础是Incisive Plan-to-Closure Methodology（IPCM）IncisiveVerificationPlan：即根据给出的设计要求制定可执行的验证计划、确定覆盖标准、安排人力和机器资源并分派验证任务。Execute：根据验证计划建立验证环境、构建验证组件、自动生成测试激励，并进行软模拟、形式化验证、模拟加速以及在线仿真。Measure：分析验证结果和整个覆盖率，并与验证计划进行对照。React：根据验证结果和与验证计划对照的情况，修正设计和测试环境的错误、调整验证计划以及人力和机器资源安排。重复上述过程直到验证收敛。IncisiveVerification为了提高测试程序的开发效率，IPCM强调测试激励的自动生成和验证组件的可重用性 Cadence公司提出了 uRM（Universal Reuse Methodology）Cadence公司提供了丰富的已开发好的uVC，包括PCI-E、AHB、Ethernet、MAC、Datalink、ARM、USB、UART、ALU等等。uVC主要由Driver、Monitor和BFM构成。Driver用于产生测试序列，并将之传递给BFM vBuilder:帮助用户开发uVC Part.4 OpenSPARC简介SUN UltraSPARC模拟与验证介绍OpenSPARC T1/T2 代码环境硬件测试验证平台SIMS体系结构级模拟环境SAM现状与未来Sun 模拟与验证Sun 的功能验证（不包括时序和物理设计验证）处理器体系结构设计验证RTL设计模拟验证DFT验证系统级环境验证固件、操作系统和各类驱动使用工具软模拟、加速器仿真、形式化验证商业工具+定制工具Sun 功能模拟与验证流程处理器设计验证流程Sun 模拟与验证环境开发开发语言Verilog 继承/惯性（T1）（主要RTL模型）System Verilog（T2/T3）Vera（覆盖率测试与随机测试）模拟验证环境模块级 SAT(Stand Alone Test)系统级 (全自动回归测试Regression)全处理器RTL模型存储子系统系统级TestbenchAssertionsMonitor(协议检测、辅助调试)Sun 验证的核心 -仿真软模拟速度限制，形式化验证的规模限制基于Xtrem的Virtual Silicon 仿真验证(10,000+VCS)多种metricRTL Stablility,Bug,CoverageSun 仿真验证原因系统级设计包括：处理器RTL、存储子系统、系统组件和TestbenchUltraSPARC T1 系统级模型 3千5百万门（超过所有形式化验证工具能力）软模拟器 一秒模拟一个周期仿真与加速仿真 In-Circuit 接口存放目标系统加速(高速模拟器)Sun同时使用了两种方式Palladium Xtreme以Xtreme为中心Sun 基于Xtreme的仿真验证减少新设计提交时间（hot-swap VCS-Xsim）简化、加速模型初始化(forces，PLI和constom system tasks)端模拟器Xsim中运行模型初始化，swapping到硬件中全速运行Sun 仿真验证 cont.Sun基于Xtreme的仿真验证（续.）快速Check-Pointing运行时保存snapshots(恢复波形、调试)Xtreme与Sun定制模拟环境集成Sun定制的Xtreme任务调度器（improve productivity）仿真为核心的验