The Simulation Semantics of Synthesisable Verilog

TL;DR

This paper identifies and repairs inconsistencies in the Verilog standard's simulation semantics, resulting in a formalisation that can execute real-world hardware designs and is accessible through visualisation.

Contribution

It provides the first executable and visual formalisation of Verilog's simulation semantics that aligns with real-world hardware practice.

Findings

Identified key inconsistencies in the Verilog standard

Repaired the formalisation to be executable

Validated the formalisation with real hardware designs

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.