0
  • 聊天消息
  • 系统消息
  • 评论与回复
登录后你可以
  • 下载海量资料
  • 学习在线课程
  • 观看技术视频
  • 写文章/发帖/加入社区
会员中心
创作中心

完善资料让更多小伙伴认识你,还能领取20积分哦,立即完善>

3天内不再提示

1+1>2:这两个工具,治好验证开发者的精神内耗

新思科技 来源:未知 2022-12-07 19:35 次阅读

99568110-761e-11ed-8abf-dac502259ad0.gif

仿真和形式验证是当今SoC设计和验证流程中使用的两个关键验证策略。它们各有所长,在查找边界漏洞并最终实现验证收敛和签核方面相辅相成。 仿真和形式验证通常由不同的团队来完成,而他们各自都有一套签核目标。由于形式验证和仿真需要不同的专业知识和技能,两个团队通常不会密切合作。然而,仿真和形式验证之间存在协同作用,它对整个验证工作大有裨益,并能加速覆盖率收敛。 在本文中,我们将通过研究仿真和形式验证之间的技术联系,探讨如何帮助验证和形式化团队更好地合作,从而有效地结合这两种技术来加速实现验证签核。

实现覆盖率收敛

为什么这么难?

仅使用仿真来实现覆盖率收敛是很难的。仿真所用的时间和测试运行的次数与已完成覆盖率目标的百分比增长之间不呈线性关系。 如下图所示,尽管随着时间的推移,仿真运行次数不断增加,但覆盖曲线却趋于平缓。这通常归结于以下两个因素:1) 那些覆盖率目标在本质上就无法达到;2) 那些难以实现的覆盖率目标可能需要手动创建测试用例,因为受约束的随机仿真可能无法达到这些覆盖率目标。在某些情况下,运行无数的仿真测试用例并不能产生最佳投资回报率,也无法实现覆盖率收敛。 9968a64c-761e-11ed-8abf-dac502259ad0.png

形式验证如何加速

覆盖率收敛

形式验证可通过两种方式加速仿真覆盖率收敛:
  • 新思科技专为分未覆盖点的可达性推出了一款VC Formal应用,即Formal Coverage Analyzer(FCA)。该应用可以生成总结性报告,指出相关覆盖率目标是否可以达到。这种分析通常称为UNR(不可达性)。如果某个覆盖率目标无法达到,可能会导致两种行为:如果设计人员在审核后确认这符合预期,则可以将相关覆盖率目标从验证计划中移除,以便提高达成的覆盖率百分比;如果这在预期之外,则通常表示这是一个设计漏洞或过约束,此时需要用户采取行动来修复设计漏洞或放宽约束。

  • 形式验证发挥作用的另一种方式是覆盖属性。使用形式化技术验证断言时,工具将充分证明属性的正确性或生成反例,而覆盖属性则与此不同,其目标是让形式化工具生成一条轨迹来显示如何能达到该覆盖点。该轨迹有助于创建新的仿真测试用例,以便打到难以覆盖的覆盖率目标。

VCS+VC Formal

集成的优势

虽然仿真和形式验证之间的协同作用并不强求两种技术一定要来自同一家EDA供应商,但如果这两种解决方案拥有其他技术共性,则会有更多好处。 新思科技符合行业标准的VCS仿真器和新思科技的创新型VC Formal解决方案拥有很多有价值的联系,能够让终端用户从中获益。 9984fe00-761e-11ed-8abf-dac502259ad0.png
  • 新思科技VCS解决方案与新思科技VC Formal解决方案共享一个通用编译前端。统一的编译确保VC Formal可以轻松地应用于VCS验证环境,并确保对设计语义和意图的解释一致。

  • 新思科技的VC Formal FCA应用可以在VCS shell内原生调用,以进行可达性分析来识别不可达目标,从而创建一个排除文件并反馈给VCS环境,以此提高仿真覆盖率。

  • 新思科技VC Formal FPV应用中运行的覆盖属性可帮助创建更多的仿真测试用例,以覆盖随机仿真难以打到的点。

  • 使用新思科技的VCS和VC Formal解决方案时,可以合并仿真和形式化覆盖率数据库。这样一来,使用一种技术验证的设计便无需使用另一种技术再次进行验证。这也大大加速了验证收敛和签核。

