Study on the Algebraic Semantics of Verilog
DOI:
Author:
Affiliation:

Clc Number:

Fund Project:

  • Article
  • |
  • Figures
  • |
  • Metrics
  • |
  • Reference
  • |
  • Related
  • |
  • Cited by
  • |
  • Materials
  • |
  • 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
    Related
    Cited by
Get Citation

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

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:October 10,2001
  • Revised:May 17,2002
  • Adopted:
  • Online:
  • Published:
You are the firstVisitors
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