Study on the Operational Semantics of 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.