t27.aiEnglish

Задержка

Вы узнаете

В скольких тактах память отвечает и что стенд памяти проверяет в чтении и записи.

Каждый ответ стоит тактов, и перечисление MemLatency спеки несёт типы, которые должно покрывать состояние ожидания. Стенд проверяет поведение: test_reset_clears, test_write_read_single, test_write_read_multiple, test_overwrite, test_all_zero_bits, девять тестов. Запись опускает тестбенч-спеку памяти в Verilog.

Попробовать

В записи найдите тесты стенда; затем в спеке найдите типы MemLatency и скажите, что должно покрывать состояние ожидания.

Открыть интерактивный урок →

t27c gen-verilog on memory_tb.t27 -- the testbench as RTL
t27c gen-verilog on memory_tb.t27 -- the testbench as RTL ↗

The memory testbench spec lowered to Verilog: what a bench looks like when the compiler emits it.

specs/fpga/testbench/memory_tb.t27

// SPDX-License-Identifier: Apache-2.0
// t27/specs/fpga/testbench/memory_tb.t27
// Memory Subsystem Testbench
// Tests BRAM, register file, and memory-mapped I/O operations
// phi^2 + 1/phi^2 = 3 | TRINITY

module Memory_Testbench {
    use fpga::memory::Memory;

    const CLK_PERIOD : u32 = 20;
    const SIM_TIMEOUT : u32 = 5_000_000;
    const MEM_BASE : u32 = 0x0000_0000;
    const MEM_SIZE : u32 = 0x0001_0000;

    var clk : bool = false;
    var rst_n : bool = false;
    var mem_addr : u32 = 0;
    var mem_wdata : u32 = 0;
    var mem_rdata : u32 = 0;
    var mem_we : bool = false;
    var mem_re : bool = false;
    var mem_valid : bool = false;
    var mem_ready : bool = false;

    var test_passed : u32 = 0;
    var test_failed : u32 = 0;

    fn tick() {
        clk = false;
        clk = true;
    }

    fn reset() {
        rst_n = false;
        tick();
        tick();
        rst_n = true;
        tick();
    }

    fn mem_write(addr : u32, data : u32) {
        mem_addr = addr;
        mem_wdata = data;
        mem_we = true;
        mem_re = false;
        tick();
        while !mem_ready { tick(); }
        mem_we = false;
    }

    fn mem_read(addr : u32) -> u32 {
        mem_addr = addr;
        mem_re = true;
        mem_we = false;
        tick();
        while !mem_ready { tick(); }
        mem_re = false;
        return mem_rdata;
    }

    test test_reset_clears {
        reset();
        invariant mem_ready == true || mem_ready == false;
    }

    test test_write_read_single {
        reset();
        mem_write(0x100, 0xCAFEBABE);
        var val : u32 = mem_read(0x100);
        invariant val == 0xCAFEBABE;
    }

test test_write_read_multiple {
         reset();
         
         while i < 16 {
            mem_write(MEM_BASE + i * 4, i * 0x11);
            i = i + 1;
        }
        i = 0;
        while i < 16 {
            var val : u32 = mem_read(MEM_BASE + i * 4);
            invariant val == i * 0x11;
            i = i + 1;
        }
    }

    test test_overwrite {
        reset();
        mem_write(0x200, 0xAAAA);
        mem_write(0x200, 0xBBBB);
        var val : u32 = mem_read(0x200);
        invariant val == 0xBBBB;
    }

    test test_all_zero_bits {
        reset();
        mem_write(0x300, 0x00000000);
        var val : u32 = mem_read(0x300);
        invariant val == 0;
    }

    test test_all_one_bits {
        reset();
        mem_write(0x300, 0xFFFFFFFF);
        var val : u32 = mem_read(0x300);
        invariant val == 0xFFFFFFFF;
    }

    test test_byte_addresses {
        reset();
        mem_write(0x400, 0x12);
        mem_write(0x401, 0x34);
        mem_write(0x402, 0x56);
        mem_write(0x403, 0x78);
        var val : u32 = mem_read(0x400);
        invariant val == 0x12;
    }

    invariant mem_size_positive : MEM_SIZE > 0;

    test test_tick_toggles_clock {
        reset();
        // Clock should start in false state after reset
        invariant clk == false;
        // After first tick, clock should be true
        tick();
        invariant clk == true;
        // After second tick, clock should be false again
        tick();
        invariant clk == false;
}
    
    test test_on_comb_returns_mem_read {
        reset();
        mem_write(0x100, 0xDEADBEEF);
        var val : u32 = on_comb(0x100);
        invariant val == 0xDEADBEEF;
    }
    
    bench bench_memory_bandwidth {
        reset();
        var i : u32 = 0;
        while i < 256 {
            mem_write(i * 4, i);
            i = i + 1;
        }
        i = 0;
        while i < 256 {
            mem_read(i * 4);
            i = i + 1;
        }
    }
}

// W696: the hardware boundary, DERIVED -- not chosen.
//
// T187 measured an exact equivalence over 617 specs: a module gets a data
// port iff the spec declares `on_comb` or `on_clock`. Without one the
// compiler emits `NO DATA PORTS -- this module cannot move a value across
// its boundary`, and synthesis optimises the whole thing away.
//
// The standing rule is that the default must NOT be guessed. Here no guess
// was made: `t27c entry-points` found exactly ONE function in this spec that
// takes a parameter, returns a value, has a body, and whose types all have a
// known width. With one candidate the choice is forced, so this forwards and
// invents nothing. 11 of 387 port-less specs qualified.
fn on_comb(addr: u32) -> u32 { return mem_read(addr); }

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

Все уроки