In: Jensen, K.: Lecture Notes in Computer Science, Vol. 616; 13th International Conference on Application and Theory of Petri Nets 1992, Sheffield, UK, pages 205-223. Springer-Verlag, June 1992.
Abstract: The asynchronous access of a group of users (e.g. processors) to a single resource (e.g. bus) is regulated by a cascade of arbiters. A single arbiter dircuit handles two users. The cascade permits any number of users to be serviced. We use a hierarchical Colored Petri Net to describe the arbiter circuit and the protocol for using it. We also describe the layout of a 2d input cascade of (2d-1) arbiters, d being the depth of the cascade. We verify the proper functioning of the cascade, first for depth d=1 using an occurrence graph analyzer to prove crucial invariants and conformance to the protocol; then for arbitrary depth using mathematical induction. As an alternative proof, we develop equivalent Petri net substitutes for the building blocks of the design and verify the resultant special net using classical net theoretic methods. Based on the verification we propose a change of the arbiter to speed-up the cascade.