In: Lecture Notes in Computer Science, Vol. 1091; Proc. 17th International Conference in Application and Theory of Petri Nets (ICATPN'96), Osaka, Japan, pages 93-112. Springer-Verlag, June 1996.
Abstract: In this paper the application of Petri nets to high level synthesis of synchronous parallel controllers is presented. A formal specification of a design is given in a form of an interpreted synchronous Petri net. Behavioral properties of the controller are verified using symbolic traversal of its Petri net model. The net state-space explosion problem is managed using binary decision diagrams (BDDs). Once the Petri net specification of a controller is tested, the BDD representation of the net's state-space is used to generate a state assignment with which the controller can be synthesized. The application of the proposed methodology to the design of a MAXbus port controller for a high performance Transputer Framestore and its comparison to the alternative implementation is discussed. The experimental results clearly demonstrate the advantages of the proposed method. Further, the significant increase of the applicability of this approach has also been achieved.