JasperGold 比想象中更强大

2017-05-15 IC验证工程师——公众号
分享到:

JasperGold是什么

当JasperGold在研讨会上,更为全面的展示给我时,我反而有些难回答“JasperGold是什么”这个问题了,因为感觉JasperGold包罗万象,突破了很多我之前的认知。


当然,从总的技术流派来说,首先JasperGold 依然属于静态验证范畴,逻辑并没有实际进行Simulation(动态仿真)。


当然,从JasperGold的主流来说,其依然是以“形式验证”作为主要推荐内容。基于断言的“属性检查”(FPV,Formal Property Verification)依然是其排行第一的APP。


DeepChip(www.deepchip.com)将其票选为2016年最佳工具。评论的理由如下:

“JasperGold is the best way to quickly verify functionality at the block level. It is complimentary to RTL simulation.”

“Rather than formal vs. simulation, I prefer to think about it as formal plus simulation. Use the right tool for the job.”


尤其是其中“formal plus simulation”,是我在和Cadence的主讲人Jin Tang交流后,深切感受到的一点。JasperGold 吸收了部分Simulation的优势,使其工作的更为高效。


JasperGold APPs的十二罗汉
QQ截图20170512234317


JasperGold共包含十二罗汉(Verification Suite是四大金刚,真的不是洪兴帮?):

    FPV:Formal Property Verification,基于断言属性的静态验证,适用于Block级(中等容量的设计),或者端到端(基于逻辑输入/输出接口)的检查,可以支持交互式操作,以及约束设置(后面介绍);

    BPS,Behavioral Property Synthesis,从RTL和波形中,自动由工具提取属性,并以SVA的形式表现,生成相关断言和覆盖率信息,并对其设置优先级。全自动化操作,大量节省关注于基础设计的人力,可以使人力投入更为有效的工作中;

    AFL,Automatic Formal Linting,对RTL代码进行Lint,以及自动的Formal的检查,可以使设计规避简单错误,基于RTL产生可以在FPV中使用的属性信息。又是全自动化操作,大量节省人力;

    X-PROP,X-Propagation快速进行X态传播的分析,协助定位由X态传播造成的问题;

    CSR,Control and Status Register Verification,人工基于表格(如Excel、Openoffice、CSV、IP-XACT等)定义控制和状态寄存器属性,工具自动的检查寄存器属性是否与定义的一致,当产生不一致时,以最小的波形长度体现其错误信息;

    CV,Connectivity Verification,人工基于表格(如Excel、Openoffice、CSV、IP-XACT等)定义接口连接关系,工具自动检查设计的连接关系是否与定义的一致;

    UNR,Coverage Unreachability,基于RTL,检查哪些代码本身就是“不可覆盖”的,可以与仿真工具配合,减少人工分析未覆盖代码的工作量,让人力更集中在那些“本身可覆盖但未覆盖”的代码上;

    DESIGN,Design Coverage,自动生成Formal验证需要的覆盖率矩阵(对,Formal也关心覆盖率),分析覆盖率信息的覆盖情况,为验证定义了“bounded proof(下限)”,即必须达到的目标,可以避免由于人为的过约束导致的验证不完备;

    SEC,Sequential Equivalency Checking,功能一致性检查,其检查关注于功能(基于端到端,由接口体现的功能),而非微架构,使其具有更大的适用范围;

    LPV,Low-Power Verification,基于设计,以及低功耗描述(UPF或CPF),自动检查设计是否满足低功耗需求;

    SPV,Security Path Verification,检查数据信息是否会被误读取,或者被误重写,以及当异常发生时,数据信息是否依然安全,例如SOC系统的总线数据一致性检查;

    PSD,Post-Silicon Debugging,即硅后(流片后)的Debug工作,这里,不是一个APP(即非工具),只是可以在以上APP的基础上,开展硅后的工作,检查相关问题;

    ABVIP,Assertion-Based Verification IP,接口和协议的自动属性检查,包括AMBA等流行的标准协议。


新认知:Expert System

JasperGold之前的引擎选择比较让人迷惑,什么时候选择什么引擎(不同于APP),总觉得是只有数学家才能做好的事情。


现在,JasperGold提供了更为智能的客户端系统,它会像参谋一样,提供我们建议,告诉我们哪里比较复杂,提供不同的操作建议以发现更为深层次的Bug,以及推荐我们切换引擎以加强发现问题的效果。


新认知:RTL Designer Signoff

RTL Designer Signoff是这次研讨会我最大的收获。当我们讨论是采用Formal还是Simulation时,往往容易走极端,非此即彼。而RTL Designer Signoff 的思想则将两者结合在了一起。


我们完全可以在RTL开发完成后,使用Formal 工具,先扫清一部分错误,再交付后续的Simulation。毕竟,Formal 的特点是投入小,产出大。在没有搭建验证平台的时候,就可以发现很多逻辑缺陷,越早发现问题,发现问题的成本越低。

新认知:形式验证也有波形
QQ截图20170512234301

JasperGold形式验证虽然是静态验证,但是,它依然可以提供波形供验证工程师分析,一个断言属性Fail了,为什么Fail,它可以通过波形的方式告诉你。


另外,当我们发现波形的接口输入,与预期不一致时,可以直接在GUI上调整输入波形(激励),非常方便。


新认知:输入激励约束


我之前认为JasperGold只能由数学引擎通过计算得出各种激励信息,而通过研讨会,我了解到JasperGold完全可以与Agent结合使用。我们可以根据自己的需要,定义输入激励,基于更加具有指向性,更加高效的激励来检查我们的设计。


当然,如前文所述,JasperGold 的Design Coverage会检测我们的激励是否过约束,是否达到了验证的底线。


新认知:功能覆盖率模型


我之前认为功能覆盖率模型只是Simulation阶段才能使用的信息,现在JasperGold可以读入功能覆盖率模型了。JasperGold可以基于自己产生的信息,进行覆盖率模型信息的采样和统计,判断是否覆盖了相应功能。


在这一点上,JasperGold 也更加体现出其Formal plus Simulation的属性。

新认知:更多的指向性

JasperGold可以在传统的形式验证,以及Simulation的路径覆盖进行折中。


传统的形式验证,其错误搜索过程是基于初始状态,cycle-by-cycle的向外进行全方向的检查。而JasperGold提供了其它选择,例如:

Cycle Swarm模式,使Formal工具可以跳过一些不重要的Cycle,而搜索那些重要的Cycle;

State Swarm模式,自动选择更为有意义的方向,更可能发现问题的方向;

Guided Search模式,当验证工程师认为哪里可能更容易遗留错误时,就指示引擎向那个方向针对性的搜索。


综上,JasperGold的搜索方式更多元化,更有指向性。


总结


JasperGold 包含了丰富的APP供我们使用;

JasperGold 提供了更为智能的专家系统作为我们的助理;

JasperGold 提供更加高效的错误检查,使RTL Designer Signoff 质量更高;

JasperGold 可以结合Formal和Simulation的优势,可以查看和调整波形,可以控制输入激励,可以结合功能覆盖率模型,可以控制验证的指向性。


总之,通过这次研讨会,我的认知得到了很大的提升,JasperGold大有可为。


×
官方微信