This paper presents the derivation of a denotational semantics from an operational semantics for a subset of the widely used hardware description language Verilog. Our aim is to build an equivalence between the operational and denotational semantics. We propose a discrete time semantic model for Verilog. Algebraic laws are also investigated in this paper, with the ultimate aim of providing a unified set of semantic views for Verilog.
%0 Book Section
%1 huibiao_01_from
%A Huibiao, Zhu
%A Bowen, Jonathan
%A Jifeng, He
%D 2001
%J Correct Hardware Design and Verification Methods
%K Verilog denotational formal methods myown operational semantics
%P 449--464
%R http://dx.doi.org/10.1007/3-540-44798-9\_34
%T From Operational Semantics to Denotational Semantics for Verilog
%U http://dx.doi.org/10.1007/3-540-44798-9\_34
%X This paper presents the derivation of a denotational semantics from an operational semantics for a subset of the widely used hardware description language Verilog. Our aim is to build an equivalence between the operational and denotational semantics. We propose a discrete time semantic model for Verilog. Algebraic laws are also investigated in this paper, with the ultimate aim of providing a unified set of semantic views for Verilog.
@incollection{huibiao_01_from,
abstract = {This paper presents the derivation of a denotational semantics from an operational semantics for a subset of the widely used hardware description language Verilog. Our aim is to build an equivalence between the operational and denotational semantics. We propose a discrete time semantic model for Verilog. Algebraic laws are also investigated in this paper, with the ultimate aim of providing a unified set of semantic views for Verilog.},
added-at = {2011-08-01T19:38:42.000+0200},
author = {Huibiao, Zhu and Bowen, Jonathan and Jifeng, He},
biburl = {https://www.bibsonomy.org/bibtex/263c959d626a443d3b2d56003db73f9a6/jpbowen},
citeulike-article-id = {2505195},
doi = {http://dx.doi.org/10.1007/3-540-44798-9\_34},
interhash = {1a5b3ff49d8cbff683d05bf902efc385},
intrahash = {63c959d626a443d3b2d56003db73f9a6},
journal = {Correct Hardware Design and Verification Methods},
keywords = {Verilog denotational formal methods myown operational semantics},
pages = {449--464},
posted-at = {2008-03-11 01:30:50},
priority = {4},
timestamp = {2011-08-01T19:38:42.000+0200},
title = {From Operational Semantics to Denotational Semantics for Verilog},
url = {http://dx.doi.org/10.1007/3-540-44798-9\_34},
year = 2001
}