论文笔记：(Security) Assertions by Large Language Models

来源：IEEE TRANSACTIONS ON INFORMATION FORENSICS AND SECURITY

I. 引言

计算机系统的安全性通常依赖于硬件的根信任。硬件漏洞可能对系统造成严重影响，因此需要支持安全验证的技术。断言验证是一种流行的验证技术，通过一组断言捕捉设计意图，用于非正式验证或测试检查。然而，编写以安全为中心的断言是一项具有挑战性的任务。在这项工作中，我们研究了新兴的大型语言模型（LLMs）在硬件断言生成中的应用，主要使用自然语言提示（如代码注释）来生成SystemVerilog断言。我们关注的是一个流行的LLM，并描述了其在“开箱即用”的情况下生成断言的能力，给定提示中不同详细程度的变化。我们设计了一个评估框架，生成各种提示，并创建了一个包含真实世界硬件设计和相应黄金参考断言的基准套件，我们希望利用LLM生成这些断言。

II. 相关工作

A. 断言验证
断言验证是数字设计流程的一部分，其中设计师意图被捕获为一组属性，在模拟、形式验证或合成到实际硬件中进行运行时检查。断言用于静态证明属性或动态验证。

B. 大型语言模型
LLMs是基于Transformer的人工神经网络，能够处理大量的文本数据集。OpenAI的Codex和GitHub Copilot等工具利用LLMs生成代码，显示出其在理解和生成代码方面的潜力。

C. 断言生成的自