广告

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

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

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

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

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

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

目的

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

形式验证的一些优点如下:
· 在设计周期早期发现bug
· 耗时更少
· 可靠
· 更快
· 更详尽

形式验证技术

下图说明了各种形式验证技术:

图1:形式验证技术(来源:Aijaz Fatima)

模型检查

模型检查,也称为属性检查,是一种基于状态的形式验证方法。

以下步骤说明了模型检查的过程:

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

20190719-002.gif
图2:模型检查的程序(来源:Aijaz Fatima)

优点和缺点

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

定理证明

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

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

优点和缺点

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

等价性检查

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

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

20190719-004.gif
图4:逻辑等效性检查(来源:Aijaz Fatima)

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

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

总结

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

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

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

本文为EET电子工程专辑 原创文章,禁止转载。请尊重知识产权,违者本司保留追究责任的权利。
  • 用碳化硅MOSFET设计一个双向降压-升压转换器 随着电池和超级电容等高效储能设备的大量使用,朝向更好的电流控制发展成为一种趋势。双向DC/DC转换器可以保持电池健康,并延长其使用寿命。
  • 集成动态过流检测的智能锁电机驱动器设计方案 本文介绍了使用高电压GreenPAK的一个特定示例,描述了针对特定电机和电池组的集成设计定制方法。这是一种非常灵活的电机控制解决方案,采用可配置的内部逻辑,可满足设计人员的需求。而且将电机驱动器集成进GreenPAK中,可以将整个电路放入很小的物理空间。
  • 采用片上网络(NoC)的新型FPGA数据架构赋能5G网络和数据 从5G网络的边缘到数据中心内部的交换机,通信和网络系统对芯片的功能带来了极大的压力,以支持其所需的计算能力和数据传输速率。传统的可编程逻辑为这些系统提供了灵活性和速率的最佳组合,但是近年来却因以太网等协议的速度提高到100G和400G而面临新挑战。
  • 在开关电源转换器中,如何充分利用SiC器件的性能优势? 碳化硅MOSFET越来越多用于千瓦级功率水平应用,涵盖如通电源,和服务器电源,和快速增长的电动汽车电池充电器市场等领域。碳化硅MOSFET之所以有如此的大吸引力,在于与它们具有比硅器件更出众的可靠性,在持续使用内部体二极管的连续导通模式(CCM)功率因数校正(PFC)设计
  • IoT设备安全性设计的八项原则 对于当今开发的每个嵌入式设备,都需要至关重要的强大安全性支持。物联网设备中的黑客攻击威胁格局日益严重,要求从设备的出厂发运开始就需要发挥其全面的安全性。本文将讨论实现更强大IoT设备安全性的步骤,并解释嵌入式安全性背后的不同概念,以及如何针对嵌入式设备安全性实施一致且包罗万象的方法。
  • 先进电子显微镜成像技术揭露垂直共振腔面射雷射的制程 本次制程分析的主轴为近期商用领域中的大热门,应用在人脸识别系统的垂直共振腔面射雷射。由制程工艺的角度出发,决定垂直共振腔面射雷射的质量有三大方面。
广告
热门推荐
广告
广告
广告
EE直播间
在线研讨会
广告
广告
面包芯语
广告
向右滑动:上一篇 向左滑动:下一篇 我知道了