大规模集成电路验证.ppt

《大规模集成电路验证.ppt》由会员分享，可在线阅读，更多相关《大规模集成电路验证.ppt（120页珍藏版）》请在三一办公上搜索。

1、VLSI Design and Verification大规模集成电路设计与验证,VLSI Verfication大规模集成电路验证,验证部分的授课内容,除VLSI设计之外的全部内容均是验证设计 vs.验证(design vs.Verification)验证 vs.测试(Verification vs.Test)投片前验证 vs.投片后验证(Pre-Silicon vs.Post-Silicon)Verfication,Validation,Testing参考资料课程教材集成电路计算机辅助设计与验证实践/算法Hardware Design Verification:Simulation and

2、 Formal Method-Based Approaches.Prentice Hall PTR.ISBN:0131433474全面的功能验证：完整的工业流程 Comprehensive Functional Verification:The Complete Industry CycleProceedings:DAC,DATE,HLDVT,ITC,验证部分课程学习组成,课程讲授|HOME实验作业 考试掌握原理的基础上强调实践验证原理，工具算法原理工具Synopsys VCS,Cadence IUS/IES,Mentor ModelSIMIFV,ZeroIn,SpyGlass,Conform

3、al,FomalityDC,RC,ICC,Encounter,TessentOffice Hour唐遇星，副研究员yuxing.微电子与微处理器研究所微处理器研究室619Monday Tuesday:20:00 22:00 and weekend302 计算机工厂停车场北楼,Agenda,Part 0.WelcomePart 1.Verfication IntroductionPart 2.Testbench Simulation ToolPart 3.Testbench Construction and OpenSPARC,Part.0 Welcome,Welcome 领域Welcome 校

4、园Welcome 课程,Part.1 Introduction,What?什么是验证？Why?为什么要验证？How?如何开展验证？验证包括哪些内容主要的验证方法验证的困境,What is Design Verification什么是验证,The Opposite of DesignDesign:Make/Implement sth that you wantVerification:Make sure that sth is what you want(correct)确保设计符合原始设计需求与目标功能正确，性能达标，功耗、良率和成本符合要求VLSI团队分工 Design Team&Verif

5、ication TeamAt least 1:1,Now 1:3 1:4Time Statistic:30%Design,70%VerficationHint:设计人员必须完成初始验证才能提交设计；但一个设计的必须由额外的验证人员审核,Design,Verification and Testing,Design Synthesis设计综合根据设定的输入输出功能，使用现有的方法、技术、材料和工艺制造设备的过程Verification验证预测并保证设计与综合在制造过程乎能够根据输入输出完成功能Test 测试用于保证按照设计综合结果来生产的器件，不受制造错误影响,Verification vs.Te

6、sting,Verification检验设计的正确性主要方法为模拟、硬件仿真和形式化方法在设备制造之前多次重复，但对一个设计仅一次完整正确验证为设计的质量负责Testing检测生产结果的正确性分两个步骤：设计期间产生测试；生产后应用测试对生产出来的每个产品均完成一次测试对器件的质量负责,Why we need Verification,Example 1 1980北美防空司令部误报遭受导弹袭击检测反馈电路故障检测反馈软件对故障未处理，直接报告预警Possible World War IIIExample 2 1996年阿丽亚娜5火箭爆炸64位双精度浮点操作转换为16位整数时产生的例外重新设计的

7、计算节点板完全重用阿丽亚娜4软件代价$800M 4颗Cluster卫星,Why we need Verfication,Example 3 Intel Pentium处理器FDIV除法错误Pentium处理器在双精度运算时有时会返回单精度的结果代价$400M 所有产品召回,如何展开验证,设计的每个步骤都对应着验证只有描述转换的过程就对应着验证,系统级设计,RTL设计,概念设计,逻辑综合,可测性设计,物理设计,signoff投片,系统级模拟,功能模拟验证,概念检测 验证计划,网表模拟 反标模拟 一致性检查,一致性检查,门级模拟 物理验证,超标量？,Pipeline,FP,L2C,多核？异构？,综

