package MESI3;

// Module BusArbiter implements the bus arbiter.
// In a multi-processor architecture with one unique bus connecting all CPUs as well as
// the main memory together, the bus is in charge of the communications between CPUs 
// as well as communications between a CPU and the main memory. when more than one 
// CPUS / memory applying for the bus, the bus always gives right to the memory first,
// as the only case that a memory needs a bus is to return the value needed by some CPU. 
// If the memory doesn't require the bus, the arbiter then gives the bus to one of the CPUs.
macro NumProcs=2;      // number of processors

// input: 
//    event [NumProcs]bool ?reqBusCPU, the require signals from CPUs for the bus access
//    event bool           ?reqBusMem, the require signal  from memory for the bus access
// output:
//    event [NumProcs]bool ackBusCPU, the acknowledges for CPUs
//    event bool           !ackBusMem, the acknowledge  for memory
module BusArbiter(event [NumProcs]bool ?reqBusCPU, ackBusCPU,
                  event bool ?reqBusMem, !ackBusMem) {
    nat{NumProcs} token;
    // by default the first CPU has the token, 
    // i.e. the right to access the bus
    token = 0;

    loop {
        // if the memory requires to write data to bus, confirm it
        if (reqBusMem) {
            ackBusMem = true;
            // and deny all CPUs' requirements
            for(i=0..NumProcs-1) {
                ackBusCPU[i] = false;
        } else { // if memory doesn't require bus access
            for(i=0..NumProcs-1) {
                ackBusCPU[(token+i)%NumProcs] = reqBusCPU[(token+i)%NumProcs] & (i==0 ? true : forall(j=0..i-1) !ackBusCPU[(token+j)%NumProcs]); 
            // pass token around
            next(token) = (token+1) % NumProcs;