%0 Journal Article
%T Study on the Operational Semantics of Verilog
Verilog操作语义研究
%A LI Yong-jian
%A HE Ji-feng
%A SUN Yong-qiang
%A
李勇坚
%A 何积丰
%A 孙永强
%J 软件学报
%D 2002
%I
%X 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.
%K Verilog
%K event scheduling
%K operational semantics
%K observation model
%K bisimulation
%K congruence
Verilog
%K 事件调度
%K 操作语义
%K 观察模型
%K 互模拟
%K 同余性
%U http://www.alljournals.cn/get_abstract_url.aspx?pcid=5B3AB970F71A803DEACDC0559115BFCF0A068CD97DD29835&cid=8240383F08CE46C8B05036380D75B607&jid=7735F413D429542E610B3D6AC0D5EC59&aid=DCDA9E82C6C89C65&yid=C3ACC247184A22C1&vid=FC0714F8D2EB605D&iid=F3090AE9B60B7ED1&sid=9475FABC7A03F4AB&eid=AA2DEEB9912F5067&journal_id=1000-9825&journal_name=软件学报&referenced_num=3&reference_num=11