用于早期检测实现问题的自动化正式代码检查。
集成电路设计人员承受着持续不断的压力，他们必须交付无bug的代码，以满足越来越严格的要求。众所周知，在开发过程的早期发现的错误越多，开发工作就会越快、越容易。然而，早期的错误检测需要设计人员承担繁重的验证开销，并影响设计过程。
设计人员可以利用的两种主要方法是静态检测和模拟。Linting需要较低的设置，并且可以基于代码的语法检测一类错误，尽管它倾向于报告许多必须分析的潜在问题，并且在检查块的顺序操作时受到限制。模拟的重点是代码操作，但需要更大程度的设置，以定向刺激创建的形式，这通常在过程的这个阶段是不可用的，并且只会检测所提供的刺激正在检查的场景中的问题。
为了早期自动检测实现问题，设计人员需要的是以一种彻底的方式为代码的顺序操作设置静态检查的快速简单的方法，而不依赖于用户提供的刺激。自动化的正式代码检查有助于在功能验证和综合之前快速消除RTL中的错误，同时提供完全自动化的简单使用模型。实现了三种不同的验证视角。
这些技术都是全自动的，不需要用户创建断言。不需要编写刺激、创建断言或理解所使用的正式机制。
让我们来看看一家大型无线通信公司如何在他们的PP32网络处理器上应用这种技术以及先进的覆盖关闭解决方案。该应用程序需要一个5层指令管道、中断处理和cpu上的任务机制。
为了充分理解自动化正式技术的影响，我们需要了解这个设计团队所面临的挑战。这组工程师正在处理非常复杂的IP验证。因此，多次回归运行的模拟花费的时间太长。验证覆盖的范围是未知的，因此无法实现完整的功能覆盖，在soc中没有发现集成错误。
对每个指令操作码使用大致一个断言，该公司就能够验证其网络处理器的功能正确性。在将形式化验证技术应用于设计时，采取了以下步骤:
实施后取得的具体成果包括:
正如您所看到的，这项技术的结果不言自明，但如果公司没有采用这种特定的正式解决方案，那么就必须进行大量的测试台编写以及无数个模拟周期。对大量情况的核查将花费大量时间，但仍不能完全核查。所有这些都将导致对零漏洞逃脱的信心不足，并且，最终，IP将更加难以重用。
如果您有兴趣了解更多关于OneSpin Inspect技术和了解其他人如何使用它，请查看我们的成功的故事．
|
|
|
|
|
|
|
|
留下回复