形式化验证，Complete Formal Verification of TriCore2 and Other Processors（五）

news2024/11/24 10:30:48

一、Article:文献出处（方便再次搜索）

（1）作者

（2）文献题目

（3）文献时间

（4）引用

二、Data:文献数据（总结归纳，方便理解）

（1）背景介绍

（2）目的

（3）结论

（4）主要实现手段

三、Comments对文献的想法（强迫自己思考，结合自己的学科）

四、Why:为什么看这篇文献（方便再次搜索）

五、Summary:文献方向归纳（方便分类管理）

一、Article:文献出处（方便再次搜索）

（1）作者

Jörg Bormann, Sven Beyer, Adriana Maggiore, Michael Siegel, Sebastian Skalberg（德国 OneSpin Solutions GmbH）
Tim Blackmore, Fabio Bruno（Infineon Technologies ，德国英飞凌技术公司）

（2）文献题目

Complete Formal Verification of TriCore2 and Other Processors

（3）文献时间

非CFF收录，2007，收录于DVCon，是在中国举办的集成电路相关的高技术会议，探讨集成电路和电子系统设计与验证中的标准语言、工具与方法学。

（4）引用

Bormann, Jörg, Sven Beyer, Adriana Maggiore, Michael Siegel, Sebastian Skalberg, Tim Blackmore and Fabio Bruno. “Complete Formal Verification of TriCore2 and Other Processors.” (2007).

二、Data:文献数据（总结归纳，方便理解）

（1）背景介绍

传统的验证方法通常无法识别设计中的所有功能错误：（简单理解为是列举验证）
- 在仿真验证中，由于无法在项目时间内部署大量的激励来充分验证IP，因此仿真无法激发所有可能的错误。
- 此外，仿真验证通常只能验证所选的测试用例，而无法穷尽地验证所有可能的输入组合和场景。
形式化验证可以通过对所有可能的输入场景进行详尽的证明来验证属性集中的所有属性。但是大多数断言和属性只能在enforce realistic behavior of the DUV（限制DUV的行为，确保其具有可行的行为）的特定条件下被证明，且这些约束条件非常依赖验证工程师的个人经验，但是工程师不一定都能考虑到corner-case。换言之，形式化验证方法无法产生无间隙的属性集，以确保设计无错误。

（2）目的

如何自动生成一个完备的属性集（即如何消除属性集中的空缺）或者如何检验写出的属性集是否完备?

（3）结论

采用自动完备性分析：
- 完备性分析：检查给定的属性集是否严格到足以在任何时间点上为模块的每个输出确定唯一的值。
- 自动完备性分析：能自动识别并突出显示尚未由任何属性验证的输入场景和相应的输出行为，来消除属性集中的空缺（识别出后会提供close gap的机会），以确保所有对设计的输入/输出行为做出贡献的功能都至少被一个属性检查过。
文中描述了两个应用该方法的例子，分别是对单流水线协议处理器和超标量 Tricore2 处理器的完整验证，得出的结论是：本文的形式化验证方法可以提供更加完整的错误检查，即基于动态的仿真不能检查出来的错误，本文的方法也可以。

（4）主要实现手段

三、Comments对文献的想法（强迫自己思考，结合自己的学科）

1.摘要中提到本文的方法是一种独立于仿真的硬件验证方法“the methodology is a self-contained approach to hardware verification, independent of simulation.” 但是文中并没有提到任何关于硬件验证的方法？关于“独立于仿真”是说属性的设计是基于指令集的，根据指令集进行分类，并对每一类指令集进行属性的编写，再对整个属性集进行完备性分析。

2.针对剔除的自动完备性分析方法，本文实验数据比较薄弱，只在文中进行了简单的叙述，只说明相对于动态仿真检查出了多少个错误，一共有多少个错误，但是更细粒度的实验指标没有，比如：验证过程中的时间开销。

3.如此看来，本文的目标旨在检验属性集是否完备，而非自动生成一个完备的属性集，那这样的话你还是得依靠经验、花费精力进行大量的属性编写？