Structural operational semantics for supporting multi-cycle operations in RTL HDLs

In this paper we formally define an operational semantics framework RTL++ for modeling behavioral RTL hardware IP. The semantics we define is neutral to existing HDLs and extends traditional sense RTL by natively supporting pipelined and multi-cycled operations with a unified register variable type. We believe this formalization help to guide the design of new HDLs or extensions of existing HDLs in terms of elevating RTL design abstraction level and also bridging the current HDL semantic gap among synthesis, simulation and formal verification tools. The intra-module and inter-module execution of RTL++ semantics are specified in Plotkin-style structural operational semantics framework. An example of implementing the RTL++ extension of SystemC is presented along with experimental results showing the benefit of modeling in RTL++.