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

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

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

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

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

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

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

目的

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

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

形式验证技术

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

g9tEETC-电子工程专辑

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

模型检查

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

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

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

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

优点和缺点

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

定理证明

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

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

优点和缺点

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

等价性检查

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

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

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

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

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

总结

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

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

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

本文为EET电子工程专辑 原创文章,禁止转载。请尊重知识产权,违者本司保留追究责任的权利。
您可能感兴趣的文章
  • 谁仍在惧怕难搞的电容负载变化?斩波放大器? 零点漂移和斩波放大器具有复杂的输出阻抗,因此在输出端出现电容负载时很难稳定。我将展示如何使用带双反馈的Riso来补偿斩波稳定运算放大器的电容负载。
  • 5G毫米波空口测试挑战与解决方法 Sub-6GHz频段可以沿用4G时期的一些技术,与之相关的射频器件产业链也相对成熟,但由于该频段资源有限,业界将目光投向了资源相对丰富的毫米波频段。毫米波频段的优势是具备大量的可用频谱带宽、波束窄、方向性好等,但这也将给未来5G终端及基站的测试带来诸多挑战。本文将从测试角度探讨毫米波芯片带来的挑战及解决方法。
  • 华为5款手机被移出GeekBench跑分榜单 日前,国外知名跑分平台Geekbench更新排名名单,同时也公布了最新黑名单,有六款设备因人工干预上榜,五款华为,一款一加。型号分别的华为Mate 10 Pro、华为P20 Pro、华为Mate 10、华为P20、华为荣耀Play、一加手机5……
  • 芯片设计如何跑赢汽车电子系统的安全性和可靠性竞赛? 无论是此前自动驾驶汽车失控导致车毁人亡,还是近段时间发生的多起高端新能源汽车因为电池/电路原因导致自燃的事件,都不禁让人感叹,这些电子技术制成的创新汽车产品,什么时候才能让人开起来更安心,停在车库里更放心呢?在笔者看来,新时代的汽车电子如果要实现安全性和可靠性,主要有以下四个障碍需要跨越。
  • LitePoint 5G实验室近日台北正式落成 LitePoint 5G实验室配合已经推出的单机测试系统 IQgig-5G, 大量简化设定与校准时间,帮助客户快速解决问题。
  • 从电源管理到无线兼容,解决物联网测试面临的五大挑战 在未来几年,AI、5G、IoT和工业自动化(IIoT)的进步将加快行业变革和创新的步伐。跨行业的各种物联网传感器将用于自动数据传输和远程设备控制。在万物互联的时代,连接将变得司空见惯,到2020年,Gartner预计将有超过200亿台物联网设备投入使用。
相关推荐
    广告
    近期热点
    广告
    广告
    广告
    可能感兴趣的话题
    广告