PAFSV: A process algebraic framework for SystemVerilog

We develop a process algebraic framework, called process algebraic framework for IEEE 1800trade SystemVerilog (PAFSV), for formal specification and analysis of IEEE 1800trade 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 1800trade SystemVerilog. To show that PAFSV is useful for the formal specification and analysis of IEEE 1800trade SystemVerilog designs, we illustrate the use of PAFSV with some examples: a MUX, a synchronous reset D flip-flop and an arbiter.