O'Reilly logo

Verification of Systems and Circuits Using LOTOS, Petri Nets, and CCS by Rakefet Kol, Michael Yoeli

Stay ahead with the world's most comprehensive technology and business learning platform.

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, tutorials, and more.

Start Free Trial

No credit card required

CHAPTER 9

Verification of Arbiters

9.1 INTRODUCTION

An arbiter circuit controls the exclusive access of one out of a number of possibly competing processes to a shared resource.

There are a number of possible algorithms for choosing the process that gets access to the resource in case of two or more competing processes. Here we only list a few examples and in Section 9.5 we provide relevant references for further study:

  • random arbiter—the selection is done at random
  • token-ring arbiter—the selection is done in a fixed cyclic order
  • priority arbiter—the selection is done according to fixed or changing priorities assigned to the processes in question

We expect an arbiter circuit to satisfy the following requirements:

(1) Mutual Exclusion: only one process may have access to the shared resource

(2) Grant Only on Request

(3) Fairness: any request by a process is eventually granted

9.2 A RANDOM ARBITER (RGDA)

We consider a circuit that has one binary incoming line INj from each process #j, and one binary outgoing line OUTj to each process #j, as described in Fig. 9.1. The rising-transition of INj is denoted Rj (request), its falling-transition is denoted Dj (done). Similarly, the rise- and fall-transitions of OUTj are denoted Gj (grant) and Aj (acknowledge), respectively. The various line changes (as can be seen in Fig. 9.1) are interpreted as follows:

images

Figure 9.1 Random RGDA arbiter ...

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, interactive tutorials, and more.

Start Free Trial

No credit card required