最新大规模集成电路验证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 CycleProceedings: DAC, DATE, HLDVT, ITCVerification vs. TestingVerification检验设计的正确性主要方法为模拟、硬件仿真和形式化方法在设备制造之前多次重复，但对一个设计仅一次完整正确验证为设计的质量负责Testing检测生产结果的正确性分两个步骤：设计期间产生测试；生产后应用测试对生产出来的每个产品均完成一次测试对器件的质量负责Why we need VerificationExample 1 1980北美防空司令部误报遭受导弹袭击检测反馈电路故障检测反馈软件对故障未处理，直接报告预警Possible World War IIIExample 2 1996年阿丽亚娜5火箭爆炸64位双精度浮点操作转换为16位整数时产生的例外重新设计的计算节点板＋完全重用阿丽亚娜4软件代价 $800M 4颗Cluster卫星Why we need VerficationExample 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 vectorDirected￿随机模￿器事件￿￿基于周期的硬件模￿器：使用硬件￿￿路建模0010100101010001110101001110101010100000000011101011011011110111Simulation-based Verification Execute the system in parallel with a reference model……with 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 mechanismRequirementsSimulateRTL ModelGate-levelModelSynthesizeSimulateTest BenchASIC or FPGAPlace & RouteTimingModelSimulate“You can 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 functionalityIt 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 property–Bound property两种方法的比￿–Simulation•Simulate the design with test stimuli and check the results•Input  output  compare expected result•Only a small part of the space can be explored•Hard to tell if testing is sufficient–Formal•Proving facts about the design•Model checking, Equivalence checking•Expected behavior  property  prove•Time and space issues•Hard to tell if properties are complete例 1：4位加法器adder4ba[3:0]b[3:0]sum[3:0]c_out44c_in4module adder4b (sum, c_out, a, b, c_in);input [3:0] a, b;inputc_in;output[3:0] sum;outputc_out;assign {c_out, sum} = a + b + c_in;endmoduleSimulation Exampleadder4b(DUT)a[3:0]b[3:0]sum[3:0]c_out44c_in4t_adder4bTestbench`timescale 1ns /1ns // time_unit/time_precisionmodule t_adder4b; reg[8:0] stim;// inputs to DUT are regswire[3:0] S;// outputs of DUT are wires wire C4;// instantiate DUTadder4b(S, C4, stim[8:5], stim[4:1], stim[0]);// stimulus generationinitial begin stim = 9'b000000000;// at 0 ns #10 stim = 9'b111100001;// at 10 ns #10 stim = 9'b000011111;// at 20 ns #10 stim = 9'b111100010;// at 30 ns #10 stim = 9'b000111110;// at 40 ns #10 $stop;// at 50 ns – stops simulationendendmodulesee “response” to each of these input vectorsUUTBehav.Verilog:“do this once”timing control for simulationTestbench RequirementsInstantiate the Design Under Test (DUT)Provide input to that unitUsually a number of different input combinations!Watch the “results” (outputs of DUT)Can watch Wave window…Can print out information to the screen or to a file`timescale 1ns /1ns // time_unit/time_precisionmodule t_adder4b; reg[8:0] stim;// inputs to DUT are regswire[3:0] S;// outputs of DUT are wires wire C4;// instantiate DUTadder4b(S, C4, stim[8:5], stim[4:1], stim[0]);// monitor statementinitial $monitor($time, C4, S, stim[8:5], stim[4:1], stim[0]);// stimulus generationinitial begin stim = 9'b000000000;// at 0 ns #10 stim = 9'b111100001;// at 10 ns #10 stim = 9'b000011111;// at 20 ns #10 stim = 9'b111100010;// at 30 ns #10 stim = 9'b000111110;// at 40 ns #10 $stop;// at 50 ns – stops simulationendendmoduleExhaustive 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(a[0]), .B(b[0]), .CI(c_in), .CO(carry1 ), .S(sum[0]) ); ADD32 U1_1 ( .A(a[1]), .B(b[1]), .CI(carry1 ), .CO(carry2 ),.S(sum[1]) ); ADD32 U1_2 ( .A(a[2]), .B(b[2]), .CI(carry2 ), .CO(carry3 ), .S(sum[2]) ); ADD32 U1_3 ( .A(a[3]), .B(b[3]), .CI(carry3 ), .CO(c_out), .S(sum[3]) );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 simulationGiven 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 green•Guarantee eventual service–Eventually, each traffic light will become greenESNVerilog 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 verifiedGuarantee no collisionsGuarantee service assuming fairnessComputational resources used:57 states searched0.1 CPU seconds•可以通￿并行、抽象和自￿化减 少￿￿￿￿–并行：采用更多的资源，设计实现与验证并行；验证编码与调试并行–抽象：不关心低层次细节，事务级、总线周期级–自动化：需要标准化的过程；目前没有通用的标准化方法；有些验证过程可自动化2/10/03ECE 426 - Lecture 549另 一种 分￿方法Black boxVerify using module I/O ports onlyNo knowledge of implementationNo access to internalsWhite boxVerify using module I/O ports and internalsFull knowledge of implementationFull access to internals during simulationGray boxVerify using module I/O ports onlyFull knowledge of implementationNo 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 and more to find fewer and fewer errors.Question: how much is enough?￿￿何￿￿止？Emotionally, or Intuitively;Out of money? Exhausted?Competition’s product is there.Software people are happy with your hardware.There have been no bugs reported for two weeks.More rigorous criteria;All tests passedTest Plan CoverageFunctional CoverageCode CoverageBug Rates have flattened toward bottom.Part.2 Testbench Simulator使用模拟工具Lint工具语法检查基于事件的模拟工具基于周期的模拟工具基于硬件原型的模拟工具检查与调试Linter 工具1/8发现共同的编程错误－快速静态的RTL代码检查参数和功能调用间不匹配的类型，参数数目不匹配在执行程序前发现错误静态工具53int 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 environment…54 int my_func(addr_ptr) int *addr_ptr;{ return (*addr_ptr)++;}main(){ int my_addr; my_func(&my_addr); return 0;}Linter 工具3/855Linter 工具4/8：局限性只能￿￿特定￿型的￿￿，不能￿￿所有￿￿只能￿￿代码￿构方面的￿￿，不能￿￿算法和数据流的￿￿拼写￿￿：不能￿出用错的￿￿于￿格，可能￿一些并不存在的￿￿错￿信息的￿￿可以在写完代码后立即运行lint工具56Linter 工具5/8•Verilog源代码的 lint•Verilog更象￿编和 basic￿言，无￿型￿言，可以￿任意寄存器￿任意￿•Verilog的 linter可以￿￿公共的￿￿。