8、合后结果功能、时序正确性,增加DFT MBIS是否影响功能,是否符合设计和工艺规则DRC LVS Antenna,主要的验证方法,Functional verification,Simulation,Hardware emulation,Formal methods,Arithmetic verification,Property checking,Equivalence checking,Theorem prover,Language containment,Symbolic model checking,Symbolic trajectory evaluation,两种主要的验证方法,基于

9、模拟的方法，适用于所有设计层次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)形式化方法理论上最佳的验证方法，数学方法受限于问题规模,

10、模拟验证与形式化验证模式,模拟验证平均对待每一种可能和输入时间受限可能不完备输入驱动形式化验证将系统和属性分类分隔子系统内必定完备输出驱动,模拟验证的主要流程,模拟方法：正确的输入得到正确的输出根据设计描述获得验证计划，构造激励，预测预测结果构建测试平台TestBench实例化待测设计DUT用激励驱动DUT运行检查DUT是否获得正确结果模拟运行，反馈设计修改回归测试，固定设计版本,形式化验证的流程,从设计中获得待验证特性抽象或者描述特性特性检查或者等价性检查可能的人工指导或模拟增加、修订或删除限定条件调试调整设计或抽象描述,模拟验证方法,最常用的验证方法，输入驱动Input vectorDir

11、ected伪随机模拟器事件驱动基于周期的硬件模拟器：使用硬件对电路建模,Simulation-based Verification,Execute the system in parallel with a reference model,with respect to some input sequences.,模拟,Find bugs by executing the implementation and checking its behavior四要素：circuit,test pattern,reference output,comparison mechanism,“You can

12、prove the presence of bugs,but you cannot prove their absence.”如果找到一个不一致，就可以证明设计有错不能证明没有不一致(没人可以证明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 ensur

13、e 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 vi

14、olation 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

15、MDesired behavior A formal specification,Model checking,模型检验形式地证明设计的断言和特征，如状态机是否可达、是否死锁、接口的断言搜索整个状态空间，找到属性不满足的点，如果找到，则失败隐式枚举状态空间：符号遍历算法，一次访问一组点，提高效率Unbound propertyBound property,两种方法的比较,SimulationSimulate the design with test stimuli and check the resultsInput output compare expected resultOnly a s

16、mall 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位加法器,adder4b,a3:0,b3:0,sum3:0,c_out,4,4,c_in,4,module ad

17、der4b(sum,c_out,a,b,c_in);input3:0 a,b;inputc_in;output3:0 sum;outputc_out;assign c_out,sum=a+b+c_in;endmodule,Simulation Example,adder4b(DUT),a3:0,b3:0,sum3:0,c_out,4,4,c_in,4,t_adder4b,Testbench,timescale 1ns/1ns/time_unit/time_precisionmodule t_adder4b;reg8:0 stim;/inputs to DUT are regswire3:0 S

18、;/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 simulatio

19、nendendmodule,see“response”to each of these input vectors,UUT,Behav.Verilog:“do this once”,timing control for simulation,Testbench Requirements,Instantiate the Design Under Test(DUT)Provide input to that unitUsually a number of different input combinations!Watch the“results”(outputs of DUT)Can watch

20、 Wave windowCan print out information to the screen or to a file,timescale 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,

21、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 simulationendendmodule,Exhaustive Simulation,综合后,module adder4b(sum,c_out

22、,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),.

23、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 abstraction,Testbench,Simulation,方法 1：Gate-level simulation,Given

24、two designs,prove that for all possible input stimuli their corresponding outputs are equivalent,Design A,Design B,=?,Input,Yes/No,Product Machine,方法 2：Equivalence Checking,例2：交通灯控制器,Guarantee no collisions：It is never possible that all traffic lights are greenGuarantee eventual serviceEventually,ea

25、ch traffic light will become green,E,S,N,Verilog program,module 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 end,/*controller for North light*/alway

26、s 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 L

27、ightControllerDesign,“It is never possible to have a green light for both N-S and E-W.”,ModelChecker,True,False+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

28、N_Sense);infinitely often(S_Go S_Sense);infinitely often(E_Go E_Sense);,All properties verified,Guarantee no collisionsGuarantee service assuming fairnessComputational resources used:57 states searched0.1 CPU seconds,可以通过并行、抽象和自动化减少验证时间并行：采用更多的资源，设计实现与验证并行；验证编码与调试并行抽象：不关心低层次细节，事务级、总线周期级自动化：需要标准化的过程；

