Formalising VERILOG

This paper defines a non-trivial subset of VERILOG using a Plotkin-style operational semantics. We discuss the algebraic properties of programs based on the notion of bisimulation.