57Linter 工具6/8￿￿ ￿度 不匹配，verilog 0￿展58Linter 工具7/859Linter 工具8/8：￿例60部分硬件仿真器与形式化验证工具ProDesign公司的CHIPitEve公司的ZeBuCadence公司的Incisive Verification、Incisive Formal Verifier 、Xtreme IIICHIPitProdesign是德国的一家公司 原型验证系统 CHIPit Platinum Edition V4 CHIPitCHIPit 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中的数据进行读取ZeBuEve是法国的一家公司硬件加速器方面的产品主要有Hammer和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-UF1.验证模式ZeBu-UF能支持多种验证模式基于信号级的C/C++/SysemC基于事务级的C/C++/SysemC/SystemVerilog基于测试向量的模拟加速基于STB的仿真基于DirectICE的仿真、以及基于SmartICE的仿真 ZeBu-UF2.调试能力动态探针和静态探针两种调试手段动态探针对模拟速度的影响较大 对于仿真，ZeBu还提供了类似逻辑分析仪的HW trigger来控制时钟和trace memory。

ZeBu-UF3.较丰富的Transactor和存储器模型 TransactorUART、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实用评测测试结果0~300us300us~1000usL2C与MI运行在HOST上5m17mL2C与MI运行在ZeBu-UF2上2.5m12m加速比50%29%ZeBu实用评测测试结果CO-Simulation过程中动态探针对模拟速度有较大的影响。

