note
一、引言 3
背景介绍：
在硬件设计领域，确保设计的正确性至关重要，而形式属性验证（FPV）是保证硬件设计质量的关键方法。 然而，编写用于验证的断言（如 SVA）是一项具有挑战性的工作，传统的方法存在一些局限性，需要不断改进和创新。 就像我们盖房子需要确保房子质量，而传统的检查方式不够完善，需要寻找更好的检查手段，这就引出了新的研究和工具的需求。
==摘要==
形式属性验证（FPV）已经存在了数十年，并且已被证明能有效地发现复杂的寄存器传输级（RTL）错误。然而，诸如用 SystemVerilog 断言（SVA）编写的形式属性，即便对于有经验的用户来说，编写起来也既耗时又容易出错。先前的工作试图通过提高抽象层次来减轻这一负担，以便从高级规范生成 SVA。然而，这并不能消除对详细硬件行为进行推理和编写描述的人工工作。受异构硬件时代对 FPV 需求的增长以及大型语言模型（LLMs）进步的推动，我们开始探索 ==LLMs 是否能够捕捉 RTL 行为并生成正确的 SVA 属性==。首先，我们设计了一个基于 FPV 的==评估框架==，用于衡量 SVA 的正确性和完整性。然后，我们对 GPT4 进行迭代评估，以制定所需的一套==语法和语义规则==，促使其生成更好的 SVA。我们扩展了开源的 AutoSVA 框架，将我们改进后的基于 GPT4 的流程集成进去，以生成安全属性，并促进它们现有的活性属性流程。最后，我们的用例评估了==（1）==GPT4 生成的 SVA 在复杂开源 RTL 上的 FPV ==覆盖率==，以及==（2）==使用生成的 SVA 来促使 GPT4 从头开始==创建 RTL==。通过这些实验，我们发现 GPT4 即使对于有缺陷的 RTL 也能生成正确的 SVA——而不会复制设计错误。特别是，它生成的 SVA 揭示了 RISC-V CVA6 核心中的一个漏洞，而这个漏洞在先前工作的评估中被遗漏了。
二、研究背景
第一节==AutoSVA 的现状和局限==
AutoSVA 的基本功能
AutoSVA 是一个开源的框架，它可以从带有注释的 RTL（寄存器传输级）模块接口生成端到端的活性属性。 这就好比是一个小助手，能从硬件设计的一些基本信息中找出部分需要检查的内容，但是它只能做一部分工作。 例如，它可以根据接口的注释，生成一些检查硬件行为的规则，但它的能力有限，只能检查部分方面，而且对于复杂的硬件模块，它可能会有些力不从心，就像这个小助手只能做一些简单的任务，遇到复杂的大工程，就会感到困难，会遗漏很多重要信息。
原文
摩尔定律终结所引发的硬件多样性的寒武纪大爆发加剧了与寄存器传输级（RTL）设计验证（DV）相关的挑战[12]。在硬件复杂性和多样性不断增长的情况下，利用行业标准的 SystemVerilog 断言（SVA）[6]进行形式属性验证（FPV）对于提供详尽的 DV 正变得越来越重要。SVA 能够表达 RTL 信号之间的时间关系，这些关系可分为两大类：==安全属性和活性属性==。安全属性规定“不会发生不好的事情”，例如有限状态机（FSM）的转换；而活性属性规定“会发生某些好的事情”，例如一个请求最终应该得到响应。FPV 工具[3]、[15]使用基于形式化方法的求解器引擎来详尽地搜索反例（CEXs）。虽然 FPV 对于 DV 非常有效，但由于学习曲线陡峭以及编写断言需要额外的努力，工程师们往往不愿意使用它[13]。 先前的工作已尝试通过将部分流程自动化来简化 FPV 的使用：AutoSVA[11]从带注释的 RTL 模块接口生成端到端的活性属性；ILA[5]从功能规范生成设计的一个模型，并将其与 RTL 实现进行对比；以及 RTLCheck[8]通过从公理规范综合 SVA 来验证 CPU 流水线的 RTL 内存一致性。
第一节==GPT4 的引入与 AutoSVA2 的诞生==
GPT4 的强大能力
GPT4 是一个在自然语言处理方面非常出色的工具，它在生成代码和描述方面有独特的优势。 在硬件设计验证中，它可以用来生成 SVA（SystemVerilog Assertions），因为它能发现 RTL 中一些没有明确表述的行为，为我们提供更全面的检查视角。 想象一下，GPT4 就像一个聪明的侦探，能够找到一些隐藏在硬件设计中的“蛛丝马迹”，这些是原来的小助手 AutoSVA 所发现不了的。
AutoSVA2 的框架构成：
基于 GPT4 的 SVA 生成流程（生成安全属性）：
为了让 GPT4 更好地发挥作用，研究人员设计了一系列规则，引导 GPT4 生成安全属性的 SVA。 这些规则会告诉 GPT4 如何根据 RTL 的信号命名、使用方式以及常见的设计模式，生成相应的安全属性。 例如，对于一个硬件模块中的计数器，GPT4 可以根据这些规则，生成检查计数器是否会超出范围的断言，防止出现数据溢出等安全问题，就像给计数器设定一个安全警戒线，一旦超过，就会发出警报。
新的接口注释生成流程（辅助生成活性属性）：
开发了一个新的流程，利用 GPT4 生成模块事务注释，描述模块之间的交互和事务流程。 这些注释可以帮助 AutoSVA 更好地理解硬件模块之间的工作关系，进而生成更准确的活性属性。 例如，对于一个总线接口模块，GPT4 可以详细描述数据在总线上是如何传输的，先传什么，后传什么，读写操作何时发生，以及不同信号之间的时序关系等。 AutoSVA 根据这些注释就能生成更准确的活性属性，确保数据传输的正确性和时序的合理性。
原文
虽然这些都是有效的工具，但它们要么只能验证 RTL 设计的子集，要么需要付出大量努力来编写结构化的规范。随着大型语言模型（LLMs）近期的进步，==一个问题==随之产生：LLMs 能否帮助加速 RTL 设计和验证呢？如果可以，我们应当如何将它们集成到现代 RTL 开发中呢？在过去几个月里，研究人员已经探索了使用 LLMs 从自然语言生成时序逻辑规范和断言[4]、[7]，以及填补不完整 RTL 中的漏洞[14]。我们采取一种更全面的方法，==探索 LLMs 是否能为给定的设计生成正确的 SVA，而无需超出 RTL 之外的任何规范——即使 RTL 中包含错误。==我们这样做的动机是，规范并非总是可用或足够精确。通常，在写出 RTL 之前，实现细节不会被充实完善。在学术和开源硬件领域尤其如此，那里的 RTL 处于持续开发中[10]。此外，仅从 RTL 生成 SVA 将使得对由 LLMs 生成的 RTL 进行形式验证成为可能[14]。
我们的方法：
从一个针对 RTL 模块的==空的形式属性验证测试平台==（FT）开始，我们的目标是生成能够对设计的正确性进行推理的 SVA，而无需手动提供有关功能或要生成的属性的细节。我们将 GPT4 [9] 用于这项整体任务，因为早期使用较小的大型语言模型（LLMs）进行的实验并不理想。==然而==，即使是最先进的 GPT4 在默认情况下也会生成语法和语义上错误的 SVA。因此，我们首先必须通过用规则迭代细化提示来教 GPT4 如何生成正确的 SVA（图 1）。然后，我们在 AutoSVA [11] 的基础上进行构建，除了促进现有的活性流程外，还纳入我们改进的基于 GPT4 的安全属性流程（图 2）。我们将我们扩展后的框架（目前是匿名的）作为 AutoSVA2 [2] 提供使用。我们的用例评估了： (1) AutoSVA2 在复杂 RTL 上的形式属性验证（FPV）覆盖率，以及 (2) 使用生成的 SVA 来促使 GPT4 从头开始创建 RTL，对于此任务，AutoSVA2 可以输出更多的 SVA（图 3）。
==我们的技术贡献如下：==
一种基于 FPV 的迭代方法，用于找出教给一个 LLM 如何从给定的 RTL 模块生成语法和语义上正确的 SVA 所需的规则。
评估 GPT4 并制定改进其 SVA 输出的规则，以及将这个改进的基于 GPT4 的 SVA 生成流程扩展到 AutoSVA 框架中。
描述 AutoSVA2 的稳健性和覆盖率。
一种由 AutoSVA2 驱动的 RTL 生成和验证方法；通过使用人工细化的生成的 SVA 作为提示，迭代地改进 LLM 生成的 RTL（图 3）。
==我们的实验发现==：
GPT4 的创造性使其能够从有错误的 RTL 中生成正确的 SVA，也就是说，它并非仅仅被迫基于我们提供的 RTL 来生成 SVA。
为了生成 SVA，GPT4 对 RTL 模块和变量的名称并不十分敏感。
对于相同的 RTL 模块，AutoSVA2 生成的属性对 RTL 行为的覆盖率比 AutoSVA 生成的属性提高了多达 6 倍[1]。
在一个小时的工程努力内，我们的 AutoSVA2 评估发现了 RISC-V CVA6 Ariane 核心[10] 中的一个漏洞，该漏洞在 AutoSVA 之前的评估[11]中被遗漏了。
当我们在提示中包含 SVA 时，GPT4 会生成更好的 RTL；其创造性使其即使在 SVA 不完全正确的情况下也能生成正确的 RTL。
本文的其余部分组织如下
第二节展示了我们用于找出 LLM 生成的 SVA 中的缺陷和测试规则以引导其生成更好的 SVA 的迭代方法。
我们早期对 GPT4 的实验向我们表明，它能够仅从 RTL 生成若干 SVA 属性，但这些属性包含语法和语义错误。然而，我们发现可以通过给 GPT4 提供要遵循的规则来引导它生成更好的 SVA。第 II - A 节描述了我们用来==迭代构建 GPT4 生成有用断言所需的提示规则集的方法==。第 II - B 节描述了我们==遇到的问题以及为克服这些问题而添加到提示中的规则==。
规则细化方法学
图 1 描绘了我们用于迭代细化要包含在大型语言模型（LLM）提示中的规则集的评估框架。尽管我们使用该框架进行的所有实验都是在 GPT4 上完成的（表 I），但我们认为它可用于评估任何 LLM 的输出质量。 这种方法学要求有一个形式属性验证测试平台（FT）。我们可以通过执行指示目标 RTL 模块的 AutoSVA [1] 脚本来快速创建一个。（生成的 FT 具有属性和工具绑定文件，但没有断言。）理论上，可以将任何 RTL 模块用作 LLM 的输入，但请注意，工程师应该能够轻松确定 SVA 的问题。理想情况下，所使用的 RTL 模块应该是完全正确的，这样形式属性验证（FPV）引擎生成的反例（CEX）是由错误的断言导致的。请记住，这种方法学的目标不是为这个 RTL 模块提供一个完整的 FT，而是细化规则，以便 LLM 生成更好的 SVA。对于我们在 GPT4 上进行的实验（在第 II - B 节中有详细说明），我们使用了 AutoSVA 存储库 [1] 中的 FIFO 模块。
第三节介绍 AutoSVA2，这是我们扩展的框架，它在 AutoSVA 的基础上集成了一个基于 GPT4 的流程，以便用更少的努力创建更完整的 FT。
四、实验部分：
在复杂 RTL 上测试 AutoSVA2
实验对象和目的： 选取了 64 位 RISC - V CVA6 Ariane 核心里的页表遍历器（PTW）和转换后备缓冲器（TLB）模块进行测试。 这些模块比较复杂，之前也被研究过，方便对比结果。 实验的目的不是要把这些模块的 RTL 完全验证正确，而是测试基于 GPT4 的 SVA 生成流程在复杂模块上的效果，并比较新生成的属性和 AutoSVA 原来的属性，看覆盖率有没有提升。 就像挑选了两个比较难的任务，来检验新方法是否比老方法更有效。
构建 PTW FT 并发现 RTL 漏洞： CVA6 在开源硬件社区很常用，而且在不断更新。 研究人员发现之前 PTW 模块有个漏洞，想看看 AutoSVA2 能不能找到这个漏洞。 他们使用 AutoSVA2 生成断言，开始时生成了几批断言，随着生成断言的增多，通过审核和验证，最终发现了能揭示该漏洞的正确断言。 这个过程就像不断挖掘线索，最终找到了隐藏的问题。
断言生成策略： 采用了一些专门的断言生成策略，让 GPT4 根据有限状态机（FSM）的状态转换等情况生成断言。 这些策略可以帮助 GPT4 更有针对性地生成有用的断言，就像给 GPT4 一些特殊的搜索方向，让它更快更准地找到硬件设计中可能存在的问题。
自动生成 SVA 的 RTL 覆盖率： 对不同的断言集进行评估，包括 AutoSVA 原有的断言和 GPT4 不同批次生成的断言。 通过语句覆盖和翻转覆盖这两个指标，发现使用 GPT4 生成多批次断言能显著提高对 RTL 的覆盖程度。 例如在 PTW 和 TLB 模块上，GPT4 生成的断言与 AutoSVA 原有的断言一起使用时，覆盖率会大大提高，说明它们可以相互补充，就像多个不同角度的检查能让我们更全面地了解硬件设计是否有问题。
五、用例 2：AutoSVA2 引导 RTL 生成
- 迭代过程： 从一个初始的 RTL 设计开始，使用 AutoSVA2 生成 SVA 断言，然后利用 FPV 工具进行验证。 根据验证结果对 RTL 进行优化修改，形成一个迭代的过程。 以 FIFO 模块为例，开始时设计可能不完善，经过多次迭代，每次根据 AutoSVA2 的验证结果修改 RTL，最终得到优化的 FIFO 模块。 就像我们不断调整建筑图纸，根据检查结果，一步步完善房子的设计，让它更加完美。
六、讨论与结论
- 讨论部分： - AutoSVA2 的优势： 生成的 SVA 更全面，能更好地覆盖复杂的硬件设计，发现更多潜在问题，而且可以引导 RTL 的优化，提高设计质量。 但 GPT4 在生成 SVA 时具有创造性，也会带来风险，需要工程师仔细审核，不能完全依赖。 -
- 完整性和正确性的关系： 即使 SVA 覆盖了完整的 RTL，也不意味着断言或 RTL 本身是正确的，需要对所有断言进行审核，确保它们符合硬件设计的正确规范，不能只看是否产生反例，因为可能存在断言和 RTL 都出错的情况。
- 结论部分： AutoSVA2 是一个有效的硬件设计验证工具，结合了 AutoSVA 和 GPT4 的优势，为硬件设计的形式属性验证提供了新的解决方案。 不过，还有很多需要改进的地方，比如优化 GPT4 的生成规则，完善 AutoSVA2 的流程，以应对更复杂的硬件设计，未来还有很大的发展空间，能帮助我们更好地进行硬件设计和验证，确保硬件产品的质量和可靠性。 这样分行后，文档的结构更加清晰，每个部分的不同信息都被拆分成了更细的行，更便于阅读和理解。你觉得这个版本怎么样呢 ？如果你还有其他要求，可以随时告诉我哦 。
