This paper presents the derivation of an operational semantics from a denotational semantics for a subset of the widely used hardware description language Verilog. Our aim is to build equivalence between the operational and denotational semantics. We propose a discrete denotational semantic model for Verilog. A phase semantics is provided for each type of transition in order to derive the operational semantics.
%0 Conference Paper
%1 huibiao_01_deriving
%A Huibiao, Zhu
%A Bowen, Jonathan
%A Jifeng, He
%D 2001
%J Software Engineering Conference, 2001. APSEC 2001. Eighth Asia-Pacific
%K Verilog denotational derivation formal methods myown operational semantics
%P 177--184
%R http://dx.doi.org/http://dx.doi.org/10.1109/APSEC.2001.991475
%T Deriving operational semantics from denotational semantics for Verilog
%U http://dx.doi.org/http://dx.doi.org/10.1109/APSEC.2001.991475
%X This paper presents the derivation of an operational semantics from a denotational semantics for a subset of the widely used hardware description language Verilog. Our aim is to build equivalence between the operational and denotational semantics. We propose a discrete denotational semantic model for Verilog. A phase semantics is provided for each type of transition in order to derive the operational semantics.
@inproceedings{huibiao_01_deriving,
abstract = {This paper presents the derivation of an operational semantics from a denotational semantics for a subset of the widely used hardware description language Verilog. Our aim is to build equivalence between the operational and denotational semantics. We propose a discrete denotational semantic model for Verilog. A phase semantics is provided for each type of transition in order to derive the operational semantics.},
added-at = {2011-08-01T19:37:01.000+0200},
author = {Huibiao, Zhu and Bowen, Jonathan and Jifeng, He},
biburl = {https://www.bibsonomy.org/bibtex/28666a6ede01182ba486968b647213a75/jpbowen},
citeulike-article-id = {900240},
doi = {http://dx.doi.org/http://dx.doi.org/10.1109/APSEC.2001.991475},
interhash = {a0f23c820305cc514619ddbebc2d4699},
intrahash = {8666a6ede01182ba486968b647213a75},
journal = {Software Engineering Conference, 2001. APSEC 2001. Eighth Asia-Pacific},
keywords = {Verilog denotational derivation formal methods myown operational semantics},
pages = {177--184},
posted-at = {2006-10-16 23:32:08},
priority = {4},
timestamp = {2011-08-01T19:37:01.000+0200},
title = {Deriving operational semantics from denotational semantics for Verilog},
url = {http://dx.doi.org/http://dx.doi.org/10.1109/APSEC.2001.991475},
year = 2001
}