The security of computer systems typically relies on a hardware root of trust. As vulnerabilities in hardware can have severe implications on a system, there is a need for techniques to support security verification activities. Assertion-based verification is a popular verification technique that involves capturing design intent in a set of assertions that can be used in formal verification or testing-based checking. However, writing security-centric assertions is a challenging task. In this work, we investigate the use of emerging large language models (LLMs) for code generation in hardware assertion generation for security, where primarily natural language prompts, such as those one would see as code comments in assertion files, are used to produce SystemVerilog assertions. We focus our attention on a popular LLM and characterize its ability to write assertions out of the box, given varying levels of detail in the prompt. We design an evaluation framework that generates a variety of prompts, and we create a benchmark suite comprising real-world hardware designs and corresponding golden reference assertions that we want to generate with the LLM.

翻译：计算机系统的安全性通常依赖于硬件信任根。由于硬件漏洞可能对系统造成严重影响，因此需要技术支持安全验证活动。基于断言的验证是一种流行的验证技术，它通过一组断言捕获设计意图，这些断言可用于形式化验证或基于测试的检查。然而，编写以安全为中心的断言是一项具有挑战性的任务。本文研究了利用新兴的大语言模型（LLM）进行硬件安全断言生成中的代码生成，其中主要使用自然语言提示（例如断言文件中作为代码注释出现的提示）来生成SystemVerilog断言。我们聚焦于一种流行的LLM，表征其在给定不同详细程度的提示时开箱即用地编写断言的能力。我们设计了一个评估框架，生成各种提示，并创建了一个基准测试集，包含真实世界的硬件设计以及我们希望用LLM生成的对应黄金参考断言。