A Preliminary Study For Event Structure Of Concurrency System

Concurrency is very common in real world, including characteristics of parallel and distribution. Concurrent systems are defined as that run in multi-machines or machines supporting multiprocess. They are composed of a group of processes, which is defined by sequential programs, and shared actions, by which processes could complete tasks interactively. Integrated circuit is typical one of concurrent systems. Because their designs have become more and more complex, while release time shorter and shorter, there is the birth of new one with top to down manner, bases on Hardware Description Language(HDL). And designs can be done up till down with it.During HDL's growing, there are many language types, such as: VHDL, Verilog and SystemC, etc. Because different languages are adapt to different phases, much time is cost on repeatitious coding. Thus, SystemVerilog is advanced by Accellera to change this situation. It provides a major set of extensions to the Verilog-2001 standard, including features for high-level, abstract system modeling, testbench automation, and the integration of Verilog with the C programming language. With these new features, SystemVerilog can be applied in different design phases to reduce repeated work. And it allows modeling and verifying very large designs more easily and with less coding.The engineers of design and verification are also excited for these great functions provided by SystemVerilog. It, however, also means complexity. Hence, there is a problem that how to use SystemVerilog correctly and without ambiguity during different design procedures to make sure the correctness of designs. Obviously, the reference manual, provided by Accellera, is not strong enough to deal with it.Hence, we study the denotational semantics of SystemVerilog. Formal methods effectively support the system design process and transformation phases for their mathematically sound basis. There are mainly two types, including interleaving and noninterleaving models. In interleaving models, the system's behavior is modeled in terms of sequence of actions that are totally ordered by sequence. While, in noninterleaving models, it is modeled in terms of sequence of actions that are only partially ordered, which reflects the causal dependencies between actions. Event structures constitute a major branch of noninterleaving models. The basic ingredients are labeled events, and the causality, conflict, and independency relation between actions.In study, EBES, a branch of noninterleaving models in formal models, is adopted to describe the true concurrent trait of systems described by SystemVerilog better. And we provide a synchronous subset from SystemVerilog. The subset mainly depicts the communication between processes and the behaviors of ones, including sequence, parallel, endless performing, judge, uncertain choice, wait, and disrupt, etc. Then we present the EBES based denotational semantics of the subset, which is described in the process-algebra format, and definition about the result after process performing and system's status. Our aim is providing a precise, unambiguous semantics for SystemVerilog in order to avoid logic mistakes in hardware designs.