MicroTESK

h1. MMU Description

_~By Alexander Kamkin, Taya Sergeeva, and Andrei Tatarnikov~_

{{toc}}

A _memory management unit_ (_MMU_) is known to be one of the most complex and error-prone components of a modern microprocessor. MicroTESK has a special subsystem, called _MMU subsystem_, intended for (1) specifying memory devices and (2) deriving testing knowledge from such specifications. The subsystem provides unified facilities for describing memory buffers (like _L1_ and _L2 caches_, _translation look-aside buffers_ (_TLBs_), etc.) as well as a means for connecting several buffers into a memory hierarchy.

h2. Grammar

<pre>

startRule

    : declaration* EOF!

    ;

declaration

    : address

    | segment

    | buffer

    | mmu

    ;

</pre>

The expression syntax is derived from nML/Sim-nML (see [[Sim-nML Language Reference]]).

h2. Address Description (address)

A buffer is accessed by an _address_, which is typically a _bit vector_ of a fixed length (width). Different buffers are allowed to have a common address space (e.g., L1 and L2 are usually both addressed by physical addresses). However, in general case, each buffer has its own domain.

An address space is described using a keyword @address@. The description includes the address type _identifier_ and the address _width_. The latter is specified in brackets. Its value should be non-negative (zero-length addresses are permitted).

h3. Grammar

<pre>

address

    : ''address'' addressTypeID ''('' expr '')''

    ;

</pre>

h3. Examples

<pre>// A 64-bit virtual address (VA).

address VA(64)</pre>

<pre>// A 36-bit physical address (PA).

address PA(36)</pre>

h2. Address Space Segment Description (segment)

An address space segment is specified using the @segment@ keyword. A segment is associated with a specific address type. It is possible to specify any number (≥ 0) of segments (with different names) for one address type. Each segment is characterized by its _identifier_ and _address range_. Different segments should have different names, but address ranges are allowed to overlap, and moreover, to be the same.

h3. Grammar

<pre>

segment

    : ''segment'' segmentID ''('' argumentID '':'' addressTypeID '')''

        ''range'' ''='' ''('' expr '','' expr '')''

    ;

</pre>

h3. Examples

<pre>

segment USEG (va: VA)

  range = (0x0000000000000000, 0x000000007fffffff)

</pre>

h2. Buffer Description (buffer)

A buffer is described using a keyword @buffer@. The description specifies a set of parameters, including @ways@, @sets@, @entry@, @index@, @match@ and @policy@. All of the parameters except @index@ (if @sets = 1@) and @policy@ are obligatory.

h3. Grammar

<pre>

buffer

    : ''buffer'' bufferTypeID ''('' addressArgID '':'' addressTypeID '')''

        (bufferParameter)*

    ;

bufferParameter

    : ways

    | sets

    | entry

    | index

    | match

    | policy

    ;

</pre>

h3. Buffer Associativity (ways)

The @ways@ parameter specifies the buffer _associativity_ (the number of lines in a set). The parameter is obligatory; its value should be positive.

h4. Grammar

<pre>

ways

    : ''ways'' ''='' expr

    ;

</pre>

h3. Buffer Length (sets)

The @sets@ parameter specifies the buffer _length_ (the number of sets a cache). The parameter is obligatory; its value should be positive.

h4. Grammar

<pre>

sets

    : ''sets'' ''='' expr

    ;

</pre>

h3. Buffer Line Format (entry)

The @entry@ parameter specifies the buffer _line format_ (a number of named fields). A field has three attributes: a name, a width and, optionally, an initial value.

h4. Grammar

<pre>

format

    : ''entry'' ''='' ''('' field ('','' field)* '')''

    ;

field

    : fieldID '':'' expr (''='' expr)?

    ;

</pre>

h3. Buffer Index Function (index)

The @index@ parameter specifies the _address-to-index function_, which maps an address into the set index. The function may be omitted if the number of sets is @1@.

h4. Grammar

<pre>

index

    : ''index'' ''='' expr

    ;

</pre>

h3. Buffer Match Predicate (match)

The @match@ parameter specifies the _address-line match predicate_, which checks if an address matches a line. The parameter is obligatory.

h4. Grammar

<pre>

index

    : ''match'' ''='' expr

    ;

</pre>

h3. Buffer Data Replacement Policy (policy)

The @policy@ parameters specifies the _data replacement_ (_eviction_) _policy_. The parameter is optional. The list of supported policies includes: @RANDOM@, @FIFO@, @PLRU@ and @LRU@.

h4. Grammar

<pre>

policy

    : ''policy'' ''='' policyID

    ;

</pre>

h3. Examples

<pre>

// A 4-way set associative cache (L1) addressed by physical addresses (PA).

