Formal Engineering Methods, International Conference on (2000)
Sept. 4, 2000 to Sept. 7, 2000
Jonathan P. Bowen , South Bank University
He Jifeng , United Nations University
Xu Qiwen , United Nations University
An operational semantics of a significant subset of the Verilog Hardware Description Language (HDL) is presented. The semantics is encoded using the logic programming language Prolog in a literate programming style. This allows the associated documentation to be maintained in step with the semantics, and the printed version to be presented in a standard mathematical operational semantics style. It also enables the semantics to be directly animated using a Prolog interpreter. Using this approach allows the exploration of sometimes-subtle behaviours of parallel programs and the possibility of rapid changes or additions to the semantics of the language covered that could be missed otherwise. In addition, it provides an extra check on the validity of the operational semantics.
H. Jifeng, X. Qiwen and J. P. Bowen, "An Animatable Operational Semantics of the Verilog Hardware Description Language," Formal Engineering Methods, International Conference on(ICFEM), York, England, 2000, pp. 199.