An Operational Semantics of Verilog

Verilog is a kind of hardware description language used abroad in industrial fields, but the study on its formal semantics is not enough. This paper describes syntax and semantics of Verilog HDL with formal methods, and establishes an operational semantics of Verilog. We describe the states of nonintercurrent and intercurrent components by two-dimensional and four-dimensional arrays, depict state transition rules of different sentences, and portray the implementation of intercurrent programs with an example.