从小众走向普及,形式化验证对系统级芯片开发有多重要?

原创 新思科技 2023-04-21 18:07

形式化验证作为一种全新的验证方法,近年来在芯片开发中快速发展,正逐渐取代传统的仿真方法。


虽然仿真在系统级验证方面仍然发挥着重要的作用,但对于单元级的signoff而言,形式化验证已经成为首选。据估计,在未来五年内仿真将逐渐被取代,仅用于子系统和系统级验证。与此同时,形式化验证方法已经开始处理一些系统级任务,随着技术的不断创新,形式化验证将逐步开始处理更多系统级任务。


形式化验证的普及

近五年来,更多机构和设计验证人员更广泛地参与到了整体验证目标之中。除了率先在半导体设计中采用形式化验证技术的英特尔公司以外,还有很多其他半导体和系统公司的开发者们开始积极地尝试这一技术。


这种扩张一定程度是因为验证结果比以往更加容易获取,以及可以被更好地量化。“应用程序”概念的出现极大地缩短了有效验证的学习曲线,对覆盖率定义的改进也让开发者们更加相信,形式化验证以得到有效衡量。此外,属性检查证明了形式化验证可以解决仿真所无法解决的难题。


这些成功的案例激发了开发者们对形式化验证更深入的思考:作为一种有效的验证技术,形式化验证是否只适用于特殊情况,或者是否有可能显著提高整体验证任务的贡献?


形式化signoff的挑战


对形式化技术而言,如果其能够取代动态技术,以更低的成本实现更高质量的signoff,那将是又一重大突破。


近年来商业形式化验证方法的积极应用,以及通过C到RTL等价性检查所做的规范级别比较,对于实现这一目标有着标志性的意义。现如今有多个模块仅通过形式化验证即可进行signoff,动态调试对signoff而言,虽仍然重要,但作用已被削弱。


考虑到数据路径元件在GPU、DSP、AI和当今许多其他加速器中的重要性,突破数据路径边界是利用形式化验证技术完成绝大多数单元signoff任务的关键一步。这种从动态signoff到形式化signoff的变化,大大提升了生产力。而以往的实验证明,用这一方法signoff的一些关键模块在多代产品中没有出现一个错误。运用形式化技术达到了更高的生产率和更高的质量,这一点已然被证实。


扩大形式化验证方法的ROI:
架构验证


在架构验证领域,形式化验证方法也取得了很大的成功。其相关应用主要包括:


  • 一致性网格结构的正确性
  • CPU集群上运行的固件的正确性

形式化验证方法的ROI不断得到验证和扩大。目前,这些技术主要依赖于开发者们在抽象化设计方面的开发经验和专业知识,以及各种开源工具和一些商业产品。随着时间推移,会有更多类似的功能实现标准化。


形式化验证开发人才需求增加


相比于动态测试,形式化验证的本质要求开发者对设计有更详细的了解。随着工业界对形式化验证提出更多需求,许多头部公司和一些掌握尖端科技的初创公司都在努力提高形式化验证的能力,这就对开发者的能力提出了更高且更新的要求。


目前企业倾向于开展基础培训来帮助应届毕业生了解和进入行业,在接受培训后,形式化验证开发者往往对工作的热情要远高于其他人,而在大学校园内,亦设置了EE/CS本科相关课程来支持行业对形式化验证开发人才的需求,期待相关专家人才迅速增多,去探索自己职业所面临的挑战和机遇。


形式化验证未来展望


五年前,有人可能认为形式化验证是解决专门问题的小众技术,但这种观点现在已经逐渐被改变。现在,大型系统和半导体公司将形式化验证视为任何可信验证策略的重要组成部分。更重要的是,形式化验证方法现在已经发展到可在某些领域中取代仿真的地步。形式化验证开始为系统级领域做出贡献,而在以前,形式化验证在这些领域被认为是不切实际的。


对于形式化验证和形式化验证团队来说,这是一个令人兴奋的时代。由于贡献不断增大和在业务关键型需求上为人们带来的更多信心,形式化验证技术对所有数字设计领域的产品设计和开发变得越来越重要。


扫描下方二维码,下载白皮书《形式化验证探索指南》,详细了解形式化验证的更多相关内容。


                                   
   

