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.

通过大语言模型 (LLM) 设计了一种新型流程，从自然语言规范中生成英语语言、线性时态逻辑和 System Verilog Assertion (SVA) 的断言，并使用测试平台验证生成的断言，验证结果表明 LLM 可以简化断言生成工作流程，改变验证工作流程。