向右滑动:上一篇 向左滑动:下一篇 我知道了
广告

形式验证简介及其三种技术形式

时间:2019-07-19 阅读:
形式验证是一种自动检查方法,它可以捕获许多常见的设计错误,并发现设计中的歧义之处。硬件系统有许多应用都至关重要,其产生的任何故障都可能导致极大的经济损失或物理损害。 本文将讨论形式验证及其各种技术形式。

形式验证是一种自动检查方法,它可以捕获许多常见的设计错误,并发现设计中的歧义之处。6u2EETC-电子工程专辑

形式验证是使用数学方法验证设计正确性的过程。其工具使用各种算法来验证设计,但不执行任何时序检查。这些工具不需要激励或测试平台,在IC设计周期的早期即可执行,也就是说,只要RTL代码可用,即可执行形式验证。因此,发现问题越早,修复就越容易。6u2EETC-电子工程专辑

形式验证的普及得益于英特尔处理器中发现的著名的奔腾漏洞,那次事件导致故障处理器被召回,英特尔不得不承担了近5亿美元的损失。还有其他各种事故,比如阿丽亚娜5型火箭的爆炸和巴拿马癌症研究所辐射计量超标事故等,实际上都可以通过形式验证得以避免。6u2EETC-电子工程专辑

硬件系统有许多应用都至关重要,其产生的任何故障都可能导致极大的经济损失或物理损害。 本文将讨论形式验证及其各种技术形式。6u2EETC-电子工程专辑

目的

形式验证技术可以追踪标准验证技术检测不到的错误。而且,若使用标准技术检测可以检测到错误,那形式验证通常可以以明显更快的速率识别错误。在通过模拟和仿真对设计进行功能验证之前,通常就已执行了形式验证。6u2EETC-电子工程专辑

形式验证的一些优点如下:6u2EETC-电子工程专辑
· 在设计周期早期发现bug6u2EETC-电子工程专辑
· 耗时更少6u2EETC-电子工程专辑
· 可靠6u2EETC-电子工程专辑
· 更快6u2EETC-电子工程专辑
· 更详尽6u2EETC-电子工程专辑

形式验证技术

下图说明了各种形式验证技术:6u2EETC-电子工程专辑

6u2EETC-电子工程专辑

图1:形式验证技术(来源:Aijaz Fatima)6u2EETC-电子工程专辑

模型检查

模型检查,也称为属性检查,是一种基于状态的形式验证方法。6u2EETC-电子工程专辑

以下步骤说明了模型检查的过程:6u2EETC-电子工程专辑

1. 对系统进行建模以得到模型M。具体来讲,系统被建模为一组状态,而状态之间具有转换,转换用于描述系统如何响应内部或外部刺激从一种状态变换到另一种状态。6u2EETC-电子工程专辑
2. 使用属性规范语言(如PSL或SVA)创建要验证的属性,以得到公式ɸ。属性是设计行为的描述。6u2EETC-电子工程专辑
3. 运行模型检查器以确定模型M是否满足公式ɸ。6u2EETC-电子工程专辑
4. 如果模型不满足属性,则生成反例。反例是违反属性的刺激,通常用仿真中的波形来表示。6u2EETC-电子工程专辑
5. 在仿真中使用系统模型运行反例以查找错误位置。6u2EETC-电子工程专辑

20190719-002.gif6u2EETC-电子工程专辑
图2:模型检查的程序(来源:Aijaz Fatima)6u2EETC-电子工程专辑

优点和缺点

一旦将系统模型和属性规范提供给模型检查器,验证过程就将是完全自动的。但是,从模型检查器要处理的状态数来看,模型检查适用于小型系统。6u2EETC-电子工程专辑

定理证明

定理证明是使用数学推理方法验证所实现的系统是否满足设计要求(或规范)的过程。它是一种基于证据的形式验证方法。6u2EETC-电子工程专辑

以下步骤解释了定理证明的过程:6u2EETC-电子工程专辑
1. 在形式数学逻辑中将系统建模为一组数学定义。6u2EETC-电子工程专辑
2. 从数学定义中导出系统的属性。6u2EETC-电子工程专辑
3. 使用定理证明器验证系统是否符合规范。定理证明器也可以称为证明助理。目前有各种可用的定理证明器,根据其基础逻辑进行分类。6u2EETC-电子工程专辑
20190719-003.gif6u2EETC-电子工程专辑
图3:定理证明的程序(来源:Aijaz Fatima)6u2EETC-电子工程专辑

优点和缺点

定理证明的最大优点是它可以处理非常复杂的系统。但是,定理证明不是完全自动的,需要人工干预才能完成,这需要时间以及操作人员的专业知识。而且,在证明失败的情况下,不会生成反例,这也使得定位错误相对困难。6u2EETC-电子工程专辑

等价性检查

等价性检查是验证两个设计在功能上是否相同的过程。两种等价性检查技术如下:6u2EETC-电子工程专辑

