为基础验证改进Verilog语义

《Proceedings of the ACM on Programming Languages》：Revamping Verilog Semantics for Foundational Verification

形式验证中模型检查存在状态爆炸、表达力不足和TCB过大的问题，本文提出基于最小编正点的Verilog新语义，支持演绎验证的模块化推理，并证明其等价于标准调度语义，在RISC-V流水线处理器验证中应用该语义有效提升验证效率，所有结论通过Rocq工具实现。

　　

摘要

在正式的硬件验证中，尤其是对于使用Verilog实现的寄存器传输级（RTL）设计，模型检验一直是主要的技术手段。然而，模型检验存在状态爆炸问题、表达能力有限以及需要较大的可信计算基础（TCB）等问题。演绎验证则具有更强的表达能力，并且能够在较小的TCB下完成基础性验证。尽管如此，Verilog的标准语义（其非确定性和全局调度特性）对其应用带来了重大挑战。

为了解决这些问题，我们提出了一种新的Verilog语义，旨在促进演绎验证的进行。我们的新语义基于最小不动点理论，以实现周期级的功能评估和模块化推理。对于基础性验证，我们证明了这种新语义与可综合设计的标准调度语义等价。我们通过一个流水线RISC-V处理器的功能正确性及进度保证的模块化验证来展示这种新语义的优势。所有这些结果都已在Rocq框架下得到了验证。