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

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

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

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

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

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

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

目的

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

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

形式验证技术

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

RH3EETC-电子工程专辑

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

模型检查

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

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

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

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

优点和缺点

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

定理证明

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

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

优点和缺点

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

等价性检查

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

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

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

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

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

总结

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

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

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

本文为EET电子工程专辑 原创文章,禁止转载。请尊重知识产权,违者本司保留追究责任的权利。
您可能感兴趣的文章
  • 干货:华为“鸿蒙”所涉及的微内核究竟是什么? 关于微内核的定义,这里有一份简单的描述:内核运行在内核态,只包含基本的多任务调度功能;其他系统服务都运行在用户态,包括文件系统,网络协议栈,甚至内存管理,驱动都是一个个独立的用户态进程,并相互做内存隔离。应用需要使用系统服务时,都通过IPC发送消息来使用其他用户态服务。
  • 电动汽车中的SiC开关将会主导动力传动系统吗? 宽带隙(WBG)半导体正被应用于包括电动汽车在内的各类功率转换器中。其承诺的更高效率和更快转换速率将节省成本、尺寸和能源,它通常被运用在充电器和辅助转换器中,但尚未在牵引逆变器中大量取代IGBT。本文将介绍最新一代SiC FET,因其提供低于IGBT的损耗以及在高温和多重应力下被证实的短路鲁棒性,而成为新型逆变器设计的绝佳选择。
  • 如何让MCU进入睡眠状态节省能耗? 我们探讨过在每种Arm Cortex-M处理器上可以找到的低功耗模式的基本原理,以及如何使用WFI和WFE指令让处理器进入睡眠模式。实际上我们真正要了解的是,低功耗模式如何在真正的微控制器上实现?这些模式是如何影响嵌入式系统的?在这篇文章中,我们将更详细探讨如何让微控制器进入睡眠状态并看看到底能够节省多少能耗。
  • 硬件安全在实现工业4.0愿望中的作用 涉及工厂数字化的工业4.0对工业市场领域的组织领导者来说有着不同的意义,随着工厂设备变得智能化和互联,数字化影响可能对网络安全产生广泛的影响。工厂的数字化正在改变价值链的各个方面,并直接影响企业的顶线和底线。
  • 112Gbps LR SerDes PHY采用CTLE和时间交错闪存ADC以降 目前最先进的112Gbps LR SerDes PHY要求最大限度地减少ADC位数,从而通过减少比较器的数量和最小化DSP中的位数来为整个系统提供最小的芯片面积和功耗开销。在这项设计工程中,CTLE的价值在于降低了所需的ADC分辨率。在CTLE电路和闪存ADC尺寸与数量之间寻找平衡点,对最小化ADC位数以实现最小系统面积和功耗开销起着关键作用。
  • 为物联网优化传感器网络设计 在当今对成本敏感的环境中,每个部署的传感设备或网络都必须在开发和部署的复杂性与物联网服务提供商、云计算公司和最终用户的价值之间取得平衡。在已部署的传感器网络中,我们现在看到的趋势是:简化网络并仅测量那些可以协助节省成本和/或增强最终用户体验的内容。
相关推荐
    广告
    近期热点
    广告
    广告
    广告
    可能感兴趣的话题
    广告