t27.aiРусский

Sizing the depth

You will learn

How depth follows from the write rate, the read rate and the worst burst, and what a real timed loop measures.

Depth is not a feeling: writes at rate W, reads at rate R, and the buffer must hold the worst burst times (W - R) over the time it lasts. Oversize it and it costs BRAM you could have spent; undersize it and it overflows silently, because a full FIFO drops or blocks and neither shows up in a waveform. The widget is a real loop with a measured time -- 19.06 s for router1, bitwalk, xc7frames2bit and the SRAM load, on a laptop at load average about 110 -- the same arithmetic of rate and time that sizes a buffer, measured on a run that really happened. The spec frame opens fifo.t27, whose fill_count is the number this lesson is about.

Try it

In the widget, find the loop's measured time and the load average it ran at; then in the spec frame find fill_count and write the depth formula for your own worst burst.

Open the interactive lesson →

tri competitors audit: the table, audited
tri competitors audit: the table, audited ↗

168 records: 14 papers entered twice, 141 cite no score, 144 state zero at pass@1.

specs/fpga/fifo.t27

// SPDX-License-Identifier: Apache-2.0
// t27/specs/fpga/fifo.t27
// Synchronous and Asynchronous FIFO Stdlib for Trinity T27 FPGA HIR
// Defines FIFO configuration with depth, data width, and flags
// Uses flat arrays + count fields (parser-compatible)
// phi^2 + 1/phi^2 = 3 | TRINITY

module Fifo {

    // === FIFO kind ===

    pub const FifoKind = enum(i8) {
        sync_fifo = 0,
        async_fifo = 1,
    }

    // === FIFO status flags ===

    pub struct FifoFlags {
        empty : bool,
        full : bool,
        almost_empty : bool,
        almost_full : bool,
    }

    // === FIFO configuration ===

    pub struct FifoConfig {
        name : &str,
        kind : i8,
        depth : u32,
        data_width : u32,
        has_almost_empty : bool,
        has_almost_full : bool,
        almost_empty_threshold : u32,
        almost_full_threshold : u32,
        use_bram : bool,
    }

    // === FIFO runtime state (for simulation) ===

    pub const MAX_FIFO_DEPTH : u32 = 65536;

    pub struct FifoState {
        fill_count : u32,
        head_ptr : u32,
        tail_ptr : u32,
        flags : FifoFlags,
    }

    // === Constructor helpers ===

    fn sync_fifo(name: &str, depth: u32, data_width: u32) -> FifoConfig {
        return FifoConfig{
            .name = name,
            .kind = 0,
            .depth = depth,
            .data_width = data_width,
            .has_almost_empty = false,
            .has_almost_full = false,
            .almost_empty_threshold = 0,
            .almost_full_threshold = 0,
            .use_bram = true,
        };
    }

    fn async_fifo(name: &str, depth: u32, data_width: u32) -> FifoConfig {
        return FifoConfig{
            .name = name,
            .kind = 1,
            .depth = depth,
            .data_width = data_width,
            .has_almost_empty = false,
            .has_almost_full = false,
            .almost_empty_threshold = 0,
            .almost_full_threshold = 0,
            .use_bram = true,
        };
    }

    fn with_almost_empty(cfg: FifoConfig, threshold: u32) -> FifoConfig {
        var result = cfg;
        result.has_almost_empty = true;
        result.almost_empty_threshold = threshold;
        return result;
    }

    fn with_almost_full(cfg: FifoConfig, threshold: u32) -> FifoConfig {
        var result = cfg;
        result.has_almost_full = true;
        result.almost_full_threshold = threshold;
        return result;
    }

    fn empty_fifo_state() -> FifoState {
        return FifoState{
            .fill_count = 0,
            .head_ptr = 0,
            .tail_ptr = 0,
            .flags = FifoFlags{
                .empty = true,
                .full = false,
                .almost_empty = false,
                .almost_full = false,
            },
        };
    }

    // === Query functions ===

    fn is_sync(cfg: FifoConfig) -> bool {
        return cfg.kind == 0;
    }

    fn is_async(cfg: FifoConfig) -> bool {
        return cfg.kind == 1;
    }

    fn addr_width(cfg: FifoConfig) -> u32 {
        var d : u32 = cfg.depth;
        var w : u32 = 0;
        while (d > 1) {
            w = w + 1;
            d = d / 2;
        }
        if (w == 0) {
            w = 1;
        }
        return w;
    }

    fn total_storage_bits(cfg: FifoConfig) -> u32 {
        return cfg.depth * cfg.data_width;
    }

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

    fn is_empty(state: FifoState) -> bool {
        return state.flags.empty;
    }

    fn is_full(state: FifoState) -> bool {
        return state.flags.full;
    }

    fn fill_count(state: FifoState) -> u32 {
        return state.fill_count;
    }

    fn has_space(state: FifoState) -> bool {
        return state.flags.full == false;
    }

    fn has_data(state: FifoState) -> bool {
        return state.flags.empty == false;
    }

    // === Push/Pop state updates ===

    fn push(state: FifoState, cfg: FifoConfig) -> FifoState {
        var result = state;
        if (state.flags.full) {
            return result;
        }
        result.tail_ptr = (state.tail_ptr + 1) % cfg.depth;
        result.fill_count = state.fill_count + 1;
        result.flags.empty = false;
        if (result.fill_count == cfg.depth) {
            result.flags.full = true;
        }
        return result;
    }

