Verilog操作语义研究  

Study on the Operational Semantics of Verilog

作　　者：李勇坚[1] 何积丰[2] 孙永强[1] 

机构地区：[1]上海交通大学计算机科学与工程系,上海200030 [2]澳门联合国大学国际软件技术研究所

出　　处：《软件学报》2002年第10期2021-2030,共10页Journal of Software

基　　金：澳门联合国大学国际软件技术研究所"实时混成系统的研究技术"(Design Techniques for Real-Time Hybrid Systems)研究计划的资助项目~

摘　　要：提出了一个结构化操作语义模型,用于描述Verilog核心子集的语言特征,此子集包含了事件驱动、基于共享变量的并发特性、时间延迟等Verilog的主要语言成分.在此操作语义模型中,所有的Verilog程序将被统一地认为是开放式系统,所以在此操作语义模型的基础上能够进一步提出Verilog开放进程的观察模型,并提出基于互模拟的观察等价概念来判定进程之间的等价关系.最后证明了所定义的观察等价关系对所有的Verilog构造子而言是一个同余关系,从而为发展相应的进程代数理论提供了一个可靠性基础.In this paper, a structural operational semantic model is presented for a core subset of Verilog, and the subset has the main features of Verilog such as event-driven computation, shared-variable concurrency, time-delay, and so on. And all the Verilog processes are seen as open systems in this operational semantic model, so a model of observation is provided for open Verilog processes, and use observation equivalence based on bisimulation to identify the equivalence between programs. The observation equivalence can be proved to be a congruence for all Verilog operators, so it provides a sound base for deriving the algebraic laws for Verilog processes.

关 键 词：VERILOG语言 操作语义 事件调度 观察模型 互模拟 同余性 

分 类 号：TP312[自动化与计算机技术—计算机软件与理论]