|
技术文库首页
|
编程
|
IC
|
晶体管
|
精解
|
中频
|
其它
|
电源
|
基础
|
电脑
|
无线
|
液晶
|
微波
|
空调
|
手机
|
|
热水器
|
电动车
|
LED屏
|
焊机
|
您现在的位置: 华玉生活网 >> 技术文库 >> 基础 >> 正文>> 繁體中文

深层解析形式验证

  形式验证(Formal Verification)是一种IC设计的验证方法,它的主要思想是通过使用形式证明的方式来验证一个设计的功能是否正确。形式验证可以分为三大类:等价性检查(Equivalence Checking)、形式模型检查(Formal Model Checking)(也被称作特性检查)和定理证明(Theory Prover) 。

  等价性检查的验证用于验证RTL设计与门级网表、门级网表与门级网表是否一致。在进行扫描链重排、时钟树综合等过程中,都可以用等价性检查保证网表的一致性。等价性检查已经融入IC标准设计流程中。等价性检查在检查ECO时非常有用。例如,设计者在修改门级网表时,由于手误,错将一个或门写成或非门,等价性检查工具通过比较RTL设计与门级网表,可以很容易地发现这种错误。

  模型检查用时态逻辑来描述规范,通过有效的搜索方法来检查给定的系统是否满足规范。模型检查是目前研究的热点,但其验证的电路规模受限制这一问题还没有得到很好的解决。

  定理证明把系统与规范都表示成数学逻辑公式,从公理出发寻求描述。定理证明验证的电路模型不受限制,但需要使用者的人工干预和较多的背景知识。

