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