Actions

History

MMU Description¶

_{By Alexander Kamkin, Taya Sergeeva, and Andrei Tatarnikov}

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.

Grammar¶

startRule
    : declaration* EOF!
    ;

declaration
    : address
    | segment
    | buffer
    | mmu
    ;

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

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).

Grammar¶

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

Examples¶

// A 64-bit virtual address (VA).
address VA(64)

// A 36-bit physical address (PA).
address PA(36)

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.

Grammar¶

segment
    : 'segment' segmentID '(' argumentID ':' addressTypeID ')'
        'range' '=' '(' expr ',' expr ')'
    ;

Examples¶

segment USEG (va: VA)
  range = (0x0000000000000000, 0x000000007fffffff)

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.

Grammar¶

buffer
    : 'buffer' bufferTypeID '(' addressArgID ':' addressTypeID ')'
        (bufferParameter)*
    ;

bufferParameter
    : ways
    | sets
    | entry
    | index
    | match
    | policy
    ;

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.

Grammar¶

ways
    : 'ways' '=' expr
    ;

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.

Grammar¶

sets
    : 'sets' '=' expr
    ;

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.

Grammar¶

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

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

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.

Grammar¶

index
    : 'index' '=' expr
    ;

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.

Grammar¶

index
    : 'match' '=' expr
    ;

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.

Grammar¶

policy
    : 'policy' '=' policyID
    ;

Examples¶

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

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.

Grammar¶

mmu
    : 'mmu' memoryTypeID '(' addressArgID ':' addressTypeID ')' = dataArgID
        (mmuVariable)*
        (mmuParameter)*
    ;

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

mmuParameter
    : read
    | write
    ;

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.

Grammar¶

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

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.

Grammar¶

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

Examples¶

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

Simplified Specification of MIPS's MMU¶

//==================================================================================================
// 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
//==================================================================================================

Files (0)

Updated by Alexander Kamkin over 9 years ago · 132 revisions

Project

General

Profile

MicroTESK

Wiki

MMU Description¶

Grammar¶

Address Description (address)¶

Grammar¶

Examples¶

Address Space Segment Description (segment)¶

Grammar¶

Examples¶

Buffer Description (buffer)¶

Grammar¶

Buffer Associativity (ways)¶

Grammar¶

Buffer Length (sets)¶

Grammar¶

Buffer Line Format (entry)¶

Grammar¶

Buffer Index Function (index)¶

Grammar¶

Buffer Match Predicate (match)¶

Grammar¶

Buffer Data Replacement Policy (policy)¶

Grammar¶

Examples¶

MMU Description (mmu)¶

Grammar¶

Memory Read Action (read)¶

Grammar¶

Memory Write Action (write)¶

Grammar¶

Examples¶

Simplified Specification of MIPS's MMU¶