// this module tests the MESI protocol with CPUs, an arbiter and a main memory together

macro NumProcs  = 2;         // number of processors

macro DataWidth   =  8;     // bit-width of registers, i.e. data words
macro ByteSize    = 256;    // nat{ByteSize} is the data type used for bytes
// macro WordSize    = 1;      // the number of bytes within a word
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 NumOfSets   =  2;     // set associativity

// 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

// three abstract instructions
macro NumInstr = 3;        // number of instructions
macro NT = 0;              // do nothing
macro RD = 1;              // read instruction
macro WT = 2;              // write instruction

module Compose(
    //nat{NumInstr} ?instr0,                        // instruction to be performed by cpu0
    //nat{MemSize} ?address0,
    //nat{ByteSize} ?data0,
    //bv{DataWidth} ?data0,
    bv{16} ?instr0,
    nat pc0,  
    //nat{NumInstr} ?instr1,                        // instruction to be performed by cpu1
    //nat{MemSize} ?address1,
    //nat{ByteSize} ?data1,
    //bv{DataWidth} ?data1,
    bv{16} ?instr1,
    nat pc1, 
    ){
    event nat{NumProcs} pidOut;                      // the processor index broadcasted.
    event [NumProcs]bool reqCache;                 // signals handling CPU requests
    event [NumProcs]bool ackCache;
    event [NumProcs]bool doneCache;               
    event [NumProcs]bool reqCacheBus; 
    event [NumProcs]bool ackCacheBus;              // signals handling bus requests
    event bool reqMemBus;
    event bool ackMemBus;
    nat{3} stateMem;                                 // state of the memory
    //event [NumProcs]nat{MemSize}  adrCPU;            // address request reading from CPU to cache
    event [NumProcs]nat adrCPU;            // address request reading from CPU to cache
    // event [NumProcs]nat{ByteSize} dataCPU;        // data request writing from CPU to cache
    event [NumProcs]bv{DataWidth} dataCPU;           // data request writing from CPU to cache
    //event nat{MemSize} adrMem;                       // address bus
    event nat adrMem;                       // address bus
    // event [LineSize]nat{ByteSize} dataMem;        // data bus
    event [LineSize]bv{DataWidth} dataMem;           // data bus
    event bool snoop;                               // signal indicating an active snoop
    event [NumProcs]bool readCPU;                   // signal indicating CPU requires a read of cache
    event [NumProcs]bool writeCPU;                  // signal indicating CPU requires a write of cache
    event bool readMem, writeMem;                   // bus signals indicating read / write requirements
    event nat{3} BusMsgOut;                         // bus signals for messages
    event nat{4} BusMsgIn;
    
    cpu0: // RdWtCPU(        instr0, address0, data0, pc0,        adrCPU[0], dataCPU[0],       readCPU[0],writeCPU[0],              reqCache[0],ackCache[0],doneCache[0]      );
        SingleCycleScalarBehav (
          instr0,                   // instruction to be performed now    
          pc0,                      // program counter
          adrCPU[0],                // address for memory access
          dataCPU[0],               // data for memory access 
          readCPU[0],writeCPU[0],                 // whether data is read or written to memory
          reqCache[0],ackCache[0],doneCache[0]    // signals for memory transaction
        );
    ||
    cache0: CacheMESI(
       0,
       pidOut,
       reqCache[0], ackCache[0], doneCache[0],
       reqCacheBus[0], ackCacheBus[0],
       stateMem,
       adrCPU[0],
       dataCPU[0],
       adrMem,
       dataMem,
       snoop,
       readCPU[0], writeCPU[0],
       readMem, writeMem,
       BusMsgOut, 
       BusMsgIn
    );
    ||    
    cpu1:
        SingleCycleScalarBehav (
          instr1,                   // instruction to be performed now    
          pc1,                      // program counter
          adrCPU[1],                // address for memory access
          dataCPU[1],               // data for memory access 
          readCPU[1],writeCPU[1],                 // whether data is read or written to memory
          reqCache[1],ackCache[1],doneCache[1]    // signals for memory transaction
        );
    ||
    cache1: CacheMESI(
       1,
       pidOut,
       reqCache[1], ackCache[1], doneCache[1],
       reqCacheBus[1], ackCacheBus[1],
       stateMem,
       adrCPU[1],
       dataCPU[1],
       adrMem,
       dataMem,
       snoop,
       readCPU[1], writeCPU[1],
       readMem, writeMem,
       BusMsgOut, 
       BusMsgIn
    ); 
    ||
    BusArbiter(reqCacheBus, ackCacheBus,
                  reqMemBus, ackMemBus);
    ||
    MainMemory(
       reqMemBus, ackMemBus, 
       adrMem, dataMem,
       readMem, writeMem, stateMem,
       snoop
       );
                  
}