Formal property verification (FPV) has existed for decades and has been shown to be effective at finding intricate RTL bugs. However, formal properties, such as those written as SystemVerilog Assertions (SVA), are time-consuming and error-prone to write, even for experienced users. Prior work has attempted to lighten this burden by raising the abstraction level so that SVA is generated from high-level specifications. However, this does not eliminate the manual effort of reasoning and writing about the detailed hardware behavior. Motivated by the increased need for FPV in the era of heterogeneous hardware and the advances in large language models (LLMs), we set out to explore whether LLMs can capture RTL behavior and generate correct SVA properties. First, we design an FPV-based evaluation framework that measures the correctness and completeness of SVA. Then, we evaluate GPT4 iteratively to craft the set of syntax and semantic rules needed to prompt it toward creating better SVA. We extend the open-source AutoSVA framework by integrating our improved GPT4-based flow to generate safety properties, in addition to facilitating their existing flow for liveness properties. Lastly, our use cases evaluate (1) the FPV coverage of GPT4-generated SVA on complex open-source RTL and (2) using generated SVA to prompt GPT4 to create RTL from scratch. Through these experiments, we find that GPT4 can generate correct SVA even for flawed RTL, without mirroring design errors. Particularly, it generated SVA that exposed a bug in the RISC-V CVA6 core that eluded the prior work's evaluation.

翻译：形式化属性验证（FPV）已存在数十年，并被证明能有效发现复杂的RTL漏洞。然而，即使对于经验丰富的用户，编写诸如SystemVerilog断言（SVA）等形式化属性既耗时又易出错。先前的研究尝试通过提高抽象层级，从高层规约生成SVA来减轻这一负担，但这并未消除对详细硬件行为进行推理和编写的人工工作量。受异构硬件时代对FPV需求增长以及大语言模型（LLM）技术进步的启发，我们开始探索LLM能否理解RTL行为并生成正确的SVA属性。首先，我们设计了一个基于FPV的评估框架，用于衡量SVA的正确性与完整性。然后，我们迭代评估GPT4，以构建一套引导其生成更优质SVA所需的语法和语义规则。我们通过集成改进后的GPT4流程来扩展开源AutoSVA框架，在生成安全属性的同时，也为其现有的活性属性生成流程提供支持。最后，我们通过用例评估了：（1）GPT4生成的SVA在复杂开源RTL上的FPV覆盖率；（2）利用生成的SVA引导GPT4从零开始创建RTL。通过实验发现，GPT4甚至能为存在缺陷的RTL生成正确的SVA，且不会复制设计错误。特别地，它生成的SVA成功暴露了RISC-V CVA6核心中一个未被先前工作评估发现的漏洞。