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