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 { pause; // 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; } } }