加入动态探针的CO-Simulation模拟速度甚至比只在HOST上运行且记录波形的模拟速度还要慢 Xtreme IIICadence公司的硬件加速器PalladiumXtreme两个系列 Xtreme IIIXtreme III最大支持7200万门 400kHz-800kHz板上存储器容量为18GB最多能支持最多能支持12个用户同时使用个用户同时使用 Xtreme III1.验证模式•支持多种验证模式•包括基于信号级的模拟加速•基于事务级的SystemC/C/C++/e模拟加速•基于断言的模拟加速,不支持基于PSL的模拟加 速，但Palladium III支持•各种仿真 Xtreme III2.调试能力 相对较强•readmemh和writememh查看和修改存储器单元；•printf（）或$display（）语句实时输出消息•snapshot •Hot-Swap功能 Xtreme III3.软件资源•与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•形式化验证的结果形式化验证的结果•Fail•Pass•Explored• 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不支持Incisive VerificationCadence公司推出的一整套验证解决方案 验证自动化验证自动化的流程 它的基础是Incisive Plan-to-Closure Methodology（IPCM） Incisive VerificationPlan：即根据给出的设计要求制定可执行的验证计划、确定覆盖标准、安排人力和机器资源并分派验证任务Execute：根据验证计划建立验证环境、构建验证组件、自动生成测试激励，并进行软模拟、形式化验证、模拟加速以及仿真Measure：分析验证结果和整个覆盖率，并与验证计划进行对照React：根据验证结果和与验证计划对照的情况，修正设计和测试环境的错误、调整验证计划以及人力和机器资源安排重复上述过程直到验证收敛Incisive Verification为了提高测试程序的开发效率，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模型存储子系统系统级TestbenchAssertionsMonitor (协议检测、辅助调试)Sun 验证的核心 -- 仿真软模拟速度限制， 形式化验证的规模限制基于Xtrem的Virtual Silicon 仿真验证 (10,000+ VCS)多种metricRTL Stablility, Bug , CoverageSun 仿真验证原因系统级设计包括： 处理器RTL、存储子系统、系统组件和TestbenchUltraSPARC 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）仿真为核心的验证带来的问题整个验证流程都有修改与变化RTL设计testBench设计断言方法Monitor实现模型release回归测试调试加速是首位需求所有内容进入仿真平台可综合设计，为定制单元开发可综合的简化RTL模型定制单元在标准模拟中无Testbench，要为仿真环境开发简化testbenchSun RTL模拟时间Sun T1 Bug报告Sun 模拟验证. 其它体系结构级验证PRM Coverage （Program Reference Manual）Directed diag, functional, traps/ASI/MMU/State-Reg Coverage Self-Checking DiagSystem interfaceReset VerificationDebug support VerificationMicroarchitecture 验证功能测试Unit Focused (all major block, Directed C/Perl Internal code)Memory Verification using Symbolic Simulation Clock Domain Checking VerificationPerformance VerificationHardware AccelerationOpenSPARC T1/T2 代码环境T1与T2的变化明显OpenSPARC T1/T2 代码环境•激励代码量为RTL代码35倍OpenSPARC T1/T2 代码环境Testbench代码量约是RTL设计的 70%T2 SAM设计优化尚不包括 perl脚本代码 (SIMS Midas Goldfinger等)硬件测试验证平台SIMSthe Glue logic between RTL design & EDA tools主要功能利用Verilog模拟环境 完成 HW设计模拟T2 only VCS over SPARC使用Synopsys Vera 完成coverage验证 建立vera运行脚本和project文件 More： 建立运行环境，参数配置，控制其它工具Clearcase、Debussy的配置与运行未提供功能：Hammer Hardware AcceleratorAxis Hardware AcceleratorPalladiumZeroInsims环境介绍sims脚本1.272 5983行perl脚本sims调用前端处理工具 configsrch、midas、goldfinger (sh+other)sims/midas调用编译预处理、汇编和连接工具bw_cpp bw_m4 g_as g_ld gmake g_objdump等工具sims调用EDA工具完成regressionsims 调用regreport、vlog等后期处理器工具What sims do? 在运行sims的model目录下，根据选择group的不同，在cmp1/fc8子目录下根据diaglist选择激励和参数建立本次regression的子目录，时间+ID建立Vera工程文件和Shell调用VCS编译Verilog代码 （testbench + RTL） 根据diaglist文件中的参数建立模拟命令为每一个测试建立子目录tlu_rand05_ind_03:cmp1_st:cmp1_mini_T2:0sims 简单流程简单流程启动参数处理启动参数处理单个测试运行单个测试运行group?regression运行运行退出退出GetOptions: 从命令行和配置文件中获取参数是否rerun第二组参数处理diag参数处理Build (vcs/vera)asm+mem.image/efuse.image编译.vr文件sjm和pci的diag JTAG/dramvcs_run/ncv_run/sim_rundiag.pl后期处理perl代码流程逐个处理test $alias准备模拟命令进入indrm(dream)call sims 单个test的sims PHASEA.1 print usage title： sims第1020行 print_header函数A.2 SETUP PHASE：在 /var/temp下建USER:TESTBENCH目录A.3 preprocessing PHASE： 调用处理汇编文件的Midas工具，该工具是perlmod；bw_cpp 将diag.s转换为 diag.cpp；bw_m4 将diag.cpp转换为diag.m4A.4 PARSING PHASE： Midas调用二进制辅助工具goldfinger，将Midas的内容diag.m4写入到diag.midas文件中，产生各个section的汇编代码，例如RED_SEC RED_EXT_SEC HPRIV_RESET HTRAPS TRAPS KERNEL USER_HEAP和MAI Midas处理diag.midas，解析其中的Section，语法检查等。

