Verilog代数语义研究
DOI:
作者:
作者单位:

作者简介:

通讯作者:

中图分类号:

基金项目:

Supported by the DTfRTS (Design Techniques for Real-Time Hybrid Systems) Project of the International Institute for Software Technology, United Nations University (澳门联合国大学国际软件技术研究所"实时混成系统的研究技术"研究计划)


Study on the Algebraic Semantics of Verilog
Author:
Affiliation:

Fund Project:

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
  • |
  • 文章评论
    摘要:

    给出了Verilog的代数语义.这是一个等式公理体系,它将Verilog语义特征通过代数规则简洁而准确地表达出来;并且这个代数语义相对于已经所作的操作语义模型来讲是可靠的,即所有的这些代数规则左右两边的进程在操作语义的观察模型下都是互模拟的.研究了此代数语义的相对完备性,即参照前面的操作语义模型,相对于扩展Verilog语言的一个子集而言,此代数语义是完备的.即所有符合这样语法的程序,如果它们是互模拟等价的,那么它们同样可以在所提出的代数系统中被推导相等.在完备性证明过程中,采用范式方法,即构造一种语法上特殊的程序,任何属于上述子集中的一个程序通过该代数规则都能够被转化为范式程序,而且范式程序在操作语义模型下是互模拟的当且仅当它们是语法相同的.上述结果具有重要的理论意义,因为现有的进程代数理论主要是针对管道通信并行语言而展开的,而对于像Verilog这种以共享变量通信为基础的复杂并行语言研究还是比较少的,对此类复杂的基于共享变量的并行语言的进程代数理论研究提出了一种通用、有效的方法.

    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.

    参考文献
    相似文献
    引证文献
引用本文

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

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2001-10-10
  • 最后修改日期:2002-05-17
  • 录用日期:
  • 在线发布日期:
  • 出版日期:
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号