Combining operational semantics, logic programming and literate programming in the specification and animation of the verilog hardware description language

An operational semantics for a significant subset of the Verilog Hardware Description Language (HDL) has been developed. An unusual aspect of the semantics is that it was formulated as a Prolog logic program. This allows the possibility of simulating the semantics. In addition, a literate programming style has been used, so the semantics can be processed by the LATEX document preparation system with minimal and fully automated preprocessing. Bringing together the paradigms of operational semantics, logic programming and literate programming in this manner has proved a great aid in a number of ways. It has helped improve the understanding of the semantics, in the formalization of semantic aspects left informal in the original mathematical formulation of the semantics, and in the maintenance of the formal semantics and its associated informal description.