清除build目录，准备参数，调用ncverilog开始模拟单个test的sims PHASEA.5 ASSEMBLY PHASE：Midas使用多个线程将上一步goldfinger形成的汇编文件编译成.o模块文件，调用预先提供的g_as二进制工具（g_as无源码，但有opensolaris可参照）A.6 LINK PHASE： Midas产生连接的描述文件diag.ld_scr；调用预先提供的g_ld工具，产生类型为elf64-sparc的diag.exe文件A.7 POSTPROCESSING PHASE：Midas产生diag.goldfinger文件，Goldfinger根据此文件产生mem.image文件在整个过程中产生 symbol.tbl， mem.image和diag.ev三个文件A.8 COPY PHASE：拷贝文件，建立diag.s、mem.imag、diag.ev、symbol.tbl和diag.exe的硬链接A.9 CLEANUP PHASE：清除build目录，准备参数，调用simv开始模拟config args/command按照group（cmp1_mini）参数选择 sys (cmp1) 选择config (diag目录下的diaglist子目录包含模拟所需要的文件和参数列表)Diaglist文件 T1 中的chip8.conf 定义 -model cmp11 或者 fc8定义 vera需要的配置文件 vcon cmp_top.vcon定义 模拟需要的各个模块需要的文件列表定义 模拟各个模块的配置 -config_rtl定义其它参数，例如vcs的build参数 -vcs_build_args 或者-ncv_build_argsT2 diag/diaglist文件和env下filelist文件sims脚本中使用opt保存了具有177/210个参数配置的Hash表Group Diag定义diaglist，默认的diaglist是$DV_ROOT/verif/diag/master_diaglist，而该文件只是引用了core1.diaglist和chip8.diaglist两个文件，后两个文件中有众多的参数配置还应用了诸如cmp2_basic.diaglist这样的文件。

 从diaglist函数中获取diag参数，调用get_opt_from_diaglist(4765)函数在该函数中将调用bw_cpp工具（Sun的cpp预编译器）来产生master_diaglist文件SAM环境OpenSPARC T1的软件环境包括两部分：伴随OpenSPARC T1项目一同开源的模拟环境，称为Arch.Tool；SAM-T1 SAM-2T1/T2处理器上的操作系统、编译、应用开发等Sun称为CoolTools的相关软件SAM-T2的代码结构优于SAM-T1，cpp代码减少， Xml和python代码增多思考的问题 模拟时间长 > 1 month (T1 cmp8/ T2 fc8) 测试激励是否足够？ cmp1_mini 51个激励 FPGA原型和裁减需要多长时间S1 > 6 months思考的问题 确定整个芯片验证的标准 ？ 通用处理器 not ASICBoot OS ＋ 典型应用 (1x – xx个应用) (可行)Random ＋ Directed 测试 （Sun） 结束语结束语谢谢大家聆听！！！谢谢大家聆听！！！121。