在当前复杂的数字设计开发过程中,功能验证十分重要。虽然硬件的复杂度仍遵循摩尔定律持续增长,但是验证的复杂性更具挑战。事实上,随着硬件复杂性随时间呈双指数增长,验证复杂性理论上也呈指数增长。验证已被公认为是设计过程中的主要瓶颈:高达70%的设计开发时间和资源花在功能验证上。Collett International Research认为,即使在验证上花费如此巨大的精力和资源,功能性缺陷仍是芯片重新流片的头号原因。

  功能性验证挑战

  边际情形(corner-case)的缺陷是仿真伪像,由于以仿真为基础的验证具有非穷尽的固有特性,因此边际情形无法被检测到。事实上,不管你用多少时间仿真,也不管你的测试平台和发生器有多么智能,通过仿真验证设计意图对于最小电路以外的所有电路来说都是不完整的。基本的仿真伪像可以被分成三类:穷尽型、可控型和可观察型,如下表1所示。

  形式验证是一个系统性的过程,将使用数学推理来验证设计意图(指标)在实现(RTL)中是否得以贯彻。形式验证可以克服所有3种仿真挑战(表1),因为形式验证能够从算法上穷尽检查所有随时间可能变化的输入值。换句话说,没有必要表明如何激励设计或创建多种条件来实现较高的可观察性。

  虽然从理论上讲,仿真测试平台的输入端口针对待验证设计(DUV)具有较高的可控性,但测试平台对内部点的可控性一般较差。为了使用基于仿真的方法识别设计错误,以下条件必须保持:

  * 必须产生正确的输入激励,以激活(也就是敏感化)设计中某个点的缺陷

  * 必须产生正确的输入激励,以便将源自缺陷的所有效果传送到输出端口

  在使用基于仿真的验证时,需要规划设计中需要验证的对象:

  * 定义需要测试的各种输入条件

  * 创建功能性覆盖模型(确定是否做了足够的仿真)

  * 搭建测试平台(检查器,测试桩,发生器等)

  * 创建特定的直接测试

  * 成年累月的仿真

  现实中,工程师一直在反复做着这些事:运行测试、调试故障、再次仿真回归组、观察各种覆盖率指标,以及调整激励(例如操控输入发生器)以覆盖以前未覆盖的设计部分。

  这里我们讨论一个弹性缓存例子(见图1)。数据可以在时钟域间改变,能够根据两个时钟之间的相位和频率偏移做出调整。数据必须无损地通过弹性缓存进行传送,即使在设计允许时钟不完全同步的情况下。在这个案例中的一个功能性缺陷例子是在时钟有效沿对齐时由于数据的变化而出现的缓存溢出。这就可能要求对所有可能的输入条件进行大量的仿真和考虑,以建模和仿真这种错误行为。

  


  图1:弹性缓存框图

  高层要求

  许多公司已经采用基于断言的验证(ABV)技术来缩短验证时间,同时改进他们的整体验证工作。然而,一般采用的ABV专注于局部的、在仿真中使用的RTL实现相关断言。所有内部断言的汇聚不会表征或完整规定微架构定义的那种模块的端到端行为。此外,当设计实现改变时,这些局部性断言不能重复使用。换句话说,通过端到端属性(包括数据完整性和包顺序)和规定模块必需的黑箱行为,高层断言(我们在本文中指高层要求)提供高得多的设计功能覆盖率,并且能在各种设计实现和多个项目之间重复使用。更重要的是,通过形式性验证模块的高层要求集,可以使验证完整性和产能得到显著提高。因此,高层形式验证无需模块级仿真,可极大地缩短系统级验证时间。让我们详细地看看图2所示的高层要求。

  

  图2:要求与RTL断言对比。

  Y轴代表抽取层,X轴代表被某个特殊断言或要求覆盖的设计数量。沿Y轴越往上走,被高层要求覆盖的设计空间就越大。证实这些高层要求具有很高价值,原因有很多:

  1. 高层要求关系到微架构中的要求

  2. 高层要求关系到测试平台中的输出检查器组

  3. 高层要求覆盖了与工程师想要写入的数百条较低层断言相同的设计空间

  4. 高层要求覆盖了由于工程师遗漏的较低层断言的缺失而未被覆盖的设计空间

  最后一点我们这里举个例子,假如设计包含一个FIFO,并且工程师忘了编写一个断言来检查FIF从不下溢。这种安全性违例将由高层要求加以识别。然而,通过形式性地验证高层要求,高层要求违例的根源就能得以跟踪。例如,如果针对高层要求在影响锥中包含了FIFO,那么导致高层要求不能满足的下溢条件将被检测到。

  理想的形式验证工具要求具有一定的规模,以便穷尽地检查所有可能的输入条件以及设计中任意点的可控性和可视性(见表1)。我们的旗舰产品,例如JasperGold,就采用了高性能和大规模的形式验证技术,能够穷尽地验证模块是否满足源自微架构的高层要求。这款产品使用数学算法,因为不需要使用仿真测试平台或激励。

  

  表1:仿真与形式验证的比较

  本文小结

  形式验证要求你以不同的方式思考。例如,仿真是完全经验主义的做法,也就是说,你通过反复试验试图查明缺陷,这要花相当多的时间尝试所有可能的组合,因此永远不会完整。另外,由于工程师必须定义和产生大量输入条件,他们的工作重点将是如何在非设计目标基础上分解设计。另一方面,形式验证是穷尽式数学技术,允许工程师仅关注设计意图,或“什么是设计的正确行为?”。

  验证实现工作包括将多种输入条件定义为测试计划的一部分、创建功能覆盖模型、开发测试平台、创建输入激励发生器、编写指导性测试以及执行测试、分析覆盖率指标、调整激励发生器以面向未验证的设计部分,然后反复这一过程。纯形式验证技术则相反,专注于证实模块的端到端、直接对应微架构规范的高层要求,帮助用户戏极大提高项目的设计和验证产能,同时确保正确性。


