t27.aiEnglish

Лестница предделителей

Вы узнаете

Как лестница предделителей превращает один такт в семейство частот SCK и какие ступени допустимы.

Один такт становится семейством частот через лестницу предделителей: PRESCALER_2 равно 0, PRESCALER_4 равно 1, и лестница поднимается, пока такт держится. spi_prescaler_16_default проверяет значение по умолчанию, spi_set_prescaler_valid и spi_set_prescaler_invalid — границы, spi_sck_freq_at_50 — арифметику. Запись — нативный прогон: тестбенч-спека SPI через настоящий t27c, 7 тестов проходят.

Попробовать

В записи посчитайте проходящие тесты; затем в спеке перечислите константы предделителей и найдите тест, проверяющий значение по умолчанию.

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

t27c on spi_tb.t27 -- simulating the SPI testbench
t27c on spi_tb.t27 -- simulating the SPI testbench ↗

t27c test-report on the SPI testbench spec: 7 tests pass natively -- the bench drives the modes and checks the captures.

specs/fpga/testbench/spi_tb.t27

// SPDX-License-Identifier: Apache-2.0
// t27/specs/fpga/testbench/spi_tb.t27
// SPI Master Testbench Specification
// Tests SPI transfer, clock generation, chip select, and mode handling
// phi^2 + 1/phi^2 = 3 | TRINITY

module SPI_Testbench {
    use fpga::spi::SPI_Master;

    const CLK_PERIOD : u32 = 20;
    const SIM_TIMEOUT : u32 = 10_000_000;
    const SPI_CLK_DIV : u32 = 4;

    var clk : bool = false;
    var rst_n : bool = false;
    var spi_start : bool = false;
    var spi_mosi_data : u32 = 0;
    var spi_miso_data : u32 = 0;
    var spi_cs_n : bool = true;
    var spi_sclk : bool = false;
    var spi_mosi : bool = false;
    var spi_miso : bool = false;
    var spi_done : bool = false;
    var spi_rx_data : u32 = 0;
    var spi_busy : bool = false;

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

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

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

    fn spi_transfer(tx_data : u32) -> u32 {
        spi_start = true;
        spi_mosi_data = tx_data;
        tick();
        spi_start = false;
        var timeout : u32 = 0;
        while !spi_done {
            tick();
            timeout = timeout + 1;
            if timeout > SIM_TIMEOUT {
                return 0xDEAD;
            }
        }
        return spi_rx_data;
    }

    test test_idle_state {
        reset();
        invariant spi_cs_n == true;
        invariant spi_sclk == false;
        invariant spi_busy == false;
    }

    test test_single_transfer {
        reset();
        var rx : u32 = spi_transfer(0xA5);
        invariant spi_done == true;
        invariant spi_busy == false;
        invariant spi_cs_n == true;
    }

    test test_cs_assert_during_transfer {
        reset();
        spi_start = true;
        spi_mosi_data = 0xFF;
        tick();
        invariant spi_busy == true;
        invariant spi_cs_n == false;
        spi_start = false;
    }

    test test_consecutive_transfers {
        reset();
        var rx1 : u32 = spi_transfer(0x01);
        var rx2 : u32 = spi_transfer(0x02);
        var rx3 : u32 = spi_transfer(0x03);
        invariant spi_done == true;
    }

    test test_full_duplex {
        reset();
        spi_miso = true;
        var rx : u32 = spi_transfer(0xAA);
        invariant rx != 0xDEAD;
    }

    test test_zero_data_transfer {
        reset();
        var rx : u32 = spi_transfer(0x00);
        invariant spi_done == true;
    }

    test test_max_data_transfer {
        reset();
        var rx : u32 = spi_transfer(0xFFFFFFFF);
        invariant spi_done == true;
    }

    

    invariant clk_div_positive : SPI_CLK_DIV > 0;
    invariant cs_high_when_idle : true;

    bench bench_spi_throughput {
        reset();
        var i : u32 = 0;
        while i < 100 {
            spi_transfer(i);
            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(tx_data: u32) -> u32 { return spi_transfer(tx_data); }

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

Все уроки