SoC验证时间

节约40%-80%

在使用新思科技的VCS和VC Formal解决方案后,很多客户发现验证时间节省了40%到80%,同时也对实现验证签核更有信心。下表显示了10种客户设计以及形式化分析在减少验证时间方面的影响。 99d96044-761e-11ed-8abf-dac502259ad0.png为了帮助客户最大限度地发挥形式化技术的优势,新思科技形式验证服务团队在世界各地提供专家支持,协助开展方法培训、验证审核和各种交钥匙项目

总结

凭借新思科技VCS与VC Formal解决方案的强大功能,形式化技术对于证明芯片设计的正确性有很大的帮助。通过使用形式化技术来增强仿真,开发者们可以加快覆盖率收敛,从而实现更高质量的设计。新思科技的VC Formal解决方案、Verdi解决方案与VCS功能验证解决方案互相紧密集成,能够提供当今复杂SoC验证所需的速度、容量和灵活性,并帮助开发者找出设计缺陷的根本原因。 更重要的是,开发者自己并不需要成为形式化专家,而只需利用这些解决方案就能取得成效。 新思科技芯片设计和验证解决方案共享通用技术和一致的设计诠释能够为验证开发者提供无缝的用户体验并带来更高的性能和生产力。新思科技产品“价值链”的持续创新能够帮助企业高效地设计下一代变革性产品。此外,新思科技的VC Formal解决方案还可与验证工具箱中的其他工具相互配合,助力开发者实现高质量的形式化签核。


原文标题:1+1>2:这两个工具,治好验证开发者的精神内耗

文章出处:【微信公众号:新思科技】欢迎添加关注!文章转载请注明出处。


声明:本文内容及配图由入驻作者撰写或者入驻合作网站授权转载。文章观点仅代表作者本人,不代表电子发烧友网立场。文章及其配图仅供工程师学习之用,如有内容侵权或者其他违规问题,请联系本站处理。 举报投诉
  • 新思科技
    +关注

    关注

    5

    文章

    790

    浏览量

    50321

原文标题:1+1>2:这两个工具,治好验证开发者的精神内耗

文章出处:【微信号:Synopsys_CN,微信公众号:新思科技】欢迎添加关注!文章转载请注明出处。

