// this module implements an abstracted CPU // the only instructions are read and write. macro NumProcs = 2; macro DataWidth = 8; // bit-width of registers, i.e. data words macro ByteSize = 256; // nat{ByteSize} is the data type osed for bytes 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 // 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 RdWtCPU( nat{NumInstr} ?instr, // instruction to be performed now nat{MemSize} ?address, //nat{ByteSize} ?data, bv{DataWidth} ?data, nat pc, // program counter event nat{MemSize} adrCPU, // address for memory access //event nat{ByteSize} dataCPU, // data for memory access event bv{DataWidth} dataCPU, // data for memory access event readCPU,writeCPU, // whether data is read or written to memory event reqCache, ackCache, doneCache // signals for memory transaction){ ) { loop{ // pretend to wait for an instruction pause; case (instr==RD | instr==WT) do{ // apply for memory access by emitting reqCache until // ackCache holds; may take time on multiprocessors weak immediate abort { loop { emit(reqCache); if(!ackCache) next(pc) = pc; waitMem1: pause; } } when(ackCache); // provide address and read/write request signal // until memory transaction is done weak immediate abort { loop { // adrMem = bv2nat(Reg[rs1]) + bv2nat(cst); // assume the adr is given by the module's parameter adrCPU // assume the data is given by dataCPU whence WT adrCPU=address; case (instr==RD) do emit(readCPU); (instr==WT) do {emit(writeCPU); dataCPU=data;} default nothing; if(!doneCache) next(pc) = pc; waitMem2: pause; } } when(doneCache); // in case of load, store the data in the register // if(opc==LD | opc==LL) // next(Reg[rd]) = dataMem; } default nothing; next(pc) = pc+1; }// end of loop } drivenby TestWT{ pause; instr=WT; address=3; data=0b00001010; pc=0; ackCache=true; pause; doneCache=true; }