Mechanical Approach to Linking Operational Semantics and Algebraic Semantics for Verilog Using Maude

Verilog is a hardware description language (HDL) that has been standardized and widely used in industry. It contains interesting features such as event-driven computation and shared-variable concurrency. This paper considers how the algebraic semantics links with the operational semantics for Verilog. Our approach is to apply the equational and rewriting logic system Maude in exploring the linking theories. Firstly we present the algebraic semantics for Verilog. We introduce the concept of head normal form and every program is expressed as a guarded choice with location status. Secondly we present the strategy of deriving operational semantics from algebraic semantics. Our mechanical approach using Maude can visually show the head normal form of each program, as well as the execution steps of a program based on the derivation strategy. Finally we also mechanize the derived operational semantics. The results mechanized from the second and third exploration indicate that the transition system of the derived operational semantics is the same as the one based on the derivation strategy.