arXiv:2503.19174v2 宣告类型: 替换 摘要: 从自然语言规范生成系统Verilog断言（SVAs）仍然是形式验证（FV）中的一个主要挑战，这主要是由于规范固有的模糊性和不完整性问题。现有的基于LLM的方法，如AssertLLM，专注于从规范文档中提取信息，往往无法捕捉到RTL代码中存在的关键内部信号交互和设计细节，导致生成不完整或错误的断言。我们提出了一种新的方法，从规范和RTL两方面构建一个知识图谱（KG），使用硬件特定的模式和领域特定的实体及关系类型。我们从规范中创建一个初始的KG，然后系统地将其与从RTL代码中提取的信息融合，形成一个统一而全面的KG。这种结合表示法提供了一种更全面的设计理解，并允许进行多分辨率的上下文合成过程，该过程旨在从KG中提取各种验证上下文。在四种设计上的实验表明，我们的方法在SVAs的质量上显著优于之前的方法。这种结构化的表示不仅提高了FV，也为未来研究代码生成和设计理解等任务铺平了道路。