利用 LLM 辅助 RTL 的形式验证
硬件体系结构
2024-10-28 v2 软件工程
摘要
形式属性验证(FPV)已存在数十年,并被证明能有效发现复杂的 RTL 错误。然而,形式属性(如以 SystemVerilog Assertions (SVA) 编写的)即便对经验用户也耗时且易错。已有工作试图通过提高抽象层级来减轻此负担,从高层规范生成 SVA。但这并未消除对详细硬件行为推理与书写的人工投入。受异构硬件时代对 FPV 需求增长及大语言模型(LLM)进展的推动,我们探索 LLM 是否能捕捉 RTL 行为并生成正确的 SVA 属性。首先,我们设计了一个基于 FPV 的评估框架来衡量 SVA 的正确性与完备性。随后,我们迭代评估 GPT4 以提炼出提示其生成更好 SVA 所需的语法与语义规则集。我们将开源 AutoSVA 框架扩展,集成我们改进的基于 GPT4 的流程以生成安全属性,并辅助其已有的活性属性流程。最后,我们的用例评估了(1) GPT4 生成的 SVA 在复杂开源 RTL 上的 FPV 覆盖率,以及(2) 使用生成的 SVA 提示 GPT4 从零创建 RTL。通过这些实验,我们发现 GPT4 即便对存在缺陷的 RTL 也能生成正确的 SVA,且不镜像设计错误。特别地,它生成的 SVA 暴露了 RISC-V CVA6 核中一个先前工作评估未发现的错误。
引用
@article{arxiv.2309.09437,
title = {Using LLMs to Facilitate Formal Verification of RTL},
author = {Marcelo Orenes-Vera and Margaret Martonosi and David Wentzlaff},
journal= {arXiv preprint arXiv:2309.09437},
year = {2024}
}
备注
This work has been submitted to the IEEE for possible publication