    fn pop(state: FifoState, cfg: FifoConfig) -> FifoState {
        var result = state;
        if (state.flags.empty) {
            return result;
        }
        result.head_ptr = (state.head_ptr + 1) % cfg.depth;
        result.fill_count = state.fill_count - 1;
        result.flags.full = false;
        if (result.fill_count == 0) {
            result.flags.empty = true;
        }
        return result;
    }

    // === Validation ===

    fn validate_fifo(cfg: FifoConfig) -> u32 {
        var errors : u32 = 0;

        if (cfg.name == "") {
            errors = errors + 1;
        }
        if (cfg.depth == 0) {
            errors = errors + 1;
        }
        if (cfg.data_width == 0) {
            errors = errors + 1;
        }
        if (cfg.has_almost_empty and cfg.almost_empty_threshold >= cfg.depth) {
            errors = errors + 1;
        }
        if (cfg.has_almost_full and cfg.almost_full_threshold >= cfg.depth) {
            errors = errors + 1;
        }

        return errors;
    }

    // === Tests ===

    test sync_fifo_is_sync
        given f = sync_fifo("tx_fifo", 16, 8)
        then is_sync(f) == true
        and is_async(f) == false

    test async_fifo_is_async
        given f = async_fifo("cross_fifo", 32, 16)
        then is_async(f) == true
        and is_sync(f) == false

    test addr_width_16
        given f = sync_fifo("f", 16, 8)
        then addr_width(f) == 4

    test addr_width_256
        given f = sync_fifo("f", 256, 32)
        then addr_width(f) == 8

    test total_storage_bits
        given f = sync_fifo("f", 16, 32)
        then total_storage_bits(f) == 512

    test bram18_small
        given f = sync_fifo("f", 16, 32)
        then bram18_count(f) == 1

    test empty_state_is_empty
        given s = empty_fifo_state()
        then is_empty(s) == true
        and is_full(s) == false
        and fill_count(s) == 0
        and has_data(s) == false
        and has_space(s) == true

    test push_increments_fill
        given cfg = sync_fifo("f", 4, 8)
        and s = empty_fifo_state()
        and s2 = push(s, cfg)
        then fill_count(s2) == 1
        and is_empty(s2) == false

    test push_to_full
        given cfg = sync_fifo("f", 2, 8)
        and s = empty_fifo_state()
        and s2 = push(s, cfg)
        and s3 = push(s2, cfg)
        then is_full(s3) == true
        and fill_count(s3) == 2

    test push_on_full_noop
        given cfg = sync_fifo("f", 2, 8)
        and s = empty_fifo_state()
        and s2 = push(s, cfg)
        and s3 = push(s2, cfg)
        and s4 = push(s3, cfg)
        then fill_count(s4) == 2

    test pop_decrements_fill
        given cfg = sync_fifo("f", 4, 8)
        and s = empty_fifo_state()
        and s2 = push(s, cfg)
        and s3 = pop(s2, cfg)
        then fill_count(s3) == 0
        and is_empty(s3) == true

    test pop_on_empty_noop
        given cfg = sync_fifo("f", 4, 8)
        and s = empty_fifo_state()
        and s2 = pop(s, cfg)
        then fill_count(s2) == 0

    test push_pop_roundtrip
        given cfg = sync_fifo("f", 4, 8)
        and s = empty_fifo_state()
        and s2 = push(s, cfg)
        and s3 = push(s2, cfg)
        and s4 = pop(s3, cfg)
        then fill_count(s4) == 1
        and has_data(s4) == true
        and has_space(s4) == true

    test with_almost_empty
        given f = sync_fifo("f", 16, 8)
        and f2 = with_almost_empty(f, 2)
        then f2.has_almost_empty == true
        and f2.almost_empty_threshold == 2

    test with_almost_full
        given f = sync_fifo("f", 16, 8)
        and f2 = with_almost_full(f, 14)
        then f2.has_almost_full == true
        and f2.almost_full_threshold == 14

    test validate_ok
        given f = sync_fifo("f", 16, 8)
        then validate_fifo(f) == 0

    test validate_empty_name
        given f = sync_fifo("", 16, 8)
        then validate_fifo(f) > 0

    test validate_zero_depth
        given f = FifoConfig{.name = "x", .kind = 0, .depth = 0, .data_width = 8, .has_almost_empty = false, .has_almost_full = false, .almost_empty_threshold = 0, .almost_full_threshold = 0, .use_bram = true}
        then validate_fifo(f) > 0

    // === Invariants ===

    invariant fill_count_non_negative
        given s = empty_fifo_state()
        assert fill_count(s) >= 0

    invariant fill_count_le_depth
        given cfg = sync_fifo("inv", 16, 8)
        and s = push(empty_fifo_state(), cfg)
        assert fill_count(s) <= cfg.depth

    invariant empty_xor_full
        given s = empty_fifo_state()
        assert (is_empty(s) and is_full(s)) == false

    invariant has_space_iff_not_full
        given s = empty_fifo_state()
        assert has_space(s) == (is_full(s) == false)

    invariant has_data_iff_not_empty
        given s = empty_fifo_state()
        assert has_data(s) == (is_empty(s) == false)

    invariant bram18_positive
        given f = sync_fifo("inv", 16, 8)
        assert bram18_count(f) > 0

    // === Benchmarks ===

    bench push_latency
        measure: nanoseconds to push(empty_fifo_state(), sync_fifo("b", 16, 8))
        target: < 100ns

    bench pop_latency
        measure: nanoseconds to pop(push(empty_fifo_state(), sync_fifo("b", 16, 8)), sync_fifo("b", 16, 8))
        target: < 100ns
}

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

Open the lesson's spec in the player ↗

All lessons