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