MicroTESK

Например,

Situation                                
{
    if (TLB(VA) = hit)
    {
        load TLB.Line:PNF;
    }
    then 
        AddTrans(VA:data,PA)                // address translation function: from VA to PA
        {
            PA = PNF::VA<6..1>;
        }   

        if(L1(PA) = hit) 
        {
            LoadMemory (L1.Line), word;                        // loading operation
        }        

        then
            StoreMemory (register := word);                   // writing operation

        else                                                  // L1 = miss
        {
            if(L2(PA) = hit)
            {
                LoadMemory (L2.Line), word;
            }
            then
                StoreMemory (register := word);

            else                            // L2 = miss
            {
                throw L2Missexception();
            }
            endif

        throw L1Missexception();
        }

    else                                     // TLB(VA) = miss
    {
        throw new MissException();
    }
}

Функция трансляции адреса:

op AddTrans           
{
    PA = VA:data;            // Data translation from VirtAddr into PhysAddr 
}

Если оценивать количественно, то соответствие около 5%. Список несоответствий буду составлять завтра. Их будет много, почти к каждой строке кода есть вопросы.

Лучше вместо переменной типа XXXAction сделать несколько атрибутов в операции XXX.

Например,

TLBAction = LOAD_ACT;
TLB.action;

лучше заменить на

TLB.load

Код, приведенный ниже, непонятен. Если нет попадания в TLB, просто генерируется прерывание (в MIPS оно называется TLBMiss). Если есть попадание, но бит V=0, генерируется прерывание TLBInvalid.

    ...
    else
       /// search in page table
       pa = va;
    endif;

Как связаны TLB и TLBFakeOp ?

type word = card(32)
type hit = card(2)

type va_t = card(32)
type pa_t = card(32)
//type mem_t = card(1024)

var va[1, va_t]
var pa[1, pa_t]
var data[1, word]

var TLB_Hit[1, hit]
var L1_Hit[1, hit]
var L2_Hit[1, hit]
var OP_MEM_Hit[1, hit]

op TLB_access(pa)
action = 
{
    TLB_Hit;   
}

op L1_access(pa)
action = 
{
    L1_Hit;
}

op L2_access(pa)
action = 
{
    L2_Hit; 
}

op OP_MEM_access(pa)
action = 
{
    OP_MEM_Hit;
}

op address_conv(pa)
action = 
{
    pa = va;
}

op LOAD(pa : pa_t, data : word)
action = 
{
    TLB_access.action(pa);
        if TLB_Hit then
            L1_access.action;
            if L1_Hit then
               address_conv.action;
            else
                L2_access.action;
                if L2_Hit then
                  address_conv.action;
                else
                    OP_MEM_access.action(pa);
                    address_conv.action;
                    // if miss - search the data in operation memory
                endif;
            endif;
        else
            TLB_exception; 
        endif;
}

op STORE(pa : pa_t, data : word)
action = 
{
    L1_access.action
    if L1_Hit then
        L2_access.action
        if L2_Hit then
            OP_MEM.store(pa, data)
        else
            L2.store(pa, data)
            OP_MEM.store(pa, data)
        endif;
    else
        L1.store(pa, data)
        L2.store(pa, data)
        OP_MEM.store(pa, data)
    endif;
  }