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

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

形式验证是使用数学方法验证设计正确性的过程。其工具使用各种算法来验证设计,但不执行任何时序检查。这些工具不需要激励或测试平台,在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月刊

阅读全文,请先
您可能感兴趣
早在十多年前,电动汽车就已经引入400V电池系统,现在我们看到行业正在向800V系统迁移,主要是为了支持直流快速充电。随着电压的提高和从400V系统中学到的经验教训,设计人员现在正专注于增强高压保护电路的性能并提高可靠性。他们正在重新评估使用熔丝、接触器或继电器的现有解决方案,以寻找响应速度更快、稳健性更强且可靠性更高的解决方案,如热熔丝和电子熔丝(即E-Fuse)。
对于工程师来说,当不同的工程有不同的电池充电需求时,设计使用可充电电池并为消费者提供出色充电体验的应用可能具有挑战性。如果对每个应用使用专用的电池充电器,会增加设计时间,因为您必须重新设计、调试和重新鉴定每个新电路。
自ChatGPT带火AI以来,AI芯片得到了空前的发展,十月底高通发布了基于Arm架构的带有AI算力的骁龙X Elite芯片。刚刚,Arm宣布将在2024年推出Cortex-M52芯片,为低功耗物联网设备带来AI加速功能。
因应人工智能(AI)等应用对于更高效能计算的需求,以及小芯片(chiplet)异质整合架构的挑战,英特尔(Intel)打造可用于下一代先进封装的玻璃(Glass Core)衬底...
由于电子器件的频率和性能不断提高,要求与之匹配的二极管必须具备恢复时间短,反向恢复电流小和软恢复等特点。而快恢复二极管(FRD)因具备上述特点而被广泛应用。本文简要介绍快恢复二极管的反向恢复过程,及基于TCAD软件工具采取一系列方法优化恢复二极管的反向恢复,使其能够实现快速而软的恢复。
网络中的各个元素必须符合特定的频率、相位和时间要求,以确保网络实现正确的端到端运行。由O-RAN联盟定义的同步架构决定了开放式RAN设备将如何满足这些要求。
根据TrendForce集邦咨询最新OLED技术及市场发展分析报告统计,在近期发表的摺叠新机中,UTG的市场渗透率已逾九成,随着摺叠手机规模持续成长,预估2023年UTG产值将达3.6亿美元;2024年可望挑战6亿美元。
随着终端及IC客户库存陆续消化至较为健康的水位,及下半年iPhone、Android阵营推出新机等有利因素,带动第三季智能手机、笔电相关零部件急单涌现,但高通胀风险仍在,短期市况依旧不明朗,故此波备货仅以急单方式进行。此外,台积电(TSMC)、三星(Samsung)3nm高价制程贡献营收亦对产值带来正面效益,带动2023年第三季前十大晶圆代工业者产值为282.9亿美元,环比增长7.9%。
治精微推出具过压保护OVP、低功耗、高精度运放ZJA3018
无线技术每天都在拯救生命,有些非常方式是人们意想不到的。在美国加利福尼亚州Scotts Valley,一名路过的慢跑者发现一处住宅冒出火焰后,按响了门铃,试图通知屋主。屋主不在家中,但无线门铃连接到了智能家居中枢,提醒屋主慢跑者试图联系。屋主立即向他提供了安全密码,让他跑进房子,从火场中救出了宠物。
作者:Jackie Gao,AMD工程师;来源:AMD开发者社区前言当FPGA开发者需要做RTL和C/C++联合仿真的时候,一些常用的方法包括使用MicroBlaze软核,或者使用QEMU仿真ZYNQ
点击左上角“锂电联盟会长”,即可关注!锂离子电池是一种二次电池(充电电池),它主要依靠Li+ 在两个电极之间往返嵌入和脱嵌来工作。随着能源汽车等下游产业不断发展,锂离子电池的生产规模正在不断扩大。本文
近日,Wi-Fi联盟宣布Wi-Fi 7规范将于第一季度末最终确定,为企业采用标准化硬件打开大门。 “基于 IEEE 802.11be 技术的 Wi-Fi CERTIFIED 7 将于 2024 年第一
AMD Vitis™ 高层次综合 ( HLS ) 已成为自适应 SoC 及 FPGA 产品设计领域的一项颠覆性技术,可在创建定制硬件设计时实现更高层次的抽象并提高生产力。Vitis HLS 通过将 C
为加强智慧应急能力建设,以新安全格局服务新发展格局,由中国科学院大学、全国安全职业教育教学指导委员会共同主办的“2023智慧应急发展论坛”于2023年12月10日在京召开。本次论坛主题是“加强智慧应急
广告分割线12月11日,据台媒报道,群创(3481.TW)竹南T1厂员工向媒体爆料,群创竹南T1厂将裁员50%!据报道,群创竹南厂工程师预计将减少一半,在线作业员也预计砍一半。群创今天表示,已于第一时
本文来源:物联传媒本文作者:市大妈前几年,对大部分人来说,FWA是一个比较陌生的领域,尽管早在3G和4G时代就已经得到一定的发展。后来,随着5G的发展,FWA作为当前5G应用量级最大的场景之一,被更多
点击左上角“锂电联盟会长”,即可关注!粉尘、水分和毛刺是锂离子电池生产过程中需要严格控制的关键因素。严格控制电池生产环境的粉尘对锂离子电池的安全和性能至关重要。生产环境粉尘控制不足会导致涂层表面产生大
本文来源:物联传媒“2023‘物联之星’中国物联网行业年度榜单” 评选活动正在火热进行中!为深度挖掘物联网领域的优秀企业、创新产品和优秀项目,审读年度热门领域和发展方向,推动物联网行业的普及与宣传,促
巨头动向腾讯今年回购金额已超过去10年总额12月11日,腾讯公告称,当日耗资约4.03亿港元,回购133万股股份。年初至今,腾讯已经出手113次,累计回购数量约1.28亿股,累计回购金额超过422亿港