29、目前没有通用的标准化方法；有些验证过程可自动化,2/10/03,ECE 426-Lecture 5,49,另一种分类方法,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 usi

30、ng module I/O ports onlyFull knowledge of implementationNo access to internals during simulation,5 验证的代价,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

31、 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 C

32、overageFunctional CoverageCode CoverageBug Rates have flattened toward bottom.,Part.2 Testbench Simulator,使用模拟工具Lint工具语法检查基于事件的模拟工具基于周期的模拟工具基于硬件原型的模拟工具检查与调试,53,Linter 工具1/8,发现共同的编程错误快速静态的RTL代码检查参数和功能调用间不匹配的类型，参数数目不匹配在执行程序前发现错误静态工具,54,int my_func(addr_ptr,ration)int*addr_ptr;float ration;return(*addr

33、_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 environment,55,int my_func(addr_ptr)int*addr_ptr;return(*addr_ptr)+;main()int my_addr;my_func(,Linter 工具3/8,56,Li

34、nter 工具4/8：局限性,只能发现特定类型的问题，不能发现所有问题只能发现代码结构方面的问题，不能发现算法和数据流的问题拼写检查：不能查出用错的词过于严格，可能报一些并不存在的问题错误信息的过滤可以在写完代码后立即运行lint工具,57,Linter 工具5/8,Verilog源代码的lintVerilog更象汇编和basic语言，无类型语言，可以对任意寄存器赋任意值Verilog的linter可以发现公共的问题。,58,Linter 工具6/8,问题 宽度不匹配，verilog 0扩展,59,Linter 工具7/8,60,Linter 工具8/8：实例,部分硬件仿真器与形式化验证工具,

35、ProDesign公司的CHIPitEve公司的ZeBuCadence公司的Incisive Verification、Incisive Formal Verifier、Xtreme III,CHIPit,Prodesign是德国的一家公司 原型验证系统 CHIPit Platinum Edition V4,CHIPit,CHIPit Platinum Edition V4是一个针对大规模芯片设计而开发的原型验证系统。最大配备21个FPGA芯片验证规模可达2000万至3000万，系统速度最高可达200Mhz。,CHIPit,主要功能和特点 适合大规模设计的架构 多层板体系架构和3-D Swit

36、ching互连技术 支持多种验证模式 原型系统验证，模拟加速 便利的调试工具 FPGA探针制作方便,Readback功能,VCD 文件供波形浏览器查看,CHIPit,原型验证流程自动化管理其它特点系统时钟可方便地通过软件进行配置；具有JTAG、PCI、PCIX、PCI-Express、USB、DVI、Ethernet等系统接口；配备板上memory或SSRAM、SDRAM、DDR SDRAM、DDR2 SDRAM等memory扩展子板；可通过Ethernet或者CF卡来配置系统。,CHIPit,与Hardi的比较 FPGA之间的互连 技术软件设置时钟频率和进行复位 Readback功能访问所有

37、的寄存器 支持transation验证模式 集成了项目管理、综合、布线、延时分析、下载、调试、仿真、Co-simulation等软件环境 CHIPit和Hardi的互连接口相同，可以通过电缆连接CHIPit和Hardi。,CHIPit,缺点CHIPit的电压统一为3.3V，增加了子板设计难度和成本，引入了电平转换的延时。CHIPit的CO-Simulation功能是2006年底才新增加的功能，缺乏现成的Transactor，其CO-Simulation的能力还有待验证。CHIPit无法对BlockRam中的数据进行读取。,ZeBu,Eve是法国的一家公司硬件加速器方面的产品主要有Hammer和

38、ZeBu两个系列Hammer是基于处理器的硬件加速器ZeBu是基于FPGA的硬件加速器。,ZeBu,第三代产品是ZeBu-UF，最大支持600万门；第四代产品是ZeBu-XXL，最大支持1亿门 最新产品Zebu-Server/Blade，200M*10,ZeBu-UF,ZeBu-UF是基于Xilinx V4LX系列构建的一块PCI扩展卡 最大支持600万门，最高速度可达200MHz,ZeBu-UF,验证模式ZeBu-UF能支持多种验证模式基于信号级的C/C+/SysemC基于事务级的C/C+/SysemC/SystemVerilog基于测试向量的模拟加速基于STB的在线仿真基于DirectIC

39、E的在线仿真、以及基于SmartICE的在线仿真,ZeBu-UF,调试能力动态探针和静态探针两种调试手段动态探针对模拟速度的影响较大 对于在线仿真，ZeBu还提供了类似逻辑分析仪的HW trigger来控制时钟和trace memory。,ZeBu-UF,较丰富的Transactor和存储器模型 TransactorUART、LCD、PCI Express、Ethernet、AHB、USB、Firewire、JTAG等等SDR、DDR、DDR2、DIMM SDR/DDR/DDR2、Flash,ZeBu-UF,软件资源综合时需要调用Synplify，并有自己的编译工具对综合后的网表进行优化ZeB

40、u的编译器会自动对设计进行划分，并完成相应的综合、映射和布局布线,ZeBu实用评测,ZeBu的加速性能易用性调试能力,ZeBu实用评测,ZeBu-UF2，最大支持300万门HOST采用Xeon 3G的CPU，内存4G，IDE硬盘。测试对象为L2C与MI联合测试环境的FPGA版本，外围测试环境包括测试激励和DDR2模型。DUT规模小于100万门，因此不必进行FPGA划分。,ZeBu实用评测,ZeBu-UF2插入HOST的PCI插槽所遇到的问题统一设计顶层问题IDDR与ODDR问题IDELAY问题LUT4问题:对于所有由FPGA内部器件实现的延迟功能，ZeBu都不支持 DDR2模型问题,ZeBu实

41、用评测,测试结果,ZeBu实用评测,测试结果CO-Simulation过程中动态探针对模拟速度有较大的影响。加入动态探针的CO-Simulation模拟速度甚至比只在HOST上运行且记录波形的模拟速度还要慢,Xtreme III,Cadence公司的硬件加速器PalladiumXtreme两个系列,Xtreme III,Xtreme III最大支持7200万门 400kHz-800kHz板上存储器容量为18GB最多能支持12个用户同时使用,Xtreme III,验证模式支持多种验证模式包括基于信号级的模拟加速基于事务级的SystemC/C/C+/e模拟加速基于断言的模拟加速,不支持基于PSL的

42、模拟加 速，但Palladium III支持各种在线仿真,Xtreme III,调试能力 相对较强readmemh和writememh查看和修改存储器单元；printf（）或$display（）语句实时输出消息snapshot Hot-Swap功能,Xtreme III,软件资源与Cadence软件验证环境集成在一起，能利用SimVision查看波形，进行事务和断言调试、具有软硬件联合调试功能和覆盖率统计功能 TBA VIP提供了较为丰富的基于事务加速的验证IP，包括PCI Express、Ethernet、AMBA、AHB、AXI等等,与ZeBu的比较,都不能处理使用FPGA中的器件来实现逻

43、辑功能ASIC的库单元模拟模型一般都会使用UDP，Xtreme III能自动将UDP映射为硬件，从而使得加速ASIC库单元成为可能，而ZeBu不具备此功能 Xtreme III支持通过层次方式直接访问位于加速器的DUT中的信号，而ZeBu不具备此功能,与ZeBu的比较,Xtreme III能通过Hot-Swap功能方便查错和执行不能被加速的激励，而ZeBu不具备此功能。Xtreme III能将断言映射为硬件，从而能进行基于断言的加速，而ZeBu不具备此功能。ZeBu-UF2支持STB，但要求测试激励必须是可综合的,Xtreme III允许测试激励不一定都是可综合,也能加速,IFV,断言:监测设

44、计中正确行为或错误行为的验证对象。断言将设计要求转换成了验证对象，从而可以用模拟器或形式化验证工具，评测设计要求是否被满足,IFV,断言可分为三种，第一种为Assertion，用于描述设计所期望的正确行为；第二种为Constraint，用于描述设计所处环境的行为；第三种为Cover，用于描述设计及其所处环境应该会到达的状态。,IFV,形式化验证的结果FailPassExplored,IFV,与模拟相比形式化验证不需要编写测试激励，只要断言编写完整，就能完全验证设计的正确性它还能发现模拟所不容易查出的错误形式化验证的有效性依赖于断言 适合进行模块级的验证和对控制逻辑进行验证，否则可能会因状态空间

45、过大而无法在规定时间内完成验证。,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通过模拟

46、的方式生成波形，而IFV不需要testbench而快速生成波形。0-IN对VHDL的支持处于Beta阶段，并且也不支持混合语言，但IFV完全支持VHDL，且也支持混合语言。Cadence在中国具有训练有素的形式化验证方面的工程师，而Mentor没有。IFV支持在断言中直接使用层次化信号名，而0-IN不支持。,Incisive Verification,Cadence公司推出的一整套验证解决方案 验证自动化的流程 它的基础是Incisive Plan-to-Closure Methodology（IPCM）,Incisive Verification,Plan：即根据给出的设计要求制定可执行的验

47、证计划、确定覆盖标准、安排人力和机器资源并分派验证任务。Execute：根据验证计划建立验证环境、构建验证组件、自动生成测试激励，并进行软模拟、形式化验证、模拟加速以及在线仿真。Measure：分析验证结果和整个覆盖率，并与验证计划进行对照。React：根据验证结果和与验证计划对照的情况，修正设计和测试环境的错误、调整验证计划以及人力和机器资源安排。重复上述过程直到验证收敛。,Incisive Verification,为了提高测试程序的开发效率，IPCM强调测试激励的自动生成和验证组件的可重用性 Cadence公司提出了 uRM（Universal Reuse Methodology）Cad

48、ence公司提供了丰富的已开发好的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验证系统级环境验证

49、固件、操作系统和各类驱动使用工具软模拟、加速器仿真、形式化验证商业工具+定制工具,Sun 功能模拟与验证流程,处理器设计验证流程,Sun 模拟与验证环境开发,开发语言Verilog 继承/惯性（T1）（主要RTL模型）System Verilog（T2/T3）Vera（覆盖率测试与随机测试）模拟验证环境模块级 SAT(Stand Alone Test)系统级(全自动回归测试Regression)全处理器RTL模型存储子系统系统级TestbenchAssertionsMonitor(协议检测、辅助调试)Sun 验证的核心-仿真软模拟速度限制，形式化验证的规模限制基于Xtrem的Virtual S

50、ilicon 仿真验证(10,000+VCS)多种metricRTL Stablility,Bug,Coverage,Sun 仿真验证,原因系统级设计包括：处理器RTL、存储子系统、系统组件和TestbenchUltraSPARC T1 系统级模型 3千5百万门（超过所有形式化验证工具能力）软模拟器 一秒模拟一个周期仿真与加速仿真 In-Circuit 接口存放目标系统加速(高速模拟器)Sun同时使用了两种方式Palladium Xtreme以Xtreme为中心Sun 基于Xtreme的仿真验证减少新设计提交时间（hot-swap VCS-Xsim）简化、加速模型初始化(forces，PLI和