Verilog代数语义研究

• 作者: 何积丰 孙永强 李勇坚
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: Verilog 代数语义 可靠性 完备性 范式归约 事件 事件触发
• 年，卷（期）: 2003,（3）
• 所属期刊栏目: 理论计算机科学
• 页码范围: 317-327
• 页数: 11页
• 分类号: TP301
• 字数: 14883字
• 语种: 中文

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	孙永强	上海交通大学计算机科学与工程系	72	373	10.0	15.0
2	李勇坚	中国科学院软件研究所	6	9	2.0	2.0
3	何积丰	澳门联合国大学国际软件技术研究所	4	16	3.0	4.0