VERA-HLS

Paper-title form: VERA-HLS: Verified Evidence Retrieval and Assertion-Guided Repair for Low-Cost HLS Generation

VERA 表示 Verified Evidence Retrieval and Assertion-Guided Repair。这个名字对应当前论文主线：用经过工具验证的先验证据检索，配合诊断断言驱动的增量修复，让本地 LLM HLS agent 以较低 token 成本完成生成、仿真和综合闭环。

VERA-HLS 是一个面向 HLS 代码生成与修复的低成本知识增强 agent。当前仓库只保留论文主线的四个核心机制：

• A. Description-Grounded Contract Analysis：先读 kernel_description.md、header、testbench，得到算子类型、接口、数据格式、风险点和语义断言。
• B. Verified Prior Memory Retrieval：从 Vitis/HLS-Eval 验证过的本地先验库检索少量相关正负经验，作为短 capsule 注入。
• C. Functional Baseline Gate：生成代码后先用普通 C/C++ 编译和 testbench 运行，失败则不进入 Vitis，避免浪费综合时间。
• D. Assertion-Gated Incremental Repair：每一轮修复只基于工具输出生成“小断言”和“增量提示”，再做最小代码修改。

token report、budget ledger、workflow artifacts 只作为实验计量设施，不作为额外机制宣传。

目录结构

vera_hls/                  核心包：runner 支撑、HLS backend、memory、diagnosis、token/budget/workflow
scripts/run_hls_eval_benchmark.py  唯一 benchmark runner
scripts/build_hls_eval_prior_memory.py  从 HLS-Eval 构建本地先验 memory
scripts/convert_bench4hls_to_hls_eval.py Bench4HLS 转 HLS-Eval-like case
scripts/queues/                 当前有效实验队列脚本
tests/                          A-D core 单元测试和 mock 集成测试
configs/*.example.json          模型配置示例，真实 key/local config 不提交

环境准备

python -m venv .venv
source .venv/bin/activate
pip install -e ".[tui]"

真实模型配置使用本地 ignored config，例如：

cp configs/qwen3_coder_30b_local.json configs/qwen3_coder_30b.local.json

本项目不使用 .env。如果使用云端兼容 OpenAI API 的模型，也把 key 放在本地 config 中，不提交到 Git。

基础检查

pytest -q
VERA-HLS --help
python scripts/run_hls_eval_benchmark.py --help

构建 HLS-Eval 先验库

先验库只从训练/先验 split 中写入 reference prior，测试 split 不泄漏。以 hard16 作为测试集时：

python scripts/build_hls_eval_prior_memory.py \
  --data-dir external/hls-eval/hls_eval_data \
  --test-case-list experiments/full/E9_hls_eval_hard16_case_list.txt \
  --out-dir experiments/splits/hls_eval_prior_split \
  --memory-path .vera_hls/memory/hls_eval_prior.sqlite

该步骤会生成：

• split.csv：prior/test 划分。
• prior_cases.txt、test_cases.txt：case 列表。
• SQLite memory：包含 verified reference prior 和可选 negative failure memory。

单 case 运行

VERA-HLS run \
  --case-path external/hls-eval/hls_eval_data/c2hlsc/add_round_key \
  --model-config configs/qwen3_coder_30b.local.json \
  --hls-backend vitis \
  --hls-platform /opt/2025.2/Vitis/base_platforms/xilinx_kv260_base_202520_1/xilinx_kv260_base_202520_1.xpfm \
  --max-llm-calls 8 \
  --semantic-first-gate \
  --contract-analysis \
  --functional-baseline-repair-retries 2 \
  --assertion-gated-functional-repair \
  --memory-path .vera_hls/memory/hls_eval_prior.sqlite \
  --generation-prior-token-budget 900 \
  --generation-prior-limit 3 \
  --no-view --snapshot

全量实验复现

HLS-Eval hard16 pass@5：

bash scripts/queues/run_e10b_hls_eval_hard16_pass5_prior_gate_20260702.sh

Bench4HLS full pass@1/pass@5：

bash scripts/queues/run_e11_bench4hls_full_pass1_pass5_prior_gate_20260703.sh

Bench4HLS 需要先转换成 HLS-Eval-like case：

python scripts/convert_bench4hls_to_hls_eval.py \
  --bench4hls-root external/Bench4HLS \
  --out-dir external/bench4hls_hls_eval_like_all

关键输出

每个 sample 目录会包含：

operator_features.json              A 的描述级算子特征
contract_analysis.json              A 的 LLM 合同分析
contract_assertion_capsule.md       A 的短断言 capsule
generation_prior_gate.json          B 的先验使用决策
generation_prior_hits.json          B 的检索命中
functional_baseline_result*.json    C 的普通 C/C++ gate 结果
diagnosis_assertion_*.json/md       D 的小断言与增量提示
stage_entry_*.json/md               每个阶段进入时的小提示
token_report.json/csv               token 统计
budget_ledger.json                  工具/LLM budget 账本
stage_records.json                  阶段记录
workflow_status.json                当前/最终状态
result.json                         单样本最终结果

以上列表就是当前 core runner 的活跃输出集合；历史实验分支的输出不属于主线复现路径。

论文主线建议

建议把贡献点收敛成一句话：VERA-HLS 用“合同断言 + 验证先验 + 功能门禁 + 增量修复”把本地 LLM 的 HLS 生成从自由修补变成可验证、低 token、可泛化的工具闭环。

实验对比建议：

• B0：远端大模型固定 LOOP。
• B1：本地模型纯 LOOP，max loop 固定。
• B2：本地模型 + contract 但不使用 prior/gate/assertion repair。
• D：VERA-HLS core。

主数据集用 HLS-Eval，外部泛化用 Bench4HLS。报告 pass@1、pass@5、CSIM/SYNTH 通过率、平均 token、失败类别变化和 prior hit 情况。