Name
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 circuit 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, d1 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 confonmance 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. |
Year | DOI | Venue |
|---|---|---|
1992 | 10.1007/3-540-55676-1_12 | Application and Theory of Petri Nets |
Keywords | Field | DocType |
arbiter cascade,formal verification,petri net | Asynchronous communication,Discrete mathematics,Arbiter,Petri net,Computer science,Mathematical induction,Stochastic Petri net,Cascade,Mutual exclusion,Distributed computing,Formal verification | Conference |
Volume | ISSN | ISBN |
616 | 0302-9743 | 3-540-55676-1 |
Citations | PageRank | References |
14 | 6.42 | 3 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Hartmann J. Genrich | 1 | 339 | 162.18 |
| Robert M. Shapiro | 2 | 211 | 63.64 |