Verification of Systems and Circuits Using LOTOS, Petri Nets, and CCS

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:

Figure 9.1 Random RGDA arbiter ...