瑞达币购买
桂山秋竹_唐年桂2023年
桂北云雾图_唐年桂202

  • 扩展阅读
  • 上一个文章:
  • 【返回网站首页】 【返回基础】
  • 下一个文章:
  • 【字体: 】【】【发表评论】【加入收藏】【告诉好友】【打印此文
    文章 软件 电影 商品

    相关文章

    本站公告

    • 扫一扫,打赏给我们,谢谢!

      本站2016年12月16日起取消ruida.org.cn域名,该域名正式作废,该域名发布任何信息与本站无关。


      启用ruida.orghy928.net域名;

      瑞达网,瑞达科技网宣

    最 新 热 门

    附页内镶内容
    健康养生 商场新品 股市K线、指标知识
     六种药酒配制法[11月7日]
     气血双补党参、麦冬、黄芪炖[11月29日]
     参桂再造丸_红参、肉桂、麻黄[11月29日]
     臂丛神经痛该怎样治疗[11月29日]
     舒筋络酊、百宝丹擦剂、参桂[11月29日]
     臂丛神经痛针灸治疗[11月29日]
     枳椇子别名:鸡爪梨,鸡爪果[11月29日]
     三七、丹参、西洋参功效与作[8月17日]
     枸杞泡姜芽(嫩姜)的做法及功[5月20日]
     十二原穴,可治疗全身疾病_中[2月2日]
     瑞达币购买
     桂山秋竹_唐年桂2023年新作品
     桂北云雾图_唐年桂2023年新作品
     广西2019年《高考指南》+《招生计
     金士科前置过滤器
     金牛前置过滤器
     USB口24系列编程器第二版含USB延
     液晶电视、液晶显示器图纸、维修
     彩电、显示器、DVD、EVD打印机等
     高清CRT彩电、显示器图纸刻录 4G
     [理财]分享:各种短视频赚钱方法评论、关注…
     [会员]股票证券投资专业交易实战控制系统
     [理财]2023年新版1分2分5分硬币回收价格表(…
     [理财]2023年新版1分2分5分硬币回收价格表(…
     [理财]2022 年新版1分2分5分硬币回收价格表…
     [理财]微信收款码如何开通商业版收信用卡费…
     [指标]R平方_基金指标
     [指标]标准差_基金指标
     [指标]平均回报_基金指标
     [基金]一些重要基金指标的解读入门
    装修案例 网站建设 电器维修
     一般水电安装几个常用尺寸[1月29日]
     三相电表接法及度数的正确读…[5月8日]
     万能通用卧室房门锁更换步骤…[2月22日]
     乳胶漆的八大施工步骤及涂刷…[2月14日]
     旧墙翻新步骤及注意事项[2月14日]
     屋面防水施工工艺流程及注意…[1月16日]
     专利产品“防污吸气帽”新产…[1月8日]
     鲁班尺吉数对照表高清图片查…[10月29日]
     砂浆胶作用与危害[9月21日]
     4种处理水泥地面起砂方法[9月21日]
     网页html点击切换显示内容完[11月7日]
     动易SiteWeaver6.6网站管理系[7月31日]
     中国阴历农历JS支持 HTML网页[2月26日]
     java script error 容错处理[2月15日]
     几款还不错的网页特效显示日[2月14日]
     图片可以调大小的代码[12月14日]
     动易SW6.8网站系统改自适应支[11月20日]
     网站建设_套餐服务[12月4日]
     网站建设-费用明细[12月4日]
     不显示出来的代码[12月3日]
     联想 小新Air 14 2019笔记本…[6月15日]
     滚筒洗衣机脱水声音大原因及…[4月17日]
     智能电视不能开机强制恢复出…[1月16日]
     各大品牌智能电视机恢复出厂…[1月16日]
     洗衣机自己排水或不存水漏水…[6月15日]
     海尔冰箱出现-03还滴滴报警[5月29日]
     TCL电视通用教程安装教程[2月2日]
     TCL L43V7300A-3D液晶彩电出…[2月2日]
     先锋液晶电视LED-32B550无光…[1月17日]
     智能电视主板的应用与维修(…[1月11日]
    电器资料 下载 读书
     视得安750D6对讲门铃工作原理…[9月13日]
     什么是量子芯片和光子芯片[5月14日]
     沃尔沃S90汽车遥控钥匙失灵的…[1月19日]
     LED显示屏瑞合信PLus单双色全…[12月22日]
     Windows 照片查看器无法显示…[8月6日]
     已经设置IE主页,但是打开还…[7月6日]
     如何调整空压机压力?空压机…[6月8日]
     剪映-视频编辑软件手机版使用…[5月28日]
     锂电池保护板作用及同口和分…[3月18日]
     怎么样让电脑显示农历?win7…[1月26日]
     [电影]《抓娃娃》高清电影
     [联想]Lenovo S540-14API Compl 
     [书籍]《墨子》原文注释译文
     [LED条屏]瑞合信单双色/全彩控制系统
     [LED条屏]LED显示屏瑞合信手机APP6.
     [书籍]全本新注聊斋志异
     [书籍]广西2023年高考指南 招生计
     [书籍]个人防护手册(第二版)
     [书籍]关于印发新型冠状病毒肺炎
     [书籍]新型冠状病毒肺炎防控方案
     广西高考2024~2022年历史类([6月25日]
     近百年龙年龙月龙日龙时具体[10月9日]
     广西2024年普通高校招生录取[6月25日]
     卷十五 杂守 第七十一原文注[6月11日]
     卷十五 号令 第七十原文注释[6月11日]
     卷十五 旗帜 第六十九原文注[6月11日]
     卷十五 迎敌祠 第六十八原文[6月11日]
     卷十五 第六十七(今阙)原文注[6月11日]
     卷十五 第六十六(今阙)原文注[6月11日]
     卷十五 第六十五(今阙)原文注[6月11日]
    珠宝玉器 在线电视台
     鸡血石与鸡血玉有什么区别[6月12日]
     鸡血玉[6月12日]
     鸡血石 (bloodstone)[6月12日]
     什么是莫桑石(Moissanite)[6月12日]
     可以戴钻石洗澡吗[1月22日]
     钻石如何保养才好呢?[1月22日]
     PT容易花的问题和钻戒保养问…[1月22日]
     切工 钻石的雕刻艺术[1月22日]
     如何保养好钻戒[1月22日]
     钻戒保养方法[1月22日]
     中央体育台
     中央新闻台
     宁夏卫视
     湖北卫视
     西藏卫视
     辽宁卫视
     河北卫视
     北京卫视
     政法频道
     农民频道
     湖南经视
     湖 南 台
     河南频道
     湖南卫视
     兵团卫视
     江苏卫视
     旅游卫视
     湖南都市
     七彩戏剧
     动漫秀场
     游戏风云
     法制天地
     魅力音乐
     新 娱 乐
     南 方 TV
     浙江卫视
     齐鲁频道
     山西影视
     东南卫视
     上海卫视
     贵州电视台
     重庆电视台
     山东卫视
     《抓娃娃》在线电影
     流浪地球2剧情介绍
     《万里归途》完整版
     《阿凡达2:水之道》耗资3.1
     2021港剧《梅艳芳》5集全.HD
     误杀2 -电影-完整版视频在线
     亲爱的/亲爱的小孩/打拐/家之
     《第一炉香》-电影-完整版视
     《扬名立万》-电影-完整版视
     长津湖-电影-完整版视频在线
    网友评论:(只显示最新10条。评论内容只代表网友观点,与本站立场无关!)
        没有任何评论

    | 服务声明 | 充值中心| 华安五金电器 | 收费标准| 论坛| 留言| 实用查询| 会员中心| 下载帮助| 设为首页|

    技术支持:瑞达科技 即时交谈QQ:237013889 QQ群:13810759 E-Mail:237013889@qq.com
    非盈利网站,如有侵权,请来信来电告知,第一时间处理,谢谢!
    桂ICP备17008104号 华玉生活网网站统计
    tj