Verilog代数语义研究

Study on the Algebraic Semantics of Verilog

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

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.