中文 英语
知识中心
导航
知识中心

形式验证

形式验证包括数学证明,以表明设计符合某种特性
受欢迎程度

描述

有几种类型的形式化方法用于验证设计。

首先是等价性检验。这需要两个设计,它们可能处于相同或不同的抽象级别,并找到它们之间的功能差异。等价性检查可以进一步分解为两个主要领域——组合等价性检查,通常被称为等价性检查,和顺序等价性检查。

通过组合等价性检验,证明逻辑综合后的设计与输入RTL描述一致。它还用于显示当进行测试逻辑或其他门级转换时,没有功能受到影响。它比较了原始描述中对应寄存器之间的组合逻辑。

顺序等价性检查是一项新兴技术,它可以采用两个具有根本不同时间的设计,使一个未计时或部分计时的模型与一个RTL模型进行比较,或者在经过重新计时或其他转换以提高功率或其他设计质量的RTL模型之间进行比较。这是大规模采用高水平合成的必要技术。

形式验证的另一个主要分支是属性检查。属性定义了必须在设计中出现的行为,或者必须不可能出现的行为。第三种选择被称为公平条件,它将确保几个选项中的每一个都不会受到不公平的对待,例如在仲裁中。

在某些情况下,可能很难证明一个性质,而不是提供一个完整的证明,有限的证明是所有可能的。一个有界的证明可能会说,该行为是,或不是,在一个定义的时钟数量内,或从一个特定的开始状态,或当某些约束应用到系统时。


形式化验证能力成熟度模型(正式的CMM)已经提出了作为一种将正式验证方法的进展定义为“级别”的方法,每个级别具有不同的目标、训练和工具需求。

第一级是自动形式检查,它关注于小的、具体的问题。第二层介绍了正式的应用程序,其中用户指定有关设计意图的内容,工具生成断言。在第三层,编写有目标的断言。这前三个级别旨在减少寻找第一个bug的时间。

接下来的两个级别更高级,并专注于到最后一个bug的时间。第四级开始使用正式的块级验证来代替模拟,其中DUT的大小通常是块或模块或小IP。第五级建立在第四级的基础上,旨在证明系统架构对于特定需求(如缓存一致性)是正确的,或者证明系统不会死锁。

这五个级别代表了当今行业的状态;事态发展可能要求今后增加更多的级别。


多媒体

十亿之门设计连接

多媒体

正式验收

多媒体

异构计算验证

多媒体

正式数据路径验证

多媒体

计划外验证

多媒体

ISO 26262统计数据

多媒体

技术讲座:功能安全的可追溯性

多媒体

技术讲座:FPGA RTL检查

多媒体

科技讲座:更好的覆盖

多媒体

技术讲座:正式的讨论

多媒体

技术讲座:正式实践

多媒体

技术讲座:正式验证

多媒体

技术讲座:调试IP

多媒体

技术讲座:SoC中的安全风险

多媒体

行政简报:正装


相关的实体

Baidu