
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++.
operational semantics framework; RTL hardware IP
operational semantics framework; RTL hardware IP
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 0 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
