Карты памяти

Вы узнаете

Как объявляется карта памяти, что значат BRAM и ROM как типы и что проверяют 15 нативных тестов.

Попробовать

В записи посчитайте проходящие тесты и доказанные инварианты; затем в спеке найдите значения MemKind и три теста make_bram.

specs/fpga/memory.t27

// SPDX-License-Identifier: Apache-2.0
// t27/specs/fpga/memory.t27
// Memory (BRAM/DRAM/ROM) Abstraction for Trinity T27 FPGA HIR
// Defines block memory primitives with read/write ports
// Uses flat arrays + count fields (parser-compatible, no Vec/generics)
// phi^2 + 1/phi^2 = 3 | TRINITY

module Memory {

    // === Memory kind ===

    pub const MemKind = enum(i8) {
        bram = 0,
        dram = 1,
        rom = 2,
    };

    // === Port kind (read vs write vs read-write) ===

    pub const MemPortKind = enum(i8) {
        read_port = 0,
        write_port = 1,
        readwrite_port = 2,
    };

    // === Latency (combinational vs registered) ===

    pub const MemLatency = enum(i8) {
        comb_read = 0,
        reg_read = 1,
    };

    // === Memory port descriptor ===

    pub struct MemPort {
        name : &str,
        kind : i8,
        addr_width : u32,
        data_width : u32,
        latency : i8,
    }

    // === Memory block descriptor ===

    pub const MAX_MEM_PORTS : u32 = 8;

    pub struct MemDesc {
        name : &str,
        kind : i8,
        depth : u32,
        data_width : u32,
        addr_width : u32,
        ports : [8]MemPort,
        port_count : u32,
    }

    // === Constructor helpers ===

    fn empty_mem_port() -> MemPort {
        return MemPort{
            .name = "",
            .kind = 0,
            .addr_width = 0,
            .data_width = 0,
            .latency = 0,
        };
    }

    fn make_mem_port(name: &str, kind: i8, addr_width: u32, data_width: u32) -> MemPort {
        return MemPort{
            .name = name,
            .kind = kind,
            .addr_width = addr_width,
            .data_width = data_width,
            .latency = 0,
        };
    }

    fn empty_mem(name: &str, kind: i8) -> MemDesc {
        return MemDesc{
            .name = name,
            .kind = kind,
            .depth = 0,
            .data_width = 0,
            .addr_width = 0,
            .ports = [empty_mem_port(); 8],
            .port_count = 0,
        };
    }

    fn make_bram(name: &str, depth: u32, data_width: u32) -> MemDesc {
        var addr_width : u32 = 0;
        var d : u32 = depth;
        while (d > 1) {
            addr_width = addr_width + 1;
            d = d / 2;
        }
        if (addr_width == 0) {
            addr_width = 1;
        }
        return MemDesc{
            .name = name,
            .kind = 0,
            .depth = depth,
            .data_width = data_width,
            .addr_width = addr_width,
            .ports = [empty_mem_port(); 8],
            .port_count = 0,
        };
    }

    fn make_rom(name: &str, depth: u32, data_width: u32) -> MemDesc {
        var addr_width : u32 = 0;
        var d : u32 = depth;
        while (d > 1) {
            addr_width = addr_width + 1;
            d = d / 2;
        }
        if (addr_width == 0) {
            addr_width = 1;
        }
        return MemDesc{
            .name = name,
            .kind = 2,
            .depth = depth,
            .data_width = data_width,
            .addr_width = addr_width,
            .ports = [empty_mem_port(); 8],
            .port_count = 0,
        };
    }

    fn add_read_port(mem: MemDesc, name: &str) -> MemDesc {
        var result = mem;
        if (result.port_count < 8) {
            result.ports[result.port_count] = make_mem_port(name, 0, result.addr_width, result.data_width);
            result.port_count = result.port_count + 1;
        }
        return result;
    }

    fn add_write_port(mem: MemDesc, name: &str) -> MemDesc {
        var result = mem;
        if (result.port_count < 8) {
            result.ports[result.port_count] = make_mem_port(name, 1, result.addr_width, result.data_width);
            result.port_count = result.port_count + 1;
        }
        return result;
    }

