// ================================================================
// 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]);
   // ============================================================
}