// ================================================================ // This file implements an arbiter that handles requests of N // components that want to access a shared resource for one point // of time. The arbiter is fair and guarantees mutually exclusive // access to the shared resource for one point of time. // The arbiter makes use of a round robin schema (daisy chain), // i.e., a token is passed around in a ring of N FlipFlops (token[i]). // At each point of time, only the component with the token can have // access to the shared ressource. // ================================================================ package Communication.MutexProtocols.RoundRobin; macro NumProc = 6; module RoundRobinArbiter([NumProc()] bool ?req, !ack) { [NumProc()] bool token; token[0] = true; loop { next(token[0]) = token[(NumProc()-1)]; ack[0] = req[0] & token[0] ; for(i=1 .. (NumProc()-1)) { next(token[i]) = token[i-1]; ack[i] = req[i] & token[i] ; } pause; } }satisfies { // ============================================================ MutualExclusive: // ------------------------------------------------------------ // at most one process is given an acknowledge // ------------------------------------------------------------ assert A G forall(i=0 .. (NumProc()-2)) forall(j=i+1 .. (NumProc()-1)) (ack[i] -> !ack[j]); // ============================================================ AcknowledgeOnlyByRequest: // ------------------------------------------------------------ // acknowledge is only given if component requests for access // ------------------------------------------------------------ assert A G forall(i=0 .. (NumProc()-1)) (ack[i] -> req[i]); // ============================================================ Fairness: // ------------------------------------------------------------ // at most one process is given an acknowledge // ------------------------------------------------------------ assert forall(i=0 .. (NumProc()-1)) !E F E G (req[i] & !ack[i]); // ============================================================ }