电子产品世界

多年来，设计重用方法为半导体 IP （SIP） 创造了一个市场，现在有了正式的技术，就需要断言 IP （AIP）。其中，每个AIP都是硬件设计中用于检测被测设计（DUT）中的协议和功能违规的可重用和可配置验证组件。LUBIS EDA 专注于正式服务和工具，因此我收到了有关他们开发这些 AIP 和检测高风险 IP 中极端情况错误的方法的最新信息。

在详细介绍 LUBIS EDA 使用的方法之前，让我们先回顾一下基于仿真的验证与形式验证有何不同。通过仿真，工程师正在编写激励来覆盖设计的所有已知状态，希望覆盖范围足够高。通过形式化验证，形式化工具可以找出设计中从输入到输出的所有可能路径。

基于仿真的验证基于形式的验证

LUBIS EDA 使用的一种方法是其内部属性生成器，它在电子系统级 （ESL） 而不是寄存器传输级 （RTL） 上工作。这使他们能够提供更快、更高质量和更高效的验证服务。属性生成器使您能够在几分钟内从抽象模型转换为 AIP，这是验证效率的巨大飞跃。该流程如下所示：首先，抽象模型由属性生成器解析和分析，然后将形式验证 IP 创建为系统验证断言 （SVA）。这些断言检查您的设计意图并提供功能行为的完整覆盖。

属性生成器流

ESL 级别的抽象模型是用 C++ 或 SystemC 编写的，可以模拟以验证其行为，属性生成器会读取该代码并为你生成 AIP。然后，通过大型语言模型 （LLM） 支持的细化步骤将断言绑定到您的 RTL 设计，以更快地获得结果。断言是人类可读的，并且是按构造更正的，因此您不需要有专门的断言评审会话。在此流中运行您最喜欢的正式工具，然后查找任何失败。

应用这种 AIP 方法的一个示例是加密哈希函数，例如 SHA-512。下面显示了左侧的 C++ 模型和右侧生成的涵盖模型部分的属性。

总结

这种方法如何使形式验证更加高效？验证工程师可以通过手动编写断言来应用形式化方法。手动编写形式断言需要时间、容易出错并且需要专业知识，因此自动执行此步骤可以节省您的工程时间和精力。

生成的断言 IP （AIP） 涵盖了所有可能的场景和刺激，以保证设计无错误。这种方法对于帮助您验证逻辑块甚至复杂的 IP 核也非常有用。

您的项目是否面临巨大的时间压力，您想利用这种高效方法的优势吗？那么您应该考虑 LUBIS EDA 的咨询服务，以实现一流的 SoC 设计质量。如果您想自己执行项目，还有一些形式验证课程可以帮助您更快地工作。LUBIS EDA 的网站也有许多关于使用形式验证技术的有用博客文章。

关键词： 设计验证 断言 IP AIP