    fn add_rw_port(mem: MemDesc, name: &str) -> MemDesc {
        var result = mem;
        if (result.port_count < 8) {
            result.ports[result.port_count] = make_mem_port(name, 2, result.addr_width, result.data_width);
            result.port_count = result.port_count + 1;
        }
        return result;
    }

    // === Query functions ===

    fn port_count(mem: MemDesc) -> u32 {
        return mem.port_count;
    }

    fn total_bits(mem: MemDesc) -> u32 {
        return mem.depth * mem.data_width;
    }

    fn has_read_port(mem: MemDesc) -> bool {
        var i : u32 = 0;
        while (i < mem.port_count) {
            if (mem.ports[i].kind == 0 or mem.ports[i].kind == 2) {
                return true;
            }
            i = i + 1;
        }
        return false;
    }

    fn has_write_port(mem: MemDesc) -> bool {
        var i : u32 = 0;
        while (i < mem.port_count) {
            if (mem.ports[i].kind == 1 or mem.ports[i].kind == 2) {
                return true;
            }
            i = i + 1;
        }
        return false;
    }

    fn is_rom(mem: MemDesc) -> bool {
        return mem.kind == 2;
    }

    fn is_bram(mem: MemDesc) -> bool {
        return mem.kind == 0;
    }

    fn addr_width(mem: MemDesc) -> u32 {
        return mem.addr_width;
    }

    // === BRAM18E1 resource estimation ===

    fn bram18_count(mem: MemDesc) -> u32 {
        var bits : u32 = mem.depth * mem.data_width;
        var count : u32 = bits / 18432;
        if (bits % 18432 > 0) {
            count = count + 1;
        }
        return count;
    }

    // === Validation ===

    fn validate_mem(mem: MemDesc) -> u32 {
        var errors : u32 = 0;

        if (mem.name == "") {
            errors = errors + 1;
        }

        if (mem.depth == 0) {
            errors = errors + 1;
        }

        if (mem.data_width == 0) {
            errors = errors + 1;
        }

        if (mem.kind == 2 and has_write_port(mem)) {
            errors = errors + 1;
        }

        return errors;
    }

    // === Tests ===

    test empty_mem_has_no_ports
        given m = empty_mem("test", 0)
        then port_count(m) == 0

    test make_bram_has_depth
        given m = make_bram("ram1", 1024, 32)
        then m.depth == 1024
        and m.data_width == 32
        and m.addr_width == 10

    test make_bram_small
        given m = make_bram("ram2", 4, 8)
        then m.addr_width == 2

    test make_bram_single
        given m = make_bram("ram3", 1, 16)
        then m.addr_width == 1

    test add_read_port_increments
        given m = make_bram("ram1", 256, 16)
        and m2 = add_read_port(m, "rda")
        then port_count(m2) == 1
        and has_read_port(m2) == true
        and has_write_port(m2) == false

    test add_write_port_increments
        given m = make_bram("ram1", 256, 16)
        and m2 = add_write_port(m, "wra")
        then port_count(m2) == 1
        and has_write_port(m2) == true
        and has_read_port(m2) == false

    test add_rw_port
        given m = make_bram("ram1", 256, 16)
        and m2 = add_rw_port(m, "rwa")
        then port_count(m2) == 1
        and has_read_port(m2) == true
        and has_write_port(m2) == true

    test is_rom
        given m = make_rom("rom1", 512, 8)
        then is_rom(m) == true
        and is_bram(m) == false

    test total_bits
        given m = make_bram("ram1", 1024, 32)
        then total_bits(m) == 32768

    test bram18_count_small
        given m = make_bram("ram1", 1024, 18)
        then bram18_count(m) == 1

    test bram18_count_large
        given m = make_bram("ram1", 4096, 36)
        then bram18_count(m) >= 8

    test validate_ok
        given m = make_bram("ram1", 256, 16)
        and m2 = add_read_port(m, "rda")
        and errors = validate_mem(m2)
        then errors == 0

    test validate_empty_name
        given m = empty_mem("", 0)
        and m2 = MemDesc{.name = "", .kind = 0, .depth = 16, .data_width = 8, .addr_width = 4, .ports = [empty_mem_port(); 8], .port_count = 0}
        and errors = validate_mem(m2)
        then errors > 0

