FVEval：理解语言模型在数字硬件形式验证中的能力
硬件体系结构
2024-11-01 v1 人工智能
摘要
大型语言模型 (LLM) 的惊人推理和代码生成能力已推动了将其应用于数字芯片设计自动化的广泛兴趣。特别是，近期的研究探索了将这些模型应用于形式验证 (FV) 的早期想法——这是一种可提供强大置信度保证但需要大量人工工作的硬件实现验证方法。尽管 LLM 驱动的自动化价值显而易见，但我们对模型性能的理解却因缺乏整体评估而受限。为此，我们提出 FVEval，这是首个针对 characterizing LLM performance in FV 任务的 comprehensive benchmark 和 evaluation 框架。该基准由三个子任务组成，衡量 LLM 在不同层次上的能力：从根据自然语言描述生成 SystemVerilog 断言 (SVA) 到推理设计 RTL 并直接在无需额外人工输入的情况下建议断言。作为测试实例，我们提出了 expert 编写的验证 collateral 的集合以及用于与工业 FV 工作流程对齐的 scalable 方法以生成合成示例。我们对广泛的现有 LLM（包括专有和开源模型）进行了 FVEval 评估，随后研究了当今 LLM 所处位置以及如何进一步促进其应用以提高数字 FV 生产力。我们的数据集和 evaluation code 可在 \url{https://github.com/NVlabs/FVEval} 访问。
关键词
引用
@article{arxiv.2410.23299,
title = {FVEval: Understanding Language Model Capabilities in Formal Verification of Digital Hardware},
author = {Minwoo Kang and Mingjie Liu and Ghaith Bany Hamad and Syed Suhaib and Haoxing Ren},
journal= {arXiv preprint arXiv:2410.23299},
year = {2024}
}