Towards a theory of bisimulation for a fragment of Verilog

In this paper, we have developed an operational semantic framework for a non-trival subset of Verilog which features event-driven computation and shared variable concurrency. The bisimulation equivalence is introduced to identify programs of the same behavior. And the bisimulation can be proved to be a congruence for all Verilog operators, so it provides a sound base for deriving the algebraic laws for parallel Verilog processes.