    test validate_zero_depth
        given m = MemDesc{.name = "x", .kind = 0, .depth = 0, .data_width = 8, .addr_width = 1, .ports = [empty_mem_port(); 8], .port_count = 0}
        and errors = validate_mem(m)
        then errors > 0

    test rom_with_write_port_invalid
        given m = make_rom("rom1", 256, 16)
        and m2 = add_write_port(m, "wra")
        and errors = validate_mem(m2)
        then errors > 0

    // === Invariants ===

    invariant bram_depth_positive
        given m = make_bram("inv", 256, 16)
        assert m.depth > 0

    invariant bram_data_width_positive
        given m = make_bram("inv", 256, 16)
        assert m.data_width > 0

    invariant addr_width_positive_for_nonzero_depth
        given m = make_bram("inv", 256, 16)
        assert m.addr_width > 0

    invariant total_bits_non_negative
        given m = make_bram("inv", 256, 16)
        assert total_bits(m) >= 0

    invariant port_count_within_bounds
        given m = make_bram("inv", 256, 16)
        and m2 = add_read_port(m, "rda")
        assert port_count(m2) <= 8

    invariant bram18_count_positive
        given m = make_bram("inv", 1024, 32)
        assert bram18_count(m) > 0

    // === Benchmarks ===

    bench bram18_count_latency
        measure: nanoseconds to bram18_count(make_bram("bench", 4096, 32))
        target: < 100ns
}

// phi^2 + 1/phi^2 = 3 | TRINITY

Открыть спеку урока в плеере ↗

Все уроки

• Модуль 1 · Что такое шина

  Зачем вообще существует шина: разговор по проводам, с кадрами и адресами, и кому позволено говорить.

  1. 01 Провода, которые говорят
  2. 02 Кадрирование разговора
  3. 03 Хозяин и слуга

• Модуль 2 · Разговор по UART

  Двухпроводная шина без такта: кадр, делитель, задающий скорость, и статус, который опрашивает драйвер.

  1. 04 Кадр: старт, данные, стоп
  2. 05 Бод и делитель
  3. 06 Статус и FIFO

• Модуль 3 · SPI под тактом

  Разговор под тактом: четыре режима, лестница предделителей и выбор кристалла на каждого подчинённого.

  1. 07 Режимы: CPOL и CPHA
  2. 08 Лестница предделителей
  3. 09 Выбор кристалла и ширины

• Модуль 4 · Регистровая шина APB

  Шина регистров: PSEL и PENABLE, строобы и ожидания, и сколько адресных бит стоит количество периферии.

  1. 10 PSEL и PENABLE
  2. 11 Строобы и ожидания
  3. 12 Дешифрация адреса

• Модуль 5 · Пять каналов AXI4

  Пять каналов: адрес, данные и отклик в обе стороны, lite или full, пакеты и идентификаторы.

  1. 13 Пять каналов
  2. 14 Lite или full
  3. 15 Пакеты и идентификаторы

• Модуль 6 · Память

  Что находится на дальнем конце каждой шины: карты памяти, типы портов и задержка, которую должно покрывать ожидание.

  1. 16 Карты памяти
  2. 17 Порты и типы
  3. 18 Задержка

• Модуль 7 · Мосты

  Почему в дизайне появляется больше одной шины и пакетный мост, переносящий работу между ними.

  1. 19 Зачем мосты
  2. 20 Пакетный мост
  3. 21 Всё в одном стенде

• Модуль 8 · Ethernet: кадры и тайминг

  Кадры, контрольная сумма кадра, тайминг RGMII и заранее зарегистрированные шаги настоящего запуска.

  1. 22 Кадры и контрольная сумма
  2. 23 Тайминг RGMII
  3. 24 Запуск на стенде

• Модуль 9 · Стенд

  Дисциплина, оберегающая настоящее железо: кто держит IO, как взять и вернуть захват, и что запускается дальше.

  1. 25 Кто держит IO
  2. 26 Захват и возврат
  3. 27 Капстоун: что запускается дальше