Computing and Informatics

We develop a process algebraic framework SVPA for the formal specification and analysis of IEEE 1800 mathrmTM SV designs. The formal semantics of SVPA is defined by means of deduction rules that associate a time transition system with a SVPA process. A set of properties of SVPA is presented for a notion of bisimilarity. SVPA may be regarded as the formal language of a significant subset of IEEE 1800 mathrmTM SV. To show that SVPA is useful for the formal specification and analysis of IEEE 1800 mathrmTM SV designs, we illustrate the use of SVPA with a multiplexer, a synchronous reset D flip-flop and an arbiter.