System Verilog Assertion (SVA) formulation- a critical yet complex task is a prerequisite in the Formal Property Verification (FPV) process. Traditionally, SVA formulation involves expert-driven interpretation of specifications, which is timeconsuming and prone to human error. However, LLM-informed automatic assertion generation is gaining interest. We designeda novel framework called ChIRAAG, based on OpenAI GPT4, to generate SVA assertions from natural language specifications. ChIRAAG constitutes the systematic breakdown of design specifications into a standardized format, further generating assertions from formatted specifications using LLM. Furthermore, we developed testbenches to verify/validate the LLM-generated assertions. Automatic feedback of log files from the simulation tool to the LLM ensures that the framework can generate correc SVAs automatically. Only 33% of LLM-generated raw assertions had errors. Our results on OpenTitan designs shows that LLMs can streamline and assist engineers in the assertion generation process, reshaping verification workflows.

翻译：System Verilog断言（SVA）编制——作为形式属性验证（FPV）流程中的一项关键而复杂的任务，传统上依赖专家对设计规格进行解读，这一过程耗时且易引入人为错误。近年来，基于大语言模型（LLM）的自动化断言生成方法逐渐受到关注。本文设计了一种名为ChIRAAG的新型框架，基于OpenAI GPT4，可从自然语言规格说明自动生成SVA断言。ChIRAAG通过系统化地将设计规格分解为标准格式，进而利用LLM从格式化规格中生成断言。此外，我们开发了验证测试平台以检验LLM生成的断言，并通过将仿真工具生成的日志文件自动反馈至LLM，确保框架能够自主生成正确的SVA。实验表明，仅33%的LLM原始生成的断言存在错误。基于OpenTitan设计的研究结果显示，LLM可有效简化并辅助工程师完成断言生成任务，从而重塑验证工作流程。