buffer L1(addr: PA)

  // The cache associativity.

  ways = 4

  // The number of sets.

  sets = 128

  // The line format.

  entry = (

    V    : 1 = 0, // The validity flag (by default, the line is invalid).

    TAG  : 24,    // The tag (the <35..12> address bits).

    DATA : 256    // The data (4 double words).

  )

  // The address-to-index function (example: using address fields).

  index = addr.INDEX

  // The address-line predicate (example: using address bits).

  match = addr<35..12> == TAG

  // The data replacement policy (example: using predefined policy LRU - Least Recently Used).

  policy = LRU

</pre>

h2. MMU Description (mmu)

Memory management unit logic is described using the @mmu@ keyword. The description includes two obligatory parameters @read@ and @write@ that describe the semantics of memory read and memory write actions respectively.

h3. Grammar

<pre>

mmu

    : ''mmu'' memoryTypeID ''('' addressArgID '':'' addressTypeID '')'' = dataArgID

        (mmuVariable)*

        (mmuParameter)*

    ;

mmuVariable

    : ''var'' variableID '':'' variableTypeID (''.'' ''entry'')? '';''

    ;

mmuParameter

    : read

    | write

    ;

</pre>

h3. Memory Read Action (read)

The @read@ parameter specifies the _read action_, which is a sequence of statements describing how the read operation is to be performed (by means of data transfers between buffers). The parameter is obligatory.

h4. Grammar

<pre>

read

    : ''read'' ''='' ''{'' sequence ''}''

    ;

</pre>

h3. Memory Write Action (write)

The @write@ parameter specifies the _read action_, which is a sequence of statements describing how the write operation is to be performed (by means of data transfers between buffers). The parameter is obligatory.

h4. Grammar

<pre>

write

    : ''write'' ''='' ''{'' sequence ''}''

    ;

</pre>

h3. Examples

<pre>

// A memory unit addressed by virtual addresses (VA).

mmu Memory(addr: VA) = data

  // The read action.

  read = {

    // Some statements.

    ...

  }

  // The write action.

  write = {

    // Some statements.

    ...

  }

</pre>

h2. Simplified Specification of MIPS''s MMU

<pre>

//==================================================================================================

// Virtual Address (VA)

//==================================================================================================

address VA(64)

//--------------------------------------------------------------------------------------------------

// User Mode Segments

//--------------------------------------------------------------------------------------------------

segment USEG (va: VA)

  range = (0x0000000000000000, 0x000000007fffffff)

segment XUSEG(va: VA)

  range = (0x0000000080000000, 0x000000ffffffffff)

//--------------------------------------------------------------------------------------------------

// Supervisor Mode Segments

//--------------------------------------------------------------------------------------------------

segment SUSEG(va: VA)

  range = (0x0000000000000000, 0x000000007fffffff)

segment XSUSEG(va: VA)

  range = (0x0000000080000000, 0x000000ffffffffff)

segment XSSEG(va: VA)

  range = (0x4000000000000000, 0x400000ffffffffff)

segment CSSEG(va: VA)

  range = (0xffffffffc0000000, 0xffffffffdfffffff)

//--------------------------------------------------------------------------------------------------

// Kernel Mode Segments

//--------------------------------------------------------------------------------------------------

segment KUSEG (va: VA)

  range = (0x0000000000000000, 0x000000007fffffff)

segment XKUSEG (va: VA)

  range = (0x0000000080000000, 0x000000ffffffffff)

segment XKSSEG (va: VA)

  range = (0x4000000000000000, 0x400000ffffffffff)

segment XKSEG (va: VA)

  range = (0xc000000000000000, 0xc00000ff7fffffff)

segment CKSSEG (va: VA)

  range = (0xffffffffc0000000, 0xffffffffdfffffff)

segment CKSEG3(va: VA)

  range = (0xffffffffe0000000, 0xffffffffffffffff)

//==================================================================================================

// Physical Address (PA)

//==================================================================================================

address PA(36)

//==================================================================================================

// Translation Lookaside Buffer (TLB)

//==================================================================================================

buffer DTLB (va: VA)

  ways   = 4

  sets   = 1

  entry  = (ASID: 8, VPN2: 27, R: 2,               // EntryHi

            G0: 1, V0: 1, D0: 1, C0: 3, PFN0: 24,  // EntryLo0

            G1: 1, V1: 1, D1: 1, C1: 3, PFN1: 24)  // EntryLo1

  index  = 0

  match  = VPN2 == va<39..13> // ASID, G and non-4KB pages are unsupported

  policy = PLRU

