• Article
  • | |
  • Metrics
  • |
  • Reference [14]
  • |
  • Related
  • |
  • Cited by
  • | |
  • Comments
    Abstract:

    In this paper, the algebraic semantics of Verilog is explored, which is a collection of laws associated with Verilog constructs. These laws provide a precise framework for describing and defining the semantics of Verilog. The special features of the semantics of Verilog are shown. All the laws presented above are sound with respect to the operational semantics, i.e., if the two processes are the two sides of a law, then they are bisimilar. At last, the completeness of the algebraic laws with respect to a subset of Verilog and the operational semantics, i.e., are explored, if such programs are bisimilar, then they are algebraically equivalent. For the proof of completeness, this method will be the discovery of a normal form program for any such programs. Each such program will have an equivalent normal form program (through transformation by the algebraic laws), but two normal form programs will be bisimilar in the operational semantics if and only if they are syntactically equivalent in a simple way. These results are of theoretical significance, for the theories of process algebra are concentrated on the channel- communication concurrent languages. But there is little work on the shared-variable concurrent languages, and a general and effective treatment to the research of such kind of complex concurrent languages is proposed in this paper.

    Reference
    [1]Li YJ, He JF, Sun YQ. Study on the operational semantics of Verilog. Journal of Software, 2002,13(10):2021~2030 (in Chinese with English Abstract).
    [2]Zhu HB, He JF. A DC-based semantics for Verilog. In: Feng YL, Notkin D, Gaudel, M-C, eds. Proceedings of the 16th IFIP World Computer Congress 2000: Theory and Practice (ICS2000). Beijing: Publishing House of Electronics Industry, 2000. 421~432.
    [3]Hoare CAR, He JF. Unifying Theories of Programming. Prentice Hall, 1998.
    [4]Xu QW. A theory of state-based parallel programming . Oxford University Computing Laboratory, 1992.
    [5]Li YJ. A study on the formal semantics of Verilog . Shanghai: Shanghai Jiaotong University, 2001 (in Chinese with English Abstract).
    [6]Hoare CAR, Hayes IJ, He JF. Laws of programming. Communications of the ACM, 1987,30(8):672~686.
    [7]Roscoe AW, Hoare CAR. Laws of Occam programming. Theoretical Computer Science, 1988,60:177~229.
    [8]Sampaio A. An Algebraic Approach to Compiler Designer. World Scientific, 1997.
    [9]Miler R. Communication and Concurrency. Prentice Hall, 1989.
    [10]Hoare CAR. Communicating Sequential Processes. Prentice Hall, 1985.
    [11]Iyoda J, He JF. Towards an algebraic synthesis of Verilog. Technical Report 218, Macau: UNU/IIST, 2001.
    [12]Iyoda J, He JF. A prolog prototype for the synthesis of Verilog. Technical Report 237, Macau: UNU/IIST, 2001.
    [13]李勇坚,何积丰,孙永强.Verilog操作语义研究.软件学报,2002,13(10):2021~2030.
    [14]李勇坚.Verilog语言形式化语义研究[博士学位论文].上海:上海交通大学,2001.
    Related
    Cited by
    Comments
    Comments
    分享到微博
    Submit
Get Citation

李勇坚,何积丰,孙永强. Verilog代数语义研究.软件学报,2003,14(3):317-327

Copy
Share
Article Metrics
  • Abstract:4073
  • PDF: 5653
  • HTML: 0
  • Cited by: 0
History
  • Received:October 10,2001
  • Revised:May 17,2002
You are the first2035322Visitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address:4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code:100190
Phone:010-62562563 Fax:010-62562533 Email:jos@iscas.ac.cn
Technical Support:Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063