HLS-LeVeri benchmark

该数据集是用于移位左高等级合成验证的初始基准预览，包含从hlstrans中过滤和增强的107个独立验证目标，每个条目总结了配对C/HLS-C基准信息，以支持移位左HLS验证研究。数据集进一步构建了一个更大的已验证4元组数据集（P_c, P_h, TB_c, TB_h），其中P_c是黄金C/C++程序，P_h是面向HLS的实现，TB_c是黄金C测试台，TB_h是HLS-C测试台，提供了完整的C/HLS-C/C-Testbench/HLS-C-Testbench结构，与其他仅提供部分验证工件的资源不同。This dataset is an initial benchmark preview for shift-left high-level synthesis (HLS) verification, containing 107 independent verification targets filtered and augmented from hlstrans. Each entry summarizes paired C/HLS-C benchmark information to support shift-left HLS verification research. The dataset further constructs a larger validated 4-tuple dataset (P_c, P_h, TB_c, TB_h), where P_c is the golden C/C++ program, P_h is the HLS-oriented implementation, TB_c is the golden C testbench, and TB_h is the HLS-C testbench, providing a complete C/HLS-C/C-Testbench/HLS-C-Testbench framework, which differs from other resources that only offer partial verification artifacts.

原始信息汇总

数据集概述

HLS-LeVeri 是一个面向高级综合（HLS）验证的开源数据集，旨在支持“左移验证”这一阶段，即在综合之前自动验证黄金C规范和面向HLS的C实现之间的功能一致性。

核心方法

该框架融合了三种技术：

• 双层次一致性检查：对输入激励、控制流和数据依赖进行静态结构对齐，随后对执行轨迹进行动态行为一致性检查。
• 覆盖率驱动的精化：通过符号执行和覆盖率分析，引导生成边界情况激励，直至验证目标达到足够的结构覆盖率。
• 知识增强的LLM Agent：一个异构的HLS验证知识图谱提供可复用的结构先验，Agent协调LLM生成、KLEE、gcov、gcc和Vitis HLS形成闭环。

数据集内容

当前发布的基准预览包含：

• 文件：HLS_LeVeri_benchmark.json
• 数量：107个独立验证目标，从 hlstrans 中筛选并增强而来
• 每条记录包含：成对的黄金C和HLS-C基准信息

论文中进一步构建了更大的已验证四元组数据集，结构为：

(P_c, P_h, TB_c, TB_h)

其中：

• P_c：黄金C/C++程序
• P_h：面向HLS的实现
• TB_c：黄金C测试平台
• TB_h：HLS-C测试平台

与其他数据集对比

数据集	C	HLS-C	C-TB	HLS-C-TB
HLSDataset	✗	✓	✗	✓
HLS-Eval	✗	✓	✗	✓
HLSTrans	✓	✓	✗	✗
HLSPilot	✓	✓	✗	✗
Ours	✓	✓	✓	✓

本数据集提供了完整的 C / HLS-C / C-Testbench / HLS-C-Testbench 结构，这是此前资源所不具备的。

相关论文

论文《Shift-Left High-Level Synthesis Verification via Knowledge-Augmented LLM Agent》发布在 arXiv 上，地址为：https://arxiv.org/abs/2606.17128

搜集汇总

数据集介绍

构建方式

HLS-LeVeri基准数据集基于HLSTrans语料库进行系统性筛选与增强，通过滤除不完整或语义不一致的样本，最终保留了107个独立的验证目标。每个目标均以四元组结构呈现，即原始C/C++规格程序、HLS导向C实现、对应的C测试基准以及HLS-C测试基准。这一完整四元组的设计填补了现有资源中测试基准缺失的空白，由知识增强的大语言模型智能体通过静态结构对齐与动态行为一致性校验自动构建，确保测试基准对在语义上对齐且覆盖率达标。

特点

该数据集的核心特点在于其首次提供了完整的C/HLS-C/测试基准四元组结构，覆盖了从规格到实现的全部验证环节。通过双层一致性校验——包括输入刺激、控制流与数据依赖的静态结构对齐，以及执行轨迹的动态行为一致性分析——保证了测试基准对的高语义保真度。此外，数据集融入覆盖驱动细化机制与异构HLS验证知识图谱，能够引导生成边缘情况刺激直至达到足够的结构覆盖率，为移位左验证研究提供了高质量的资源基础。

使用方法

