VERT

VERT是一个开源的数据集，由德克萨斯大学达拉斯分校和英特尔公司的研究人员共同创建，旨在提高大型语言模型对SystemVerilog断言生成的能力。该数据集通过系统性地增强开源硬件描述语言仓库中的变量，生成合成的代码片段及其对应的断言，支持学术界和工业界研究人员对开源模型进行微调，以超越大型专有模型在准确性和效率方面的表现，同时确保数据隐私和降低成本。

VERT is an open-source dataset co-created by researchers from The University of Texas at Dallas and Intel Corporation, aiming to enhance the capability of Large Language Models (LLMs) in generating SystemVerilog assertions. This dataset systematically augments variables within open-source hardware description language repositories to generate synthetic code snippets and their corresponding assertions, supporting researchers from both academia and industry to fine-tune open-source models so as to outperform large proprietary models in terms of accuracy and efficiency, while ensuring data privacy and reducing costs.

搜集汇总

数据集介绍

构建方式

VERT数据集通过系统地增强开源硬件描述语言（HDL）存储库中的变量来构建，以生成合成代码片段及其对应的断言。这些代码片段涵盖了硬件验证中常见的条件结构，包括if-else语句、case语句和组合结构，并确保了同步和异步断言的均衡分布。数据集的构建旨在解决现有大型语言模型（LLMs）在生成硬件验证断言时遇到的挑战，如时钟周期误解、条件映射错误、嵌套if-else语句处理和长条件处理。

特点

VERT数据集的特点在于其针对性，专门设计用于提高LLMs在硬件验证断言生成方面的性能。数据集包含20,000个样本，涵盖了硬件设计中常见的各种条件结构，并经过精心设计以解决LLMs在断言生成中的常见错误。此外，VERT数据集通过使用重叠蕴涵符号和延迟计数来标准化格式，以帮助LLMs准确捕获时钟周期信息。数据集的合成性质确保了模型的多样性和鲁棒性，避免了过拟合特定命名约定或设计特征。

使用方法

使用VERT数据集进行LLMs的微调涉及使用开源模型，如DeepSeek Coder和Llama，并在其上进行训练，以提高它们在生成硬件验证断言方面的准确性。微调过程包括使用低秩适配器（LoRA）技术，该技术允许对模型进行高效更新，同时保持计算成本最低。在微调后，LLMs的性能在生成语法正确和功能正确的断言方面得到了显著提高，超过了GPT-4o等大型专有模型。为了评估性能，使用了突变测试、形式验证和基于模拟的分析，以确保断言的完整性和可靠性。

背景与挑战

背景概述

在当今的SoC设计中，硬件验证是至关重要的，它占据了约70%的开发时间。SystemVerilog断言确保了正确的功能。然而，现有的工业实践依赖于手动断言生成，这随着硬件系统变得复杂而变得越来越不可行。最近的研究表明，大型语言模型（LLMs）可以自动化这个过程。然而，像GPT-4o这样的专有SOTA模型往往会生成不准确的断言，并且需要昂贵的许可证，而较小的开源LLMs需要微调以管理HDL代码的复杂性。为了解决这些问题，我们引入了VERT，一个开源数据集，旨在使用LLMs增强SystemVerilog断言生成。VERT使学术和工业界的研究人员能够微调开源模型，在准确性和效率方面优于更大的专有模型，同时通过本地微调和消除昂贵的许可证来确保数据隐私。数据集是通过系统地从开源HDL存储库中增强变量来创建的，以生成合成代码片段及其相应的断言。实验结果表明，微调后的模型如Deepseek Coder 6.7B和Llama 3.1 8B在包括OpenTitan、CVA6、OpenPiton和Pulpissimo在内的平台上优于GPT-4o，比基线模型提高了96.88%，比GPT-4o提高了24.14%。VERT可在https://github.com/AnandMenon12/VERT上获得。

当前挑战

VERT数据集面临的挑战包括：1)所解决的领域问题，即硬件验证中SystemVerilog断言的自动生成；2)构建过程中所遇到的挑战，例如确保断言的语法和功能正确性，以及处理复杂的设计模式和硬件架构。

常用场景

经典使用场景

VERT 数据集的创建旨在解决硬件验证中系统级芯片（SoC）设计中日益复杂的挑战。该数据集通过提供大量经过精心策划的 SystemVerilog 断言和相应的 RTL 代码片段，为研究人员和行业专家提供了一个宝贵的资源，用于微调开源大型语言模型（LLMs），以生成准确无误的断言。VERT 数据集的常见使用场景包括自动化断言生成，从而减少开发时间并降低错误风险，特别是在复杂硬件系统设计方面。此外，VERT 还支持对开源 LLMs 进行本地微调，以确保数据隐私，并消除对昂贵许可的依赖。

解决学术问题

VERT 数据集解决了现有 LLMs 在生成硬件验证断言方面存在的关键问题。这些模型通常无法准确捕捉时钟周期延迟、正确映射 'if' 条件到 'else' 分支，以及处理复杂的逻辑表达式。VERT 通过提供大量经过精心策划的数据，使开源 LLMs 能够克服这些局限性，从而提高断言生成的准确性和可靠性。此外，VERT 还支持对开源模型进行本地微调，从而确保敏感设计数据的安全性，并提供了一种无需昂贵许可即可提高性能和可访问性的解决方案。

衍生相关工作

VERT 数据集的推出引发了一系列相关研究，旨在进一步推动硬件验证领域的发展。研究人员已经开始探索如何利用 VERT 数据集来微调更大的 LLMs，以进一步提高断言生成的准确性和可靠性。此外，VERT 数据集还推动了新的研究框架和方法的发展，旨在解决 LLMs 在硬件验证中存在的其他挑战。这些研究工作包括开发新的数据清理和标准化方法、探索更先进的微调技术以及开发新的评估指标，以确保生成的断言的准确性和可靠性。VERT 数据集的推出为硬件验证领域带来了新的机遇和挑战，为未来的研究工作提供了坚实的基础。