We develop a process algebraic framework, called process algebraic framework for IEEE 1800™ SystemVerilog (PAFSV), for formal specification and analysis of IEEE 1800™ SystemVerilog designs. The formal semantics of PAFSV is defined by means of deduction rules that associate a time transition system with a PAFSV process. A set of properties of PAFSV is presented for a notion of bisimilarity. PAFSV may be regarded as the formal language of a significant subset of IEEE 1800™ SystemVerilog. To show that PAFSV is useful for the formal specification and analysis of IEEE 1800™ SystemVerilog designs, we illustrate the use of PAFSV with some examples: a MUX, a synchronous reset D flip-flop and an arbiter.
展开▼
