System Verilog Assertion (SVA) formulation -- a critical yet complex task is a prerequisite in the Assertion Based Verification (ABV) process. Traditionally, SVA formulation involves expert-driven interpretation of specifications, which is time-consuming and prone to human error. Recently, LLM-informed automatic assertion generation is gaining interest. We designed a novel framework called ChIRAAG, based on OpenAI GPT4, to generate SVA from natural language specifications of a design. ChIRAAG constitutes the systematic breakdown of design specifications into a standardized format, further generating assertions from formatted specifications using LLM. Furthermore, we used few test cases to validate the LLM-generated assertions. Automatic feedback of log messages from the simulation tool to the LLM ensures that the framework can generate correct SVAs. In our experiments, only 27% of LLM-generated raw assertions had errors, which was rectified in few iterations based on the simulation log. Our results on OpenTitan designs show that LLMs can streamline and assist engineers in the assertion generation process, reshaping verification workflows.

翻译：System Verilog断言（SVA）的制定——作为断言导向验证（ABV）流程中关键且复杂的环节——是验证过程的前提条件。传统上，SVA的制定需要专家对设计规范进行人工解读，这一过程耗时且易受人为错误影响。近年来，基于大语言模型（LLM）的自动化断言生成方法逐渐受到关注。我们设计了一个基于OpenAI GPT4的新型框架ChIRAAG，用于根据设计的自然语言规范生成SVA。该框架系统地将设计规范分解为标准化的格式，并利用LLM从格式化后的规范中生成断言。此外，我们使用少量测试用例来验证LLM生成的断言。通过将仿真工具的日志信息自动反馈给LLM，该框架能够确保生成正确的SVA。在我们的实验中，LLM生成的原始断言中仅有27%存在错误，这些错误基于仿真日志经过少量迭代后得以修正。我们在OpenTitan设计上的实验结果表明，LLM能够简化和辅助工程师的断言生成过程，从而重塑验证工作流程。