一句话：提出基于最小不动点的 Verilog 语义，支持周期级求值与模块化推理，并在 Rocq 中证明其与标准调度语义等价。
Verilog RTL 设计的验证长期依赖模型检测，但存在状态爆炸、表达力有限与可信基庞大等问题。演绎验证虽表达力强、TCB 小，却因 Verilog 标准语义的非确定性与全局调度难以应用。本文提出一种面向演绎验证的新 Verilog 语义，以最小不动点为核心，实现周期级函数式求值与模块化推理；针对可综合设计，证明该语义与标准调度语义等价。作者在 Rocq 中机器化全部结果，并完成流水线 RISC-V 处理器的模块化功能正确性与进展性验证，表明该语义可支撑根基性硬件验证。
In formal hardware verification, particularly for Register-Transfer Level (RTL) designs in Verilog, model checking has been the predominant technique. However, it suffers from state explosion, limited expressive power, and a large trusted computing base (TCB). Deductive verification offers greater expressive power and enables foundational verification with a minimal TCB. Nevertheless, Verilog’s standard semantics, characterized by its nondeterministic and global scheduling, pose significant challenges to its application. To address these challenges, we propose a new Verilog semantics designed to facilitate deductive verification. Our semantics is based on least fixpoints to enable cycle-level functional evaluation and modular reasoning. For foundational verification, we prove our semantics equivalent to the standard scheduling semantics for synthesizable designs. We demonstrate the benefits of our semantics with a modular verification of a pipelined RISC-V processor’s functional correctness and progress guarantees. All our results are mechanized in Rocq.
@article{paperbot2914,
title = {Revamping Verilog Semantics for Foundational Verification},
author = {Joonwon Choi and Jaewoo Kim and Jeehoon Kang},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA2},
year = {2025},
doi = {10.1145/3763084}
}