用户可直接加载HLS_LeVeri_benchmark.json文件获取107个验证目标，每个条目包含配对程序及其测试基准路径。研究场景包括评估不同验证工具在移位左HLS验证任务上的表现，或将其作为训练与测试基准，用于开发基于大语言模型的自动验证智能体。建议使用标准C编译环境以及Vitis HLS工具链来执行测试基准并对比输出一致性，如需扩展实验可使用数据集结构构建更大的四元组验证集合。

背景与挑战

背景概述

随着电子设计自动化技术的迅猛发展，高层次综合（HLS）已成为将C/C++程序转化为硬件实现的核心手段。然而，在综合之前，对黄金C规范与HLS导向C实现之间的功能一致性进行验证，始终是一个棘手难题。HLS-LeVeri基准数据集由清华大学的Zhihan Xiao、Zhe Zhao、Luke Ztz Hu和Songping Mai等人创建，旨在推动移位左验证（Shift-Left Verification）阶段的研究。该数据集构建了包含107个独立验证目标的基准预览，每个目标均提供配对的高覆盖、语义对齐的C与HLS-C测试台，完整覆盖（P_c, P_h, TB_c, TB_h）四元组结构，填补了现有数据集仅提供部分验证工件的空白。其发布对该领域的影响深远，为HLS验证的早期自动化与智能化奠定了坚实基础。

当前挑战

该数据集面临的挑战主要体现在两个方面。领域问题上，现有HLS验证流程多依赖综合后的仿真，难以在早期阶段检测功能失配，导致设计迭代成本高昂。构建过程中，面临三大难题：一是如何自动生成既覆盖输入刺激、控制流和数据依赖，又能捕捉行为一致性的双层一致性检验测试台；二是必须借助符号执行与覆盖率剖析，驱动生成覆盖边缘案例的精细测试台，直至达到充分的结构覆盖率；三是需要构建异构HLS验证知识图谱，通过LLM代理协调KLEE、gcov、GCC和Vitis HLS等工具，形成闭环验证，这对知识整合与工具编排提出了极高要求。

常用场景

经典使用场景

在高级综合（HLS）设计流程中，验证金黄色C规范与面向HLS的C实现之间的功能一致性是一项严峻挑战。HLS-LeVeri benchmark专为左移验证阶段设计，核心用途在于自动构建高覆盖、语义对齐的测试平台（testbench）对，对黄金C程序与HLS-C程序进行双层次一致性校验。通过结合静态结构对齐与动态行为追踪，该数据集不仅涵盖了控制流、数据依赖及执行轨迹的精细比对，还利用符号执行与覆盖率引导生成边界案例刺激，从而精准识别设计本身与测试平台引入的差异。其经典应用场景聚焦于在综合操作之前，以最小化人工干预实现验证目标的结构覆盖达标。

实际应用

在实际工程场景中，HLS-LeVeri benchmark为从软件原型到硬件加速的转型提供了可靠的安全网。工业界通常使用HLS将C/C++算法映射到FPGA或ASIC，而规范与实现间的隐蔽功能差异往往导致后期花大量成本进行综合后调试。利用本数据集，工程师可以在综合前以自动化测试平台全面校验HLS-C代码的行为一致性，显著降低回归测试与迭代维护的人力投入。此外，其知识增强型LLM代理框架可无缝嵌入企业级HLS开发流水线，实现从代码提交到验证报告生成的闭环流程，特别适用于对验证收敛周期有严格要求的异构计算产品线。通过减少无效综合迭代与加速bug定位，该数据集正在被用于优化通信基带、自动驾驶视觉处理器等高性能芯片的设计验证流程。

衍生相关工作

HLS-LeVeri benchmark的发布催生了一系列高质量衍生研究。后续工作基于其四元组结构与双层次校验机制，发展了更高效的测试平台自动生成算法，例如融合控制流敏感采样与变异测试的刺激优化策略。同时，该数据集提供的异构知识图谱成为训练专用LLM代理的基础资源，推动了提问式验证智能体在HLS领域的应用，相关工作在DAC、ICCAD等顶级会议上持续发表。此外，研究者利用该benchmark系统评估不同HLS编译器（如Vivado HLS、Intel i++）的语义保留特性，进而提出编译器自适应的错误注入检测方法。开源社区也受其启发，构建了更广泛的跨项目验证基准（如HLS-PolyBench），延伸了数据集的覆盖范围与复用价值，形成了以左移验证为核心的学术生态链。