新思科技 新思科技(Synopsys, Inc.)以芯片产业的“根技术”推动AI、5G、高性能计算、智能汽车等前沿应用的核心技术发展。
评论
  • 每日可见的315MHz和433MHz遥控模块,你能分清楚吗?众所周知,一套遥控设备主要由发射部分和接收部分组成,发射器可以将控制者的控制按键经过编码,调制到射频信号上面,然后经天线发射出无线信号。而接收器是将天线接收到的无线信号进行解码,从而得到与控制按键相对应的信号,然后再去控制相应的设备工作。当前,常见的遥控设备主要分为红外遥控与无线电遥控两大类,其主要区别为所采用的载波频率及其应用场景不一致。红外遥控设备所采用的射频信号频率一般为38kHz,通常应用在电视、投影仪等设备中;而无线电遥控设备
    华普微HOPERF 2025-01-06 15:29 164浏览
  • 「他明明跟我同梯进来,为什么就是升得比我快?」许多人都有这样的疑问:明明就战绩也不比隔壁同事差,升迁之路却比别人苦。其实,之间的差异就在于「领导力」。並非必须当管理者才需要「领导力」,而是散发领导力特质的人,才更容易被晓明。许多领导力和特质,都可以通过努力和学习获得,因此就算不是天生的领导者,也能成为一个具备领导魅力的人,进而被老板看见,向你伸出升迁的橘子枝。领导力是什么?领导力是一种能力或特质,甚至可以说是一种「影响力」。好的领导者通常具备影响和鼓励他人的能力,并导引他们朝着共同的目标和愿景前
    优思学院 2025-01-08 14:54 61浏览
  • 在智能家居领域中,Wi-Fi、蓝牙、Zigbee、Thread与Z-Wave等无线通信协议是构建短距物联局域网的关键手段,它们常在实际应用中交叉运用,以满足智能家居生态系统多样化的功能需求。然而,这些协议之间并未遵循统一的互通标准,缺乏直接的互操作性,在进行组网时需要引入额外的网关作为“翻译桥梁”,极大地增加了系统的复杂性。 同时,Apple HomeKit、SamSung SmartThings、Amazon Alexa、Google Home等主流智能家居平台为了提升市占率与消费者
    华普微HOPERF 2025-01-06 17:23 202浏览
  • 本文介绍编译Android13 ROOT权限固件的方法,触觉智能RK3562开发板演示,搭载4核A53处理器,主频高达2.0GHz;内置独立1Tops算力NPU,可应用于物联网网关、平板电脑、智能家居、教育电子、工业显示与控制等行业。关闭selinux修改此文件("+"号为修改内容)device/rockchip/common/BoardConfig.mkBOARD_BOOT_HEADER_VERSION ?= 2BOARD_MKBOOTIMG_ARGS :=BOARD_PREBUILT_DTB
    Industio_触觉智能 2025-01-08 00:06 92浏览
  • 根据环洋市场咨询(Global Info Research)项目团队最新调研,预计2030年全球无人机锂电池产值达到2457百万美元,2024-2030年期间年复合增长率CAGR为9.6%。 无人机锂电池是无人机动力系统中存储并释放能量的部分。无人机使用的动力电池,大多数是锂聚合物电池,相较其他电池,锂聚合物电池具有较高的能量密度,较长寿命,同时也具有良好的放电特性和安全性。 全球无人机锂电池核心厂商有宁德新能源科技、欣旺达、鹏辉能源、深圳格瑞普和EaglePicher等,前五大厂商占有全球
    GIRtina 2025-01-07 11:02 119浏览
  • 故障现象一辆2017款东风风神AX7车,搭载DFMA14T发动机,累计行驶里程约为13.7万km。该车冷起动后怠速运转正常,热机后怠速运转不稳,组合仪表上的发动机转速表指针上下轻微抖动。 故障诊断 用故障检测仪检测,发动机控制单元中无故障代码存储;读取发动机数据流,发现进气歧管绝对压力波动明显,有时能达到69 kPa,明显偏高,推断可能的原因有:进气系统漏气;进气歧管绝对压力传感器信号失真;发动机机械故障。首先从节气门处打烟雾,没有发现进气管周围有漏气的地方;接着拔下进气管上的两个真空
    虹科Pico汽车示波器 2025-01-08 16:51 69浏览
  • 村田是目前全球量产硅电容的领先企业,其在2016年收购了法国IPDiA头部硅电容器公司,并于2023年6月宣布投资约100亿日元将硅电容产能提升两倍。以下内容主要来自村田官网信息整理,村田高密度硅电容器采用半导体MOS工艺开发,并使用3D结构来大幅增加电极表面,因此在给定的占位面积内增加了静电容量。村田的硅技术以嵌入非结晶基板的单片结构为基础(单层MIM和多层MIM—MIM是指金属 / 绝缘体/ 金属) 村田硅电容采用先进3D拓扑结构在100um内,使开发的有效静电容量面积相当于80个
    知白 2025-01-07 15:02 141浏览
  • 大模型的赋能是指利用大型机器学习模型(如深度学习模型)来增强或改进各种应用和服务。这种技术在许多领域都显示出了巨大的潜力,包括但不限于以下几个方面: 1. 企业服务:大模型可以用于构建智能客服系统、知识库问答系统等,提升企业的服务质量和运营效率。 2. 教育服务:在教育领域,大模型被应用于个性化学习、智能辅导、作业批改等,帮助教师减轻工作负担,提高教学质量。 3. 工业智能化:大模型有助于解决工业领域的复杂性和不确定性问题,尽管在认知能力方面尚未完全具备专家级的复杂决策能力。 4. 消费
    丙丁先生 2025-01-07 09:25 116浏览
  • By Toradex 秦海1). 简介嵌入式平台设备基于Yocto Linux 在开发后期量产前期,为了安全以及提高启动速度等考虑,希望将 ARM 处理器平台的 Debug Console 输出关闭,本文就基于 NXP i.MX8MP ARM 处理器平台来演示相关流程。 本文所示例的平台来自于 Toradex Verdin i.MX8MP 嵌入式平台。  2. 准备a). Verdin i.MX8MP ARM核心版配合Dahlia载板并
    hai.qin_651820742 2025-01-07 14:52 106浏览
  •  在全球能源结构加速向清洁、可再生方向转型的今天,风力发电作为一种绿色能源,已成为各国新能源发展的重要组成部分。然而,风力发电系统在复杂的环境中长时间运行,对系统的安全性、稳定性和抗干扰能力提出了极高要求。光耦(光电耦合器)作为一种电气隔离与信号传输器件,凭借其优秀的隔离保护性能和信号传输能力,已成为风力发电系统中不可或缺的关键组件。 风力发电系统对隔离与控制的需求风力发电系统中,包括发电机、变流器、变压器和控制系统等多个部分,通常工作在高压、大功率的环境中。光耦在这里扮演了
    晶台光耦 2025-01-08 16:03 58浏览
我要评论
0
点击右上角,分享到朋友圈 我知道啦
请使用浏览器分享功能 我知道啦