我们提出了HierSVA，这是一个集成套件，结合了用于LLM驱动的分层硬件形式验证的管道、数据集和基准测试。HierSVA-SP将RTL预处理工具链与LLM循环形式验证流程相结合，以生成分层RTL上的参考SystemVerilog Assertions (SVA)。通过将其应用于BaseJump STL，我们得到了HierSVA-DS，一个包含342个模块的数据集，具有层次元数据和深度范围0-9，并附带28个模块-错误对的深度子集，包含自然语言规范和错误变体。
HierSVA-B将断言质量分解为六个指标轴：语法正确性、断言证明成功率、空洞性、规范可信度、变异覆盖率和形式核心覆盖率。将HierSVA-B应用于十二个最近的LLM，揭示了三项发现。首先，模块级编译率为67.1%；在可评估的运行中生成的断言中，82.1%证明是非空洞的，但相应的断言集仅检测到了70.2%的可注入故障，并覆盖了36.2%的形式核心。其次，在深度子集中的211个可评估模型-模块条目上，断言集能够以0.87的召回率标记有缺陷的RTL，但40%的预测有缺陷结果是对正确RTL的假阳性，限制了精确度为0.60。第三，代理模式提高了S1风格的可证明性和强度指标，但增益趋于平稳并出现波动。
代码和文档可在 GitHub 获取，数据集可在 Hugging Face 获取。
博主点评： HierSVA通过将LLM与硬件验证结合，展现了深度学习在硬件设计领域的潜力，尤其是在形式验证的自动化方面。这一进展将为未来的硬件设计提供更高效的验证工具，尽管当前的假阳性率仍需关注与优化。