buffer JTLB (va: VA)

  ways   = 64

  sets   = 1

  entry  = (ASID: 8, VPN2: 27, R: 2,               // EntryHi

            G0: 1, V0: 1, D0: 1, C0: 3, PFN0: 24,  // EntryLo0

            G1: 1, V1: 1, D1: 1, C1: 3, PFN1: 24)  // EntryLo1

  index  = 0

  match  = VPN2 == va<39..13> // ASID, G and non-4KB pages are unsupported

  policy = NONE

//==================================================================================================

// Cache Memory (L1 and L2)

//==================================================================================================

buffer L1 (pa: PA)

  ways   = 4

  sets   = 128

  entry  = (V: 1 = 0, TAG: 24, DATA: 256)

  index  = pa<11..5>

  match  = V == 1 && TAG == pa<35..12>

  policy = PLRU

buffer L2 (pa: PA)

  ways   = 4

  sets   = 4096

  entry  = (V: 1 = 0, TAG: 19, DATA: 256)

  index  = pa<16..5>

  match  = V == 1 && TAG == pa<35..17>

  policy = PLRU

//==================================================================================================

// MMU Logic (Interaction between TLB, L1 and L2)

//==================================================================================================

mmu pmem(va: VA) = (data: 64) 

  var tlbEntry: JTLB.entry;

  var l1Entry: L1.entry;

  var l2Entry: L2.entry;

  var evenOddBit: 5;

  var g: 1;

  var v: 1;

  var d: 1;

  var c: 3;

  var pfn: 24;

  var pa: PA;

  var cachePA: PA;

  var cacheData: 256;

  read = {

    // The address is unaligned.

    if va<0..2> != 0 then

      exception("AddressError");

    endif; // If the address is unaligned.

    // The default cache policy.

    c = 3;

    // The address is from the USEG segment (only USEG and KSEG segments are supported).

    if USEG(va).hit then

      // The address hits the DTLB.

      if DTLB(va).hit then

        tlbEntry = DTLB(va);

      // The address hits the JTLB.

      elif JTLB(va).hit then

        tlbEntry = JTLB(va);

      // The address does not hit the TLB.

      else

        exception("TLBRefill");

      endif; // If the address hits the DTLB.

      // Only 4KB pages are supported.

      evenOddBit = 12;

      // The VPN is even.

      if va<evenOddBit> == 0 then

        g   = tlbEntry.G0;

        v   = tlbEntry.V0;

        d   = tlbEntry.D0;

        c   = tlbEntry.C0;

        pfn = tlbEntry.PFN0;

      // The VPN is odd.

      else

        g   = tlbEntry.G1;

        v   = tlbEntry.V1;

        d   = tlbEntry.D1;

        c   = tlbEntry.C1;

        pfn = tlbEntry.PFN1;

      endif; // If the VPN is even.

      // The EntryLo is valid.

      if v == 1 then

        pa = pfn<24..(evenOddBit - 12)>::va<(evenOddBit - 1)..0>;

      // The EntryLo is invalid.

      else

        exception("TLBInvalid");

      endif; // If the EntryLo is valid.

    // The address is from the KSEG0 or KSEG1 segment.

    else

      pa = va<28..0>;

    endif; // If the address is from the USEG segment.

    // The address is cacheable.

    if c<1..0> != 2 then

      cachePA = pa;

      cachePA<4..0> = 0;

      // The address hits the L1.

      if L1(pa).hit then

        l1Entry = L1(pa);

        cacheData = l1Entry.DATA;

        data = cacheData<(8 * pa<4..0> + 63)..(8 * pa<4..0>)>;

      // The address does not hit the L1.

      else

        // The L2 cache is used.

        if c<1..0> == 3 then

          // The address hits the L2.

          if L2(pa).hit then

            l2Entry = L2(pa);

            cacheData = l2Entry.DATA;

            data = cacheData<(8 * pa<4..0> + 63)..(8 * pa<4..0>)>;

            // Fill the L1.

            l1Entry.V = 1;

            l1Entry.TAG = pa<35..12>;

            l1Entry.DATA = cacheData;

            L1(pa) = l1Entry;

          // The address does not hit the L2.

          else

            cacheData = pmem[cachePA + 24]::pmem[cachePA + 16]::pmem[cachePA + 8]::pmem[cachePA];

            data = cacheData<(8 * pa<4..0> + 63)..(8 * pa<4..0>)>;

            // Fill L2.

            l2Entry.V = 1;

            l2Entry.TAG = pa<35..17>;

            l2Entry.DATA = cacheData;

            L2(pa) = l2Entry;

            // Fill L1.

            l1Entry.V = 1;

            l1Entry.TAG = pa<35..12>;

            l1Entry.DATA = cacheData;

            L1(pa) = l1Entry;

          endif; // If the address hits the L2.

        // The L2 cache is bypassed.

        else

          cacheData = pmem[cachePA + 24]::pmem[cachePA + 16]::pmem[cachePA + 8]::pmem[cachePA];

          data = cacheData<(8 * pa<4..0> + 63)..(8 * pa<4..0>)>;

          l1Entry.V = 1;

          l1Entry.TAG = pa<35..12>;

          l1Entry.DATA = cacheData;

          L1(pa) = l1Entry;

        endif; // If the L2 cache is used.

      endif; // If the address hits the L1.

    // The address is uncacheable.

    else

      data = pmem[pa];

    endif; // If the address is cacheable.

  }

  write = {

    // The address is unaligned.

    if va<0..2> != 0 then

      exception("AddressError");

    endif; // If the address is unaligned.

    // The default cache policy.

    c = 3;

    // The address is from the USEG segment (only USEG and KSEG segments are supported).

    if USEG(va).hit then

      // The address hits the DTLB.

      if DTLB(va).hit then

        tlbEntry = DTLB(va);

      // The address hits the JTLB.

      elif JTLB(va).hit then

        tlbEntry = JTLB(va);

      // The address does not hit the TLB.

      else

        exception("TLBRefill");

      endif; // If the address hits the DTLB.

      // Only 4KB pages are supported.

      evenOddBit = 12;

      // The VPN is even.

      if va<evenOddBit> == 0 then

        g   = tlbEntry.G0;

        v   = tlbEntry.V0;

        d   = tlbEntry.D0;

        c   = tlbEntry.C0;

        pfn = tlbEntry.PFN0;

      // The VPN is odd.

      else

        g   = tlbEntry.G1;

        v   = tlbEntry.V1;

        d   = tlbEntry.D1;

        c   = tlbEntry.C1;

        pfn = tlbEntry.PFN1;

      endif; // If the VPN is even.

      // The EntryLo is valid.

      if v == 1 then

        // The EntryLo is clean.

        if d == 1 then

          pa = pfn<24..(evenOddBit - 12)>::va<(evenOddBit - 1)..0>;

        // The EntryLo is dirty.

        else

          exception("TLBModified");

        endif; // If the EntryLo is clean.

      // The EntryLo is invalid.

      else

        exception("TLBInvalid");

      endif; // If the EntryLo is valid.

    // The address is from the KSEG0 or KSEG1 segment.

    else

      pa = va<28..0>;

    endif; // If the address is from the USEG segment.

    // The address is cacheable.

    if c<1..0> != 2 then

      cachePA = pa;

      cachePA<4..0> = 0;

      // The address hits the L1.

      if L1(pa).hit then

        // Update the L1.

        l1Entry = L1(pa);

        l1Entry.DATA<(8 * pa<4..0> + 63)..(8 * pa<4..0>)> = data;

        L1(pa) = l1Entry;

        // Only the write-through policy is supported.

        pmem[pa] = data;

      // The address does not hit the L1.

      else

        // The L2 cache is used.

        if c<1..0> == 3 then

          // The address hits the L2.

          if L2(pa).hit then

            // Update the L2.

            l2Entry = L2(pa);

            l2Entry.DATA<(8 * pa<4..0> + 63)..(8 * pa<4..0>)> = data;

            L2(pa) = l2Entry;

            // Fill the L1.

            l1Entry.V = 1;

            l1Entry.TAG = pa<35..12>;

            l1Entry.DATA = l2Entry.DATA;

            L1(pa) = l1Entry;

            // Only the write-through policy is supported.

            pmem[pa] = data;

          // The address does not hit the L2.

          else

            pmem[pa] = data;

            cacheData = pmem[cachePA + 24]::pmem[cachePA + 16]::pmem[cachePA + 8]::pmem[cachePA];

            // Fill the L2.

            l2Entry.V = 1;

            l2Entry.TAG = pa<35..17>;

            l2Entry.DATA = cacheData;

            L2(pa) = l2Entry;

            // Fill the L1.

            l1Entry.V = 1;

            l1Entry.TAG = pa<35..12>;

            l1Entry.DATA = cacheData;

            L1(pa) = l1Entry;

          endif; // If the address hits the L2.

        // The L2 cache is bypassed.

        else

          pmem[pa] = data;

          cacheData = pmem[cachePA + 24]::pmem[cachePA + 16]::pmem[cachePA + 8]::pmem[cachePA];

          // Fill the L2

          l1Entry.V = 1;

          l1Entry.TAG = pa<35..12>;

          l1Entry.DATA = cacheData;

          L1(pa) = l1Entry;

        endif; // If the L2 cache is used.

      endif; // If the address hits the L1.

    // The address is uncacheable.

    else

      pmem[pa] = data;

    endif; // If the address is cacheable.

  }

//==================================================================================================

// The End

//==================================================================================================

</pre>