电子教案soc设计方法与实现-课件第9章

第九章SoC功能验证郭炜魏继增郭筝谢憬内容大纲功能验证概述功能验证方法与验证规划系统级功能验证仿真验证自动化形式验证基于断言的验证内容大纲功能验证概述功能验证方法与验证规划系统级功能验证仿真验证自动化形式验证基于断言的验证随着设计的进行，越接近最后的产品，修正一个设计缺陷的成本就会越高不同设计阶段修正一个设计缺陷所需费用示意图验证的概念在IC设计与制造领域，通常所说的验证（Verification）和测试（Test）是两种不同的事验证在设计过程中确认所设计的正确性通过软件仿真、硬件模拟和形式验证等方法进行在流片之前要做的。测试检测芯片是否存在制造或封装过程中产生的缺陷。采用测试设备进行检查功能验证功能验证一般是指设计者通过各种方法比较设计完成的电路和设计文档规定的功能是否一致，保证逻辑设计的正确性。通常不包括面积、功耗等硬件实现的性能检测SoC功能验证的挑战系统复杂性提高增加验证难度设计层次提高增加了验证工作量发展趋势：内容大纲功能验证概述功能验证方法与验证规划系统级功能验证仿真验证自动化形式验证基于断言的验证仿真为基本出发点的功能验证方法功能验证开发流程制订验证计划功能验证需求激励产生策略结果检测策略验证开发提高验证的效率内容大纲功能验证概述功能验证方法与验证规划系统级功能验证仿真验证自动化形式验证基于断言的验证系统级功能验证行为级功能验证测试数据控制流，包括初始化和关闭I/O设备、验证软件功能、与外界的通信，等等性能验证通过性能验证可以使设计者清楚地知道整个系统的工作速度、功耗等性能方面的指标。协议验证根据总线协议对各个模块的接口部分进行验证系统级验证系统级的测试平台边界条件设计的不连续处出错的条件极限情况系统级的测试平台标准性能指标覆盖率指标内容大纲功能验证概述功能验证方法与验证规划系统级功能验证仿真验证自动化形式验证基于断言的验证仿真验证平台激励的生成直接测试激励：检测到测试者所希望检测到的系统缺陷可以快速、准确地产生大量的与实际应用一致的输入向量随机测试激励：检测到测试者没有想到的一些系统缺陷带约束的随机测试激励是指在产生随机测试向量时施加一定的约束，使所产生的随机测试向量满足一定的设计规则。带约束的随机激励生成的例子x1和x2为系统的两个输入，它们经过独热码编码器编码之后产生与被验证设计（DUV）直接相连的输入输入约束：in[0]+in[1]+in[2]<=1这样产生的随机向量就可以保证它们的合法性用SystemVerilog语言写的带约束随机激励生成例子输入data的数量限制在1～1000programautomatictest;

//defineconstraintclassTransaction;

randbit[31:0]src,dst,data[];//Dynamicarray

randcbit[2:0]kind;

//Cyclethroughallkinds

constraintc_len

{

data.size

inside{[1:1000]};}//LimitarraysizeEndclass//instantiationTransactiontr;

//startrandomvectorgenerationinitialbegintr=new();

if(!tr.randomize())$finish;transmit(tr);endendprogram响应的检查可视化的波形检查：直观，但不适用于复杂系统设计自动比对检查：通过相应的检测模型或验证模型来自动完成输出结果的比对覆盖率的检测覆盖率数据通常是在多个仿真中收集的覆盖率的模型由针对结构覆盖率（StructuralCoverage）和功能覆盖率（FunctionalCoverage）两种目标而定义的模型所组成。可细化为：限状态机覆盖率（FSMCoverage）表达式覆盖率（ExpressionCoverage）交叉覆盖率（CrossCoverage）断言覆盖率（AssertionCoverage）用SystemVerilog语言写的覆盖率检测的例子programautomatictest(busifc.TBifc);classTransaction;

randbit[31:0]src,dst,data;

randenum{MemRd,MemWr,CsrRd,CsrWr,

IoRd,IoWr,Intr,Nop}

kind;

endclass

covergroupCovKind;

coverpointtr.kind;//Measurecoverage

endgroup

Transactiontr=new();//Instantiatetransaction

CovKind

ck=new(); //Instantiategroup

initialbegin

repeat(32)begin//Runafewcycles

if(!tr.randomize())$finish;

ifc.cb.kind<=tr.kind;//transmittransaction

ifc.cb.data<=tr.data;//intointerface

ck.sample();//Gathercoverage

@ifc.cb;//Waitacycle

end

endendprogram内容大纲功能验证概述功能验证方法与验证规划系统级功能验证仿真验证自动化形式验证基于断言的验证形式验证形式验证（FormalVerification）静态形式验证（StaticFormalVerification）和半形式验证（Semi-FormalVerification）静态形式验证不需要施加激励，也不需要通过仿真来验证。目前，SoC设计中常用的静态形式验证方法是相等性检查。半形式验证是一种混合了仿真技术与形式验证技术的方法。常用的半形式验证是混合属性检查或模型检查，它将形式验证的完整性与仿真的速度、灵活性相结合。静态形式验证相等性检查（EquivalentCheck）对设计进行覆盖率100％的快速验证主要是检查组合逻辑的功能相等性不需要测试平台和测试矢量，不需要进行仿真可用于比较RTL与RTL、RTL与门级、门级与门级的功能相等性，被广泛应用于版图提取的网表与RTL代码比较，特别是做完ECO后要进行网表和修改后的RTL的相等性检查。半形式验证半形式验证（Semi-FormalVerification）仿真和形式验证形结合，如混合模型检查（ModelChecking）或属性检查（PropertyChecking）的方法。内容大纲功能验证概述功能验证方法与验证规划系统级功能验证仿真验证自动化形式验证基于断言的验证基于断言的验证仿真验证面临的问题：可观测性和可控制性合适的输入矢量能够激活错误错误要能够以某种预期的形式输出采用断言描述设计的行为，在仿真时起到监控作用，当监控的属性出现错误时，立刻触发错误的产生，增加了设计在仿真时的可观测性问题。也可以用在形式属性检查中作为要验证的属性。属性检查（PropertyCheck）时，是对整个状态空间进行搜索，能够控制到每一个信号并能指出错误的具体位置，解决了设计验证时的可控制性和可观察性问题。验证实现所花费的时间与验证的质量断言的作用断言的作用断言语言及工具的使用断言语言CorSystemCSystemVerilogAssertion(SVA)PropertySpecificationLanguage(PSL)(IBM,basedonSugar)OpenVerificationLibrary(OVL)Verilog,VHDLSVA（SystemVerilogAssertion）例子用Verilog实现的检查器：always@(posedgeA)begin

repeat(1)@(posedgeclk);fork:A_to_Bbegin@(posedgeB)$display(“SUCCESS:Barrivedintime\n”,$time);disableA_to_B;endbeginrepeat(1)@(posedgeclk)@(posedgeB)display(“SUCCESS:Barrivedintime\n”,$time);disableA_to_B;endbeginrepeat(2)@(posedgecl