// ================================================================ // 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. // To guarantee fairness, the arbiter makes use of a daisy chain, // i.e., a token is passed around in a ring of N FlipFlops (token[i]). // If a component requests access to the shared resource, and has // currently the token, then its persistence flag persreq[i] is set. // If the component still requests access to the shared resource // when the token comes back, then this component will definitely // receive an acknowledge signal ack[i]. // If the component with the token does not have already set its // persistence flag, then the arbiter makes use of static priorities: // component 0 has highest and component (NumProc-1) has lowest priority. // ================================================================ package Communication.MutexProtocols.DMA_Arbiter; macro NumProc = 5; module DMA_Arbiter([NumProc()] bool ?req, ack) { [NumProc()] bool token, persreq; bool static; nat j; token[0] = true; loop { // ---------------------------------------------------- // use static priorities if that component that currently // has the token has no outstanding persistent request // ---------------------------------------------------- static = !exists(i=1 .. (NumProc()-1)) (persreq[i] & token[i]); next(persreq[0]) = req[0] & (persreq[0] | token[0]); next(token[0]) = token[(NumProc()-1)]; ack[0] = req[0] & persreq[0] & token[0] | static & req[0]; for(i=1 .. (NumProc()-1)) { next(persreq[i]) = req[i] & (persreq[i] | token[i]); next(token[i]) = token[i-1]; ack[i] = req[i] & persreq[i] & token[i] | static & req[i] & (forall(j=0 .. (i-1)) !req[j]); } 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]); // ============================================================ }