// ************************************************************************** //
//                                                                            //
//    eses                   eses                                             //
//   eses                     eses                                            //
//  eses    eseses  esesese    eses   Embedded Systems Group                  //
//  ese    ese  ese ese         ese                                           //
//  ese    eseseses eseseses    ese   Department of Computer Science          //
//  eses   eses          ese   eses                                           //
//   eses   eseses  eseseses  eses    University of Kaiserslautern            //
//    eses                   eses                                             //
//                                                                            //
// ************************************************************************** //

// ----------------------------------------------------------------------------
// opcodes of the instructions
// ----------------------------------------------------------------------------

macro ADD   = 0b000000;
macro ADDU  = 0b000001;
macro ADDI  = 0b000010;
macro ADDIU = 0b000011;
macro SUB   = 0b000100;
macro SUBU  = 0b000101;
macro SUBI  = 0b000110;
macro SUBIU = 0b000111;
macro MUL   = 0b001000;
macro MULU  = 0b001001;
macro MULI  = 0b001010;
macro MULIU = 0b001011;
macro DIV   = 0b001100;
macro DIVU  = 0b001101;
macro DIVI  = 0b001110;
macro DIVIU = 0b001111;

macro SLT   = 0b010000;
macro SLTU  = 0b010001;
macro SLE   = 0b010010;
macro SLEU  = 0b010011;
macro SEQ   = 0b010100;
macro SNE   = 0b010101;

macro AND   = 0b010110;
macro OR    = 0b010111;
macro NAND  = 0b011000;
macro NOR   = 0b011001;

macro LD    = 0b011010;
macro ST    = 0b011011;
macro LVWS  = 0b011100;
macro SVWS  = 0b011101;
macro LL    = 0b011110;
macro SC    = 0b011111;
macro MOV   = 0b100000;
macro MOVU  = 0b100001;

macro BEZ   = 0b100010;
macro BNZ   = 0b100011;
macro JMP   = 0b100100;
macro J     = 0b100101;

macro SYNC  = 0b100111; // note that this group of instructions share the same
macro OVF   = 0b100111; // opcode, and differ in the additional function code
macro MVTM  = 0b100111; // listed below
macro MVFM  = 0b100111;
macro MVTL  = 0b100111;
macro MVFL  = 0b100111;

macro fn_SYNC  = 0b0000000;
macro fn_OVF   = 0b0000001;
macro fn_MVTM  = 0b0000010;
macro fn_MVFM  = 0b0000011;
macro fn_MVTL  = 0b0000100;
macro fn_MVFL  = 0b0000101;


// --------------------------------------------------------------------------
// special macros
// --------------------------------------------------------------------------
macro DataWidth     =  8;                         // bit-width of registers
macro UpperWord(r)  = r{2*DataWidth-1:DataWidth}; // upper half of double word
macro LowerWord(r)  = r{DataWidth-1:0};           // lower half of double word



// --------------------------------------------------------------------------
// write back stage of the structural implementation
// --------------------------------------------------------------------------

module WriteBack(
    nat pc,                         // program counter
    bv{6} ?opc,                     // opcode of instr
    bv{7} ?fnc,                     // constant operand of S-type instructions
    bv{10} ?adr,                    // jump address of J-type instruction
    nat{8} ?rd,                     // register destination
    bv{2*DataWidth} ?AluRes,        // ALU result (contains memory address)
    bv{DataWidth} ?LoadRes,         // Load result
    bool ?CondRes,                  // result of branch condition
    [8]bv{DataWidth} !Reg,          // scalar registers
    bv{DataWidth} !overflw          // overflw register (completing result)
) {
        case
            // ----------------------------------------------------------------
            // instructions writing to Reg[rd]
            // ----------------------------------------------------------------
            (bv2nat(opc)<=bv2nat(0b011001)
              | opc==MOV | opc==MOVU | opc==OVF & fnc==fn_OVF) do {
                next(overflw) = UpperWord(AluRes);
                if(rd!=0)
                    next(Reg[rd]) = LowerWord(AluRes);
                next(pc) = pc+1;
                }
            // ----------------------------------------------------------------
            // load and store instructions
            // ----------------------------------------------------------------
            (opc==LD | opc==LL | opc==ST | opc==SC | opc==SYNC & fnc==fn_SYNC) do {
                if(rd!=0)
                    next(Reg[rd]) = LoadRes;
                next(pc) = pc+1;
                }
            // ----------------------------------------------------------------
            // branch and jump instructions
            // ----------------------------------------------------------------
            (opc==BEZ | opc==BNZ) do
                next(pc) = (CondRes ? pc+bv2int(AluRes) : pc+1);
            (opc==JMP) do 
                next(pc) = pc + bv2int(AluRes);
            (opc==J) do 
                next(pc) = pc + bv2int(adr);
            // ----------------------------------------------------------------
        default nothing;
}