The bibliographic entry was discovered and compiled by a machine, and published without a person checking it against the publication. The publication itself is the authors' own work — this badge says nothing about it.
Revamping Verilog Semantics for Foundational Verification
From OpenAlex, which stores abstracts as an
index of words and their positions: what is shown is rebuilt from that,
and reads fluently whether or not it is what the author wrote.
Abstract
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{choi2025revamping,
title = {Revamping Verilog Semantics for Foundational Verification},
author = {Joonwon Choi and Jaewoo Kim and Jeehoon Kang},
year = {2025},
journal = {Proceedings of the ACM on Programming Languages},
publisher = {Association for Computing Machinery},
volume = {9},
number = {OOPSLA2},
pages = {950--977},
doi = {10.1145/3763084},
}