System Verilog Assertion (SVA) formulation, a critical yet complex task, is a pre-requisite in the Formal Property Verification (FPV) process. Traditionally, SVA formulation involves expert-driven interpretation of specifications. This is time consuming and prone to human error. However, recent advances in Large Language Models (LLM), LLM-informed automatic assertion generation is gaining interest. We designed a novel LLM-based pipeline to generate assertions in English Language, Linear Temporal Logic, and SVA from natural language specifications. We developed a custom LLM-based on OpenAI GPT4 for our experiments. Furthermore, we developed testbenches to verify/validate the LLM-generated assertions. Only 43% of LLM-generated raw assertions had errors, including syntax and logical errors. By iteratively prompting the LLMs using carefully crafted prompts derived from test case failures, the pipeline could generate correct SVAs after a maximum of nine iterations of prompting. Our results show that LLMs can streamline the assertion generation workflow, reshaping verification workflows.

翻译：System Verilog断言（SVA）的制定是形式属性验证（FPV）过程中的关键但复杂的先决任务。传统上，SVA制定依赖于专家驱动的规范解读，这一过程耗时且易受人为错误影响。然而，随着大语言模型（LLM）的近期进展，基于LLM的自动断言生成正引起广泛关注。我们设计了一种新型LLM流水线，可从自然语言规范生成英语、线性时序逻辑和SVA三种形式的断言，并基于OpenAI GPT4开发了定制化LLM用于实验。此外，我们构建了测试平台以验证/校验LLM生成的断言。原始LLM生成的断言中仅43%存在错误（含语法错误与逻辑错误）。通过基于测试用例失败信息精心构建提示词进行迭代提示，该流水线在最多九次迭代后即可生成正确的SVA。研究结果表明，LLM能够简化断言生成工作流，重塑验证流程。