// the module MainMemory implements the shared memory of a multi-processor architecture.
// In a multi-processor architecture, the main memory is accessed for read / write when
// there is a cache miss in any of the CPU's cache. It snoops the bus and waits for the
// read / write signal, and if there is such a signal, the memory starts to work correspondingly.
//
// A memory transaction usually takes much longer than a cache access. During the transaction,
// the memory is not available for the CPUs. That's why when a CPU trying to get access
// to the memory, it always have to check for the availability of the memory first, 
// right after the CPU got access to the bus. If the memory is working, then the CPU has to
// give up the bus and retry to access the bus next cycle, and see if the memory is free.
// This somehow awkward situation reflects the inefficiency of memory access in a multi-
// processor environment.
//
// Another issue is when the memory finished its work, it must compete for the bus again
// to send the data back to the CPU who needs it. This holds for both read and write operations.
// For read, the reason is clear, as some CPU is waiting for the memory's data.
// For write, it is still reasonable to write data back to bus because some other CPU might
// happened to require that data just during the time when memory's writing.
//
// The shared Memory has three states: Free, Working and Done
// Free:    the memory is not working and the bus has no valid data from the memory.
// Working: the memory is reading or writing something. This usually takes much longer time.
// Done:    the memory has finished reading / writing, and gets access to the bus and puts the
//          valid data on to the bus, so that the CPU waiting can be noticed and start reading.

macro NumProcs   = 2;      // number of processors

macro DataWidth   =  8;     // bit-width of registers, i.e. data words
macro MemSize     = 10;     // size of main memory in words, i.e. bv{DataWidth}
macro NumOfLines  =  2;     // number of cache lines
macro LineSize    =  2;     // size of cache lines in words, i.e. bv{DataWidth}
macro SetAssoc    =  2;     // set associativity

macro DivUp(n,m) = ((n-1)/m)+1; // compute n/m, but round towards infinity
macro CacheSize  = NumOfLines * SetAssoc * LineSize;
macro LinesInMem = DivUp(MemSize,LineSize);
macro TagSize    = DivUp(LinesInMem,NumOfLines);
macro LineIdRng  = MemSize % NumOfLines;

macro ReadDelay  = 2;      // delay for reading from the memory
macro WriteDelay = 3;      // delay for writing to the memory

// states of the memory
macro MemBusy    = 0;      // memory is busy working
macro MemFree    = 1;      // memory is free
macro MemDone    = 2;      // memory has finished working and loads the bus with valid data

// inputs:
//   event bool ? ackMemBus,           the signal indicating if the memory gets access to the bus
//   event ?readMem,?writeMem,         signals indicating a read / write request for the memory
// outputs:
//   event bool ! reqMemBus,           the signal indicating a requirement to access the bus
//   nat{3} !stateMem,                 the variable indicating the state of the memory
// inouts:
//   event nat{MemSize} adrMem,                 the address of the line to be read / written
//   event [LineSize]bv{DataWidth} dataMem,     the line to be read / written
module MainMemory(
       event bool ! reqMemBus, ? ackMemBus, 
       //event nat{MemSize} adrMem,
       event nat adrMem,
       // event [LineSize]nat{256} dataMem,
       event [LineSize]bv{DataWidth} dataMem,
       event ?readMem,?writeMem,
       nat{3} !stateMem,
       event ?snoop
       ){

       // memory
       // [MemSize]nat{256} memory;
       [MemSize]bv{DataWidth} memory;
       
       // local stores for the address and data on the bus
       nat{MemSize}  adrMemLoc;
       // [LineSize]nat{256} dataMemLoc;
       [LineSize]bv{DataWidth} dataMemLoc;
       // address of the word in the requested line
       nat{LineSize} adrInL;
       nat{MemSize/LineSize} adrLine;
       
       loop {
           // initially the memory is free
           stateMem = MemFree;
       
           // snoops the bus to see if there is anyone demanding a read / write?
           memwait: immediate await(readMem | writeMem);

           // change the memory state to busy
           next(stateMem) = MemBusy;
               
           if(readMem) { // perform read operation
               adrMemLoc = adrMem; // store the address from the bus
               adrLine = adrMem / LineSize;

               // penality for memory reads
               for(i=0..ReadDelay)
                   pause;
               // for a read access, we assign data the requested value memory[adrMemLoc]
               for(i=0..LineSize-1)
                   dataMemLoc[i] = memory[adrLine * LineSize +i];
           } else if(writeMem) { // perform write operation
               adrMemLoc = adrMem; // store the address from the bus
               adrLine = adrMem / LineSize;
               // store the input data from the bus
               // only store the word to be written
               adrInL = adrMemLoc % LineSize;
               dataMemLoc[adrInL] = dataMem[adrInL];
               // penality for memory writes
               for(i=0..WriteDelay)
                   pause;
               // for a write access, we assign memory[adrMemLoc] the provided value dataMemLoc
               memory[adrMemLoc] = dataMemLoc[adrInL];
           } else pause; //!! this is necessary, or there will be causality confliction on reqMemBus.
           // make room for (readMem & writeMem), which might have the meaning of flush.
           
           // once finished reading / writing, try to put data back onto the bus
           // have to wait for the snoopings
           suspend{
               emit(reqMemBus);
               while(!ackMemBus){ pause; emit(reqMemBus); }
           }when(snoop);
           // once get the bus, set memory state to Done
           stateMem = MemDone;
		   // put the address and data onto the bus
           adrMem = adrMemLoc;
		   for(i=0..LineSize-1)
               dataMem[i] = memory[adrLine * LineSize + i];

           // release the bus
           pause;
       } // end of loop
} // end of module