From algebraic semantics to denotational semantics for Verilog |
| |
Authors: | Huibiao Zhu Jifeng He Jonathan P Bowen |
| |
Affiliation: | (1) Software Engineering Institute, East China Normal University, 3663 Zhongshan Road (North), Shanghai, 200062, China;(2) Museophile Limited, Oak Barn, Sonning Eye, Reading, RG4 6TN, UK |
| |
Abstract: | This paper considers how the algebraic semantics for Verilog relates with its denotational semantics. Our approach is to derive
the denotational semantics from the algebraic semantics. We first present the algebraic laws for Verilog. Every program can
be expressed as a guarded choice that can model the execution of a program. In order to investigate the parallel expansion
laws, a sequence is introduced, indicating which instantaneous action is due to which exact parallel component. A head normal
form is defined for each program by using a locality sequence. We provide a strategy for deriving the denotational semantics
based on head normal form. Using this strategy, the denotational semantics for every program can be calculated. Program equivalence
can also be explored by using the derived denotational semantics.
A short version of this paper appeared in Proc. ICECCS 2006: 11th IEEE International Conference on Engineering of Complex Computer Systems 48]. This work is partially supported by the National Basic Research Program of China (No. 2005CB321904), the National High
Technology Research and Development Program of China (No. 2007AA010302) and the National Natural Science Foundation of China
(No. 90718004). Jonathan Bowen is a visiting professor at King’s College London and an emeritus professor at London South
Bank University. |
| |
Keywords: | Algebraic semantics Denotational semantics Unifying theories of programming Semantic relating Verilog |
本文献已被 SpringerLink 等数据库收录! |
|