Automated Hardware Implementation of Computer Communication Protocols Using Petri Net Based Methods

Although formal methods have been developed for the analysis and synthesis of communication protocols, they have only been applied at the software level. With advances in VLSI and transmission technologies, it is expected that the software implementation of these protocols will eventually be replaced by specialised VLSI circuits in order to achieve the high end-to-end throughput and reliability required for future computer communication protocols. In order to ensure the conformance of these VLSI circuits to their specifications, formal methods should also be applied to hardware development. In this paper, we present a formal method called Hardware Petri Nets (H-nets) which can be used to assist in the design and implementation of reliable protocols in hardware. The concepts of hierarchical and modularized modelling structures are introduced in H-nets to enable direct mapping of a model into hardware. Furthermore, in order to meet the growing demand for faster and more reliable networks, a design environment which can automate the process from specification and verification to the implementation of the communication protocols is necessary. The way in which H-nets are employed in such a protocol design system is described in this paper.