得到一个统一的看看正式、模拟和加速度/仿真验证。
在过去的二十年,形式验证已从一个利基技术练习只有专家主流芯片发展的一个重要组成部分。一路上,几个进步需要更广泛的采用正式的可行的。其中包括断言的标准化语言,增强正式的发动机的性能和容量,更好的调试功能,按钮“应用程序”来解决具体问题。此外,正式的工具和他们的结果与从传统的模拟测试结果综合,这样团队成员和领导可以有一个统一的视图的验证进度。
这可能听起来很明显,但它并非如此多年。即使对芯片团队使用正式的工具,它是经常听到管理抱怨他们不知道如何衡量价值“角落里那群博士”增加了验证过程。对于那些考虑领养一个孩子,一个常见的问题是“如果我使用正式的,我不需要测试在模拟什么?“很难回答这些问题没有一个统一的看看正式、模拟、和加速度/仿真验证。
在OneSpin最近的渗透用户的小组会议在慕尼黑,我们的一个专家用户做一个优秀的演讲来解决这个需要。Antti Rautakoura目前SoC / ASIC验证专家在离开诺基亚在芬兰坦佩雷大学追求博士学位。他开始讨论今天的大型芯片的令人难以置信的复杂性,包括增加并行性来弥补这一事实单线程性能落后于摩尔定律。这使得更多的压力验证团队,他们的工作通常消耗大约三分之二的项目总工作。
Antti指出,有很多验证工具,它并不总是清楚项目将带来最大的好处。他说,关键在于从一个坚实的验证计划,然后选择正确的工具和正确的度量。高质量的度量提供具体的证据由特定工具或增值,另外,显示冗余。我们同意与他的声明“每个记录、传达和测量流是有价值的。“关键是一个验证计划,涵盖所有工具,紧随其后的是一组指标,可以准确测量的进展。
验证计划是简单的列出用例编写和运行仿真。Antti指出,不再是这样。验证计划应该基于设计特征,使用信息工具或方法将用于验证每个特性和指标确定验证完成后。例如,一个特性可能覆盖点列表必须达到模拟、正式的、或两者为了考虑功能验证。Antti指出,这种方法”是计划和结果为中心的由自然”和“可以洞察的真实完整性验证。”
虽然有一些特定于供应商的解决方案整合正式从模拟与计划和指标,这些工作只在封闭的工具流。管理强调支持第三方验证规划工具的重要性,并描述了他如何使用OneSpinPortableCoverage为了满足这种需求的解决方案。他雇佣了OneSpin验证计划集成应用形式分析结果导入任何领先的规划工具。他强调,用户必须理解之间的映射的结果模拟和正式,并检查有界(不完全)证明仔细看看还需要更多的验证。
Antti然后讨论覆盖在结合流的作用。他看到了OneSpin覆盖关闭加速器的高价值的应用,该标识的部分的设计不能达到任何模拟试验或形式分析。这种“死代码”应该被移除或记录,如果是由于重用或调试结构。他指出,死代码的决心可能会受到限制的设计,强调验证团队必须仔细检查约束,确保准确的结果。
如果不删除无用代码的设计,它必须被排除在覆盖率结果,使其缺乏可达性不人为地降低覆盖率指标。这也意味着验证团队不浪费时间和资源运行模拟,尝试访问点的设计。可及的部分设计,覆盖指标从正式的分析应综合与仿真。Antti使用OneSpin验证覆盖集成应用将从OneSpin量化指标应用的覆盖观众任何主要第三方模拟器。量化提供了基于模型的变异范围,该行业的最精确的度量来判断如何设计了断言。
Antti说,我们PortableCoverage流使设计和验证团队之间的共同责任,并赞扬我们的高效应用和支持第三方工具。他也给了一个很好的总结验证计划和管理的价值:
我们感谢Antti展示他的谈话和分享他的专长与我们的用户。他完整的视频演示,可用https://www.onespin.com/resources/videos/osmosis-2019/antti-rautakoura-nokia。我们希望你跟我们一样喜欢它。
|
|
|
|
|
|
|
|
|
|
留下一个回复