Despite numerous previous formalisation projects targeting Verilog, the semantics of Verilog defined by 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 both inconsistent 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 to-date most complete Verilog formalisation inherits these problems and how after we repair these problems in the semantics it can be used to execute real-world designs. This repaired semantics is thus the first formalisation of Verilog’s simulation semantics compatible with real-world designs. Additionally, to make the results of this paper available to a wider (nonmathematical) audience, we provide a visual formalisation of Verilog’s simulation semantics.