逻辑等价性检查(LEC):也称为组合等价性检查,它是验证两个设计在寄存器之间具有相同组合逻辑的过程。两个被比较的设计也应具有相同数量的寄存器。该技术用于验证不同抽象级别的两个设计在功能上是否相同;例如,门级网表在功能上与布局网表是否相同。6u2EETC-电子工程专辑

20190719-004.gif6u2EETC-电子工程专辑
图4:逻辑等效性检查(来源:Aijaz Fatima)6u2EETC-电子工程专辑

顺序等价性检查(SEC):顺序等价性检查是验证两个设计在功能上是否相同的过程,并且在提供相同输入时验证是否有相同的输出。它用于比较两种设计的顺序逻辑,而这两种设计可能有不同的实现。SEC是一个复杂的过程,因此非常受设计规模的限制。6u2EETC-电子工程专辑

有时,IC的设计会在最后一刻进行修改,以合并一些功能、时序、电源或其他修复,或者包括一些额外的逻辑,如扫描逻辑、电源控制电路等。这些变化也需要验证。标准验证程序会耗费大量时间,因此会推迟产品上市时间。而顺序等效性检查将修改后的设计与标准设计进行比较,并验证它们在功能上是否一致。6u2EETC-电子工程专辑
20190719-005.gif6u2EETC-电子工程专辑
图5:顺序等效性检查(来源:Aijaz Fatima)6u2EETC-电子工程专辑

总结

总而言之,形式验证是一种自动检查方法,可以捕获许多常见的设计错误,并可以发现设计中的歧义之处。它是一种详尽的方法,涵盖了所有输入场景,还可以检测边角案例异常。6u2EETC-电子工程专辑

形式验证可以节省设计人员的时间和精力,因为潜在问题在开发测试环境之前即被发现。它可用于设计的高级描述、RTL或GLS表示等阶段。市场上有各种各样复杂的形式验证工具,其中许多工具还提供按钮方式用以查找设计中的问题。6u2EETC-电子工程专辑

本文同步刊登于电子工程专辑杂志2019年7月刊6u2EETC-电子工程专辑

本文为EET电子工程专辑 原创文章,禁止转载。请尊重知识产权,违者本司保留追究责任的权利。
您可能感兴趣的文章
  • 嵌入式平台上的自动音频接口测试 从模拟音频到数字音频端口,各种类型的接口层出不穷。每种类型的接口在设计和测试中都面临自身的挑战。在组装和生产过程中,这些接口的测试涵盖了整个路径,从模拟或数字前端到处理单元的数字音频输入端口。本文介绍一种常用的技术,用于检测音频接口测试中与装配相关的故障问题。
  • 解决物联网设备在电池寿命结束时遇到的关键问题 许多物联网应用都依靠小型非充电式电池供电,因此优化电池续航时间非常重要。为了了解产品的电池功耗特征,制造商纷纷使用各种工具来执行电池功耗分析。因为物联网演进极为迅速,产品开发周期非常短。设计和验证工程师必须快速了解其设备的功耗特征及其产生原因,因此需要将功耗与射频及子电路事件关联起来。许多工程师发现,基于事件的功耗分析可以快速揭示他们需要重点关注的事件,有针对性地改善设备的功耗特性。
  • 精通5G网络的秘密武器——5G移动网络测试 在过去的二十年间,无线网络迅速发展,波束成形、大规模多输入多输出、毫米波频谱、以及新的更灵活的空中接口,这些5G关键技术将网络复杂性提升到了一个全新的水平。执行网络测试对于成功的5G商业部署变得至关重要。同时,工程师们在确保避免仓促执行5G现场网络测试的同时,找到合适的合作伙伴以应对这些现场测试5G网络的新挑战也是至关重要。
  • 深圳制造中国首颗极地遥感专用卫星,预计9月升空 8月14日,“三极遥感星座观测系统”的首颗试验卫星——京师一号在深圳包装入箱,预计在今年9月发射升空。南极和北极遥感系统通过每天对极地区域的全覆盖观测,对支撑国家北极航道开发和环境保护意义重大。
  • 测试专家用实例告诉你如何用好示波器 在电源设计中稳定性是一项非常重要的指标,根据反馈理论,一个反馈系统的稳定性可以通过其系统传递函数得出。工程实践中通常会使用环路增益的波特图来判断系统的稳定性。
  • “后段”突围!华为联手台厂自组供应链 据报道,因美方禁令封锁,华为联合台湾地区半导体厂商一起突围,日月光投控旗下矽品成为华为第一家青睐的台资厂商。矽品位于福建晋江的封测厂,原本是为了配合联电与福建晋华合作的存储器厂而设立,但福建晋华新建12吋厂计划已停摆,故将转为为海思提供来自台积电南京厂生产的芯片后段封测服务。
相关推荐
    广告
    近期热点
    广告
    广告
    广告
    可能感兴趣的话题
    广告