FLAG：面向芯片通信协议形式规范的形式化与 LLM 辅助 SVA 生成

芯片通信协议的形式规范对系统单芯片 (SoC) 的设计与验证至关重要。然而，手动从非结构化文档构建这些形式规范往往繁琐且易出错。虽然近期研究尝试利用大语言模型 (LLM) 从设计文档生成 SystemVerilog Assertion (SVA) 属性以辅助寄存器-传输水平 (RTL) 设计验证，但在实际应用中，这些方法对通信协议的 SVA 生成并不奏效。由于协议规范文档具有非结构化且歧义性特征，LLM 往往难以提取必要信息，最终生成无关甚至错误的属性。我们提出 FLAG 框架，包含两个阶段以辅助从非形式化文档构建形式化协议规范。第一阶段采用预定义模板集生成候选 SVA 属性；为避免遗漏必要属性，我们发展基于语法的方法生成覆盖 various 通信协议关键信号行为的全面模板集。第二阶段结合无歧义时序图与规范文档中的文本描述，对错误属性进行筛选。首先采用形式化方法检查候选属性并筛除与时序图不一致的属性，然后咨询 LLM 进一步依据文本描述移除错误属性，最终获得完整的属性集。在 various 开源通信协议上的实验表明，FLAG 在从非形式化文档生成 SVA 属性方面有效且可靠。