The Simulation Semantics of Synthesisable Verilog

TL;DR

This work identifies that Verilog's simulation semantics, as specified by the standard, are inconsistent with practical use and with themselves, hindering formal reasoning about synthesisable hardware designs. It analyzes root causes, repairs the Chen et al. mathematical formalisation to be executable and practice-compatible, and demonstrates results on real and test-case hardware designs. In parallel, it introduces VV, a browser-based visualisation of Verilog's event queue to make the semantics accessible and aid debugging. Collectively, the repairs and the visual tool enable executable reasoning about Verilog designs and offer a path toward standard improvements and broader accessibility for tool developers and hardware designers alike.

Abstract

Despite numerous previous formalisation projects targeting Verilog, the semantics of Verilog defined by the Verilog standard -- Verilog's simulation semantics -- has thus far eluded definitive mathematical formalisation. Previous projects on formalising the semantics have made good progress but no previous project provides a formalisation that can be used to execute or formally reason about real-world hardware designs. In this paper, we show that the reason for this is that the Verilog standard is inconsistent both with Verilog practice and itself. We pinpoint a series of problems in the Verilog standard that we have identified in how the standard defines the semantics of the subset of Verilog used to describe hardware designs, that is, the synthesisable subset of Verilog. We show how the most complete Verilog formalisation to date inherits these problems and how, after we repair these problems in an executable implementation of the formalisation, the repaired implementation can be used to execute real-world hardware designs. The existing formalisation together with the repairs hence constitute the first formalisation of Verilog's simulation semantics compatible with real-world hardware designs. Additionally, to make the results of this paper accessible to a wider (nonmathematical) audience, we provide a visual formalisation of Verilog's simulation semantics.

Figures (8)

• Figure 1: Target syntax of expressions $e$, statements $s$, module items $\textit{mi}$, and modules $m$. Square brackets ($[\ldots]$) denote optional elements and times ($\ldots*$) denotes repetition. Redundant syntax is omitted to avoid clutter, e.g., "$\textit{ee} ,\,\textit{ee}$" instead of "$\textit{ee}\ \texttt{or}\ \textit{ee}$" in event expressions (ee) or reg instead of logic in variable declarations (mi).
• Figure 2: Three code fragments for discussing the semantics of procedural processes.
• Figure 3: Three code fragments for discussing the semantics of continuous assignments.
• Figure 4: Example hardware design circuit (a), test bench circuit_tb (b), and test-bench output (c).
• Figure 9: Intermodule simulation semantics problems.