AssertionBench

Name: AssertionBench
Creator: 伊利诺伊大学芝加哥分校
Published: 2024-06-26T22:47:28+08:00

arXiv2024-06-26 更新2024-06-29 收录

硬件设计

断言生成

数据链接：

https://github.com/achieve-lab/assertion_data_for_LLM 数据链接链接失效反馈

官方服务：

资源简介：

AssertionBench数据集由伊利诺伊大学芝加哥分校的研究团队创建，包含100个精心挑选的Verilog硬件设计，每个设计都附有通过GOLDMINE和HARM生成的正式验证的断言。数据集大小适中，涵盖了多种硬件设计类型，如UART协议的接收器和发送器、编码器、解码器及浮点运算单元中的算术操作等。创建过程中，研究团队利用了深度学习模型和大型语言模型进行断言生成，并通过正式验证确保断言的准确性。该数据集主要应用于硬件设计的验证领域，旨在通过量化评估大型语言模型在断言生成任务中的表现，推动硬件设计验证技术的发展。

The AssertionBench dataset was created by a research team from the University of Illinois at Chicago, containing 100 meticulously selected Verilog hardware designs, each accompanied by formal assertions generated through the GOLDMINE and HARM tools. The dataset is of moderate size and covers a variety of hardware design types, such as UART protocol receivers and transmitters, encoders, decoders, and arithmetic operations within floating-point units. During its creation, the research team utilized deep learning models and large language models for assertion generation, ensuring the accuracy of the assertions through formal verification. This dataset is primarily applied in the field of hardware design verification, aiming to quantify the performance of large language models in the assertion generation task, and to promote the development of hardware design verification technology.

提供机构：

伊利诺伊大学芝加哥分校

创建时间：

2024-06-26

原始信息汇总

AssertionBench 数据集概述

数据集描述

目的：评估大型语言模型（LLM）在硬件设计断言生成中的有效性和适用性。
内容：包含100个来自OpenCores的Verilog硬件设计，每个设计均配有由GOLD MINE和HARM生成的正式验证断言。
应用：用于比较GPT-3.5、GPT-4o、CodeLLaMa 2和LLaMa3-70B等LLM在生成功能正确断言方面的表现。

数据集组成

硬件设计：100个Verilog设计文件。
断言来源：GOLD MINE和HARM工具生成的正式验证断言。
模型响应：包含GPT-3.5、GPT-4、LLaMA3-70B和CodeLLaMa2-70B的1-shot和5-shot学习响应，以JSON格式保存。

软件工具

IVerilog：用于编译和运行Verilog HDL设计的编译器。
GOLD MINE：用于从Verilog HDL设计中挖掘断言的工具。
HARM：基于提示的断言挖掘工具，用于从.vcd文件中生成断言。
JasperGold：用于正式功能验证的软件，验证生成的断言。

评估框架

评估方法：使用1-shot和5-shot学习比较不同LLM的表现。
参数设置：max_new_tokens = 1024; temperature = 1.0; seed = 50;。
错误修正：使用GPT-3.5修正语法错误。

相关出版物

标题：AssertionBench: A Benchmark to Evaluate Large-Language Models for Assertion Generation
作者：Vaishnavi Pulavarthi, Deeksha Nandal, Soham Dan, Debjit Pal
状态：已被NAACL 2025接受。
链接：https://arxiv.org/pdf/2406.18627

搜集汇总

数据集介绍

构建方式

AssertionBench数据集的构建方式是将100个经过精选的Verilog硬件设计从OpenCores网站收集，并为每个设计生成形式上经过验证的断言，这些断言由GOLDMINE和HARM生成。这些设计涵盖了广泛的硬件类型，包括UART协议的接收器和发射器、编码器、解码器以及FPU中的加法、乘法和二进制补码运算。数据集还包含五个用于1-shot和5-shot学习的训练示例，每个示例都是一个包含Verilog设计和其形式上经过验证的断言的元组。

特点

AssertionBench数据集的特点是它提供了一个全面的基准，用于量化当前和未来的大型语言模型（LLMs）在断言生成任务上的有效性。数据集包含各种复杂性的设计，使其成为评估LLMs在生成硬件设计断言方面的能力的理想选择。此外， AssertionBench 还提供了形式上经过验证的断言，这有助于研究人员探索LLMs在断言生成方面的适用性。

使用方法

使用AssertionBench数据集的方法涉及对LLMs进行训练和评估，以生成硬件设计的断言。研究人员可以使用数据集中的训练和测试设计来训练LLMs，并使用形式验证引擎（如Cadence JasperGold）来评估生成的断言的有效性。数据集还可以用于评估不同LLMs之间的性能差异，并研究LLMs在生成断言方面的局限性。

背景与挑战

背景概述

AssertionBench数据集的创建旨在解决硬件设计中断言生成的挑战。断言在硬件设计的仿真和形式验证中扮演着关键角色，其质量直接影响硬件验证的准确性。尽管过去的研究结合了数据驱动统计分析和静态分析，以从硬件设计源代码和设计执行跟踪数据中生成高质量的断言，但它们在扩展到工业规模的大型设计、产生大量低质量断言、无法捕捉微妙和非平凡的设计功能，以及不提供易于理解的断言解释等方面存在困难。随着大型语言模型（LLMs）的出现，研究人员开始探索将断言生成建模为序列到序列的翻译（S2St）并利用提示工程技术生成断言。然而，关于不同LLMs在断言生成方面的有效性和适用性，尚缺乏定量的评估。AssertionBench数据集包含了从OpenCores收集的100个精心挑选的Verilog硬件设计，并为每个设计提供了使用GOLDMINE和HARM生成的形式化验证断言。该数据集为评估LLMs在生成硬件设计功能正确断言方面的有效性提供了一个平台，并展示了LLMs在生成断言方面的性能差异和改进空间。

当前挑战

AssertionBench数据集面临的主要挑战包括：1)如何有效地利用LLMs生成功能正确的断言，特别是在没有大量手工提示的情况下；2)LLMs在处理复杂的硬件设计时，如何捕捉设计的语义含义；3)LLMs在生成断言时，如何避免生成语法错误；4)如何提高LLMs生成断言的准确性，尤其是在多时钟周期设计行为方面。此外，当前数据集仅关注Verilog设计，未来研究需要扩展到其他硬件设计语言，并考虑使用辅助工件（如控制数据流图、变量依赖图等）来提高LLMs的性能。

常用场景

经典使用场景

AssertionBench 数据集主要用于评估大型语言模型（LLMs）在生成硬件设计断言方面的有效性。该数据集包含了 100 个精心挑选的 Verilog 硬件设计，每个设计都配备了从 GOLDMINE 和 HARM 生成的形式化验证断言。通过 AssertionBench，研究者可以比较不同 LLMs（如 GPT-3.5、GPT-4o、CodeLLaMa 2 和 LLaMa3-70B）在推断硬件设计功能性正确断言方面的能力。该数据集允许研究者探索使用更多上下文例子的优势，以及为生成更高比例的功能性正确断言而改进 LLMs 的空间。

衍生相关工作

AssertionBench 衍生了一系列相关工作，包括但不限于：1. 对现有 LLMs 在断言生成任务上的性能进行评估和比较；2. 开发新的断言生成工具和方法，利用 LLMs 的能力来提高断言生成的质量和效率；3. 研究如何利用 LLMs 的上下文学习能力来生成更准确的断言；4. 探索如何将 LLMs 应用于其他硬件设计验证任务，如功能覆盖分析和故障诊断。这些相关工作将进一步推动 LLMs 在硬件设计验证领域的应用和发展。

数据集最近研究