一句话：提出核心语言 λV，为 Verilog 给出覆盖完整特性、可执行且经测试的操作语义，并解决语义陷阱。
Verilog 是主流硬件描述语言，但其语义陷阱常困扰软硬件开发者，已有形式语义研究不够全面。本文借鉴 JavaScript/Python 核心语言思路，提出核心语言 λV，用尽可能少的语言结构刻画 Verilog 本质，并给出形式操作语义。λV 覆盖迄今最完整的语言特性，同时处理已知语义陷阱。作者用约 27,000 行 Java 实现并系统测试其全域性与与 Verilog 的一致性。作为可靠参考语义，λV 能发现真实模拟器中的语义 bug，揭示标准规范中的歧义；还可作为核心语言支持状态空间探索和 concolic execution 等工具。
With the increasing need to apply modern software techniques to hardware design, Verilog, the most popular Hardware Description Language (HDL), plays an infrastructure role. However, Verilog has several semantic pitfalls that often confuse software and hardware developers. Although prior research on formal semantics for Verilog exists, it is not comprehensive and has not fully addressed these issues. In this work, we present a novel scheme inspired by previous work on defining core languages for software languages like JavaScript and Python. Specifically, we define the formal semantics of Verilog using a core language called λ V , which captures the essence of Verilog using as few language structures as possible. λ V not only covers the most complete set of language features to date, but also addresses the aforementioned pitfalls. We implemented λ V with about 27,000 lines of Java code, and comprehensively tested its totality and conformance with Verilog. As a reliable reference semantics, λ V can detect semantic bugs in real-world Verilog simulators and expose ambiguities in Verilog’s standard specification. Moreover, as a useful core language, λ V has the potential to facilitate the development of tools such as a state-space explorer and a concolic execution tool for Verilog.
@article{paperbot1835,
title = {The Essence of Verilog: A Tractable and Tested Operational Semantics for Verilog},
author = {Qinlin Chen and Nairen Zhang and Jinpeng Wang and Tian Tan and Chang Xu and Xiaoxing Ma and Yue Li},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {OOPSLA2},
year = {2023},
doi = {10.1145/3622805}
}