世界各地采用不同的正式核查方式。
正式验证正在全球范围内的工程团队为无错误和可靠的数字芯片进行复杂的功能验证。事实上，考虑到形式化验证在针对广泛的验证挑战方面的灵活性，许多困难的验证挑战都可以通过形式化验证解决。正式核查在易于使用和能力方面的最新进展使其成为一种更加不可或缺的工具。
奇怪的是，各大洲实施正式核查的方式似乎各不相同。全球趋势和用于正式验证的模型几乎可以被认为是一个大陆分水岭。在一个有趣的二分法中，正式可能也会减少这种二分法的影响。
SystemC在亚洲的大型半导体和电子系统公司很流行，现在才开始在其他地方的工程界流行起来。高级综合将算法和通常用SystemC和c++编写的潜在的不定时设计模型转换为完全定时的RTL设计块。在日本，这种机制已被用作一种生成具有不同微架构的设计组件的方法，同时快速有效地优化算法处理数据路径，提供灵活性和更快的上市时间。SystemC语言基于c++，而c++不是为硬件描述而设计的，因此可能会给更熟悉hdl的工程师带来问题。日本的工程团队现在使用基于SystemC的正式验证来检测和消除SystemC代码中的这些语言问题(例如x状态问题和竞争条件)，然后再进行高级合成。这种正式验证的使用正在传播到世界各地的其他公司，缓解了他们使用SystemC的问题。
在几大洲之外的欧洲，安全关键设计很重要，因为那里有大型汽车工业。它在美国开始变得重要起来，但势头还不够强劲。形式化验证在系统和随机故障验证方面有多种应用，以满足ISO 26262标准的要求。它解决了安全关键硬件高效开发中的具体挑战，显著改变了验证过程的质量和效率，并简化了满足ISO 26262标准所需的活动。欧洲为安全关键应用进行设计的工程团队将其视为一种强大的技术，可以发现硬件设计漏洞，否则这些漏洞可能会逃避基于模拟的验证，并导致系统故障。形式化的验证还提高了工程团队计算诊断性故障覆盖的能力，这再次改进了流程，并使其更容易普遍应用。
总部位于美国的工程团队的关注点与其他大陆的工程师同事略有不同，他们经常面临需要快速解决的更紧迫的项目问题的挑战。正式核查在解决用其他方法难以处理的具体和困难核查问题方面已被证明是非常宝贵的。无论是自动化应用程序还是基于断言的验证，形式化可以在模拟之上提供一层功能，从而减少验证计划。正式验证已经在验证过程的末尾的错误查找周期中使用了几年，并且它的应用正在周期的开始阶段向前移动，在那里它取代了一些更困难的块的模拟。将覆盖度量结合起来，并将正式的方法集成到验证计划过程中，可以带来更高的效率。
形式化验证为所有这些应用程序提供解决方案的能力演示了如何在不同的环境中使用该技术。展望未来，半导体行业需要思考的是，这种不同大洲的分歧是未来的浪潮，还是应用的趋同。或者是否正式的工具可以统一这些不同的方法，并允许所有的工程团队从彼此的经验中受益。
|
|
|
|
|
|
|
|
留下回复