收藏 人收藏

    评论

    相关推荐

    HarmonyOS NEXT应用元服务开发Intents Kit(意图框架服务)习惯推荐方案开发者测试

    意图框架向开发者提供真机测试能力,即开发者可连接设备进行调测。开发者完成代码开发之后,功能正式上架应用市场前,可以在HarmonyOS NEXT设备上面进行自
    发表于 11-25 17:37

    HarmonyOS NEXT应用元服务开发Intents Kit(意图框架服务)事件推荐开发者测试

    意图框架向开发者提供真机测试能力,即开发者可连接设备进行调测。开发者完成代码开发之后,功能正式上架应用市场前,可以在HarmonyOS NEXT设备上面进行自
    发表于 11-18 17:39

    【RA-Eco-RA2E1-48PIN-V1.0开发板试用】1、资料获取、环境搭建及简单验证

    使用51、STM32等开发平台的开发者而言,瑞萨无疑是一全新的挑战,一尚未涉足的领域。 瑞萨并不随波逐流,主要表现在它的库函数、开发工具
    发表于 10-18 13:07

    OFFSET N1和N2这两个引脚不是都是两个输入性质的引脚吗?为什么会有固定的-12V输出呢?

    N2)发现,均存在一-12V的电源电压。 请问,OFFSET N1和N2这两个引脚不是都是两个
    发表于 09-10 07:58

    触发器的两个稳定状态分别是什么

    触发器作为数字电路中的基本逻辑单元,具有两个稳定状态,这两个状态通常用于表示二进制数码中的0和1
    的头像 发表于 08-12 11:01 698次阅读

    tftlcd画线程序里面xerr>distance和yerr>distance两个条件能成立吗?

    delta_x,delta_y中最大值,所以xerr>distance和yerr>distance这两个条件是不
    发表于 04-22 07:35

    I.MX6ULL-飞凌 ElfBoard ELF1板卡- 应用层更改引脚复用的方法

    工具读一下这两个寄存器 因为这两个寄存器是连续的,所以也可以使用这个命令直接读两个寄存器: 可以看出,这两个MUX寄存器的值为0,以UAR
    发表于 03-29 15:29

    嵌入式学习-飞凌ElfBoard ELF 1板卡 - 应用层更改引脚复用的方法

    工具读一下这两个寄存器 因为这两个寄存器是连续的,所以也可以使用这个命令直接读两个寄存器: 可以看出,这两个MUX寄存器的值为0,以UAR
    发表于 03-29 15:28

    爱立信旗下Vonage与AT&T合作,通过API为开发者提供更丰富的网络能力

    近日,爱立信旗下的Vonage正在与美国跨国电信运营商AT&T合作,通过API为开发者和企业提供更丰富的网络能力。
    的头像 发表于 03-21 10:37 1.2w次阅读

    放大器器件手册上为什么会有MAG和MSG这两个指标呢?

    需要外匹配的管子的手册上,经常会有MAG和MSG这两个指标。
    的头像 发表于 03-18 18:21 3612次阅读
    放大器器件手册上为什么会有MAG和MSG<b class='flag-5'>这两个</b>指标呢?

    源码开放,开发者手机 buff 叠满

    开发者手机开源代码编译指导 编译环境建议: ubuntu20.04 Linux 系统内存:最低 16G Pyhon 3.8 安装必要工具: sudo apt-get update sudo
    发表于 03-04 14:29

    1+1&;amp;gt;2!它们组合可以同时实现高精度和高输出功率

    性能。市面上很少能见到兼具所有这些特性的运算放大器。但是,您可以使用两个单独的放大器来构建这种放大器,形成复合放大器。将两个运算放大器组合在一起,就能将各自的优势特性集成于
    的头像 发表于 02-20 08:22 416次阅读
    <b class='flag-5'>1+1&</b>;<b class='flag-5'>amp</b>;<b class='flag-5'>gt</b>;<b class='flag-5'>2</b>!它们组合可以同时实现高精度和高输出功率

    基于ZWS云和LoRa网关的环境监测“1+1&;amp;gt;2”方案

    环保部门在治理环境污染问题时,面临的一重要挑战是如何实时掌握不同地区的环境情况。为了解决这一问题,本文将介绍一种基于ZWS云和LoRa网关的环境监测“1+1>;2”方案。传统的环境监测方法需要
    的头像 发表于 12-22 08:24 670次阅读
    基于ZWS云和LoRa网关的环境监测“<b class='flag-5'>1+1&</b>;<b class='flag-5'>amp</b>;<b class='flag-5'>gt</b>;<b class='flag-5'>2</b>”方案

    【涂鸦T2-U开发板试用体验】开发者注册&amp;amp;产品固件下载

    开发即可。 产品创建成功以后产品需要有授权才能接入涂鸦iot平台,每个产品有两个免费测试授权可以申请,如果使用T2-U开发板 板子上已经有预制授权,不需要单独申请。 交付形式务必
    发表于 12-17 23:03

    零欧姆电阻器额定功率如何计算?注意,这两个参数很关键!

    零欧姆电阻器额定功率如何计算?注意,这两个参数很关键!
    的头像 发表于 12-05 17:29 786次阅读
    零欧姆电阻器额定功率如何计算?注意,<b class='flag-5'>这两个</b>参数很关键!