Article :Browse 3548 Download 3508
Received:February 13, 2001 Revised:April 24, 2001
Received:February 13, 2001 Revised:April 24, 2001
Abstract:In this paper, a structural operational semantic model is presented for a core subset of Verilog, and the subset has the main features of Verilog such as event-driven computation, shared-variable concurrency, time-delay, and so on. And all the Verilog processes are seen as open systems in this operational semantic model, so a model of observation is provided for open Verilog processes, and use observation equivalence based on bisimulation to identify the equivalence between programs. The observation equivalence can be proved to be a congruence for all Verilog operators, so it provides a sound base for deriving the algebraic laws for Verilog processes.
Foundation items:
Author Name | Affiliation |
LI Yong-jian | 上海交通大学,计算机科学与工程系,上海,200030 |
HE Ji-feng | 澳门联合国大学,国际软件技术研究所,澳门 |
SUN Yong-qiang | 上海交通大学,计算机科学与工程系,上海,200030 |
Reference text:
LI Yong-jian,HE Ji-feng,SUN Yong-qiang.Study on the Operational Semantics of Verilog.Journal of Software,2002,13(10):2021-2030
LI Yong-jian,HE Ji-feng,SUN Yong-qiang.Study on the Operational Semantics of Verilog.Journal of Software,2002,13(10):2021-2030