t27.aiEnglish

Провода, которые говорят

Вы узнаете

Зачем нужна шина, сколько стоит двухпроводный разговор UART и что проверяет спека, открывающая курс.

Шина существует потому, что выводы дороги: двум чипам, которым надо поговорить, приходится делить провода, и провода несут разговор, о котором обе стороны договорились заранее. Простейший случай — UART из спеки этого урока, ZeroDSP_UART: два провода, без такта, обе стороны согласовали скорость — спека несёт UART_CLOCK_HZ равный 100,000,000 и UART_BAUD_RATE равный 115,200. Запись прогоняет t27c check по спеке: 0 ошибок, 0 предупреждений — стартовую планку, которую проходит спека каждого урока. Плеер компилирует её в вашем браузере.

Попробовать

В записи найдите количество ошибок и предупреждений; затем в спеке найдите UART_CLOCK_HZ и UART_BAUD_RATE и разделите их, получив период бита.

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

t27c check on uart.t27 -- the spec compiles
t27c check on uart.t27 -- the spec compiles ↗

t27c check typechecks the UART spec: 0 errors, 0 warnings, the first bar every lesson's spec clears.

specs/fpga/uart.t27

// SPDX-License-Identifier: Apache-2.0
// t27/specs/fpga/uart.t27
// ZeroDSP FPGA UART Specification
// UART for debugging and communication
// φ² + 1/φ² = 3 | TRINITY

module ZeroDSP_UART {
    use base::types;
    use base::ops;
    use isa::registers;

    const UART_CLOCK_HZ : u32 = 100_000_000;
    const UART_BAUD_RATE : u32 = 115200;
    const UART_BIT_PERIOD : u32 = UART_CLOCK_HZ / UART_BAUD_RATE;

    const UART_WIDTH : usize = 8;
    const UART_FIFO_DEPTH : usize = 16;

    const STATUS_IDLE : u8 = 0;
    const STATUS_TX_BUSY : u8 = 1;
    const STATUS_RX_BUSY : u8 = 2;
    const STATUS_ERROR : u8 = 3;

    struct UARTState {
        tx_data : u8,
        tx_valid : bool,
        tx_ready : bool,
        rx_data : u8,
        rx_valid : bool,
        rx_error : bool,
        bit_counter : u8,
        status : u8,
    }

    var uart_state : UARTState = UARTState{
        .tx_data = 0,
        .tx_valid = false,
        .tx_ready = true,
        .rx_data = 0,
        .rx_valid = false,
        .rx_error = false,
        .bit_counter = 0,
        .status = STATUS_IDLE,
    };

    struct UARTConfig {
        baud_divisor : u32,
        parity_enable : bool,
        stop_bits : u8,
        fifo_enable : bool,
    }

    var uart_config : UARTConfig = UARTConfig{
        .baud_divisor = UART_CLOCK_HZ / (UART_BAUD_RATE * 16),
        .parity_enable = false,
        .stop_bits = 1,
        .fifo_enable = true,
    };

    fn uart_tx_ready() -> bool {
        return uart_state.tx_ready;
    }

    fn uart_tx_send(data: u8) -> bool {
        if (!uart_state.tx_ready) {
            return false;
        }
        uart_state.tx_data = data;
        uart_state.tx_valid = true;
        uart_state.tx_ready = false;
        uart_state.status = STATUS_TX_BUSY;
        return true;
    }

    fn uart_rx_ready() -> bool {
        return uart_state.rx_valid;
    }

    fn uart_rx_read() -> u8 {
        uart_state.rx_valid = false;
        return uart_state.rx_data;
    }

    fn uart_status() -> u8 {
        return uart_state.status;
    }

    fn uart_reset() -> void {
        uart_state.tx_data = 0;
        uart_state.tx_valid = false;
        uart_state.tx_ready = true;
        uart_state.rx_data = 0;
        uart_state.rx_valid = false;
        uart_state.rx_error = false;
        uart_state.bit_counter = 0;
        uart_state.status = STATUS_IDLE;
    }

    fn uart_configure(
        baud_divisor: u32,
        parity_enable: bool,
        stop_bits: u8,
        fifo_enable: bool,
    ) -> void {
        uart_config.baud_divisor = baud_divisor;
        uart_config.parity_enable = parity_enable;
        uart_config.stop_bits = stop_bits;
        uart_config.fifo_enable = fifo_enable;
    }

    test uart_initially_idle
        given status = uart_status()
        then status == STATUS_IDLE

    test uart_tx_ready_initially
        given ready = uart_tx_ready()
        then ready == true

    test uart_rx_not_valid_initially
        given valid = uart_rx_ready()
        then valid == false

    test uart_tx_send_returns_true_when_ready
        given result = uart_tx_send(0x55)
        then result == true

    test uart_tx_send_returns_false_when_busy
        given uart_tx_send(0x55)
        and   result = uart_tx_send(0xAA)
        then result == false

    test uart_reset_clears_status
        given uart_tx_send(0x55)
        and   uart_reset()
        and   status = uart_status()
        then status == STATUS_IDLE

    test uart_reset_restores_tx_ready
        given uart_tx_send(0x55)
        and   uart_reset()
        and   ready = uart_tx_ready()
        then ready == true

    test uart_configure_changes_baud_divisor
        given uart_configure(100, false, 1, true)
        then uart_config.baud_divisor == 100

    test uart_configure_parity_enable
        given uart_configure(54, true, 2, false)
        then uart_config.parity_enable == true
        and uart_config.stop_bits == 2
        and uart_config.fifo_enable == false

    test uart_bit_period_calc
        then UART_BIT_PERIOD == UART_CLOCK_HZ / UART_BAUD_RATE

    test uart_constants
        then UART_FIFO_DEPTH == 16
        and UART_WIDTH == 8
        and STATUS_IDLE == 0
        and STATUS_TX_BUSY == 1
        and STATUS_RX_BUSY == 2
        and STATUS_ERROR == 3

    test uart_tx_send_updates_state
        given result = uart_tx_send(0x42)
        then result == true
        and uart_state.tx_data == 0x42
        and uart_state.tx_valid == true
        and uart_state.tx_ready == false
        and uart_state.status == STATUS_TX_BUSY

    test uart_rx_read_clears_valid
        given uart_state.rx_data = 0x99;
        and   uart_state.rx_valid = true;
        given data = uart_rx_read()
        then data == 0x99
        and uart_state.rx_valid == false

    test uart_reset_clears_rx_error
        given uart_state.rx_error = true;
        and   uart_reset()
        then uart_state.rx_error == false

    test uart_reset_clears_bit_counter
        given uart_state.bit_counter = 7;
        and   uart_reset()
        then uart_state.bit_counter == 0

    test uart_statement_body_with_given
        given tmp = 1
        and   y = 2
        then tmp == y

    invariant uart_status_valid
        given status = uart_status()
        assert status == STATUS_IDLE or status == STATUS_TX_BUSY or 
               status == STATUS_RX_BUSY or status == STATUS_ERROR

    invariant uart_tx_ready_inverse_tx_busy
        given status = uart_status()
        assert (uart_state.tx_ready) == (status == STATUS_IDLE)

    bench uart_tx_ready_latency
        measure: nanoseconds to uart_tx_ready()
        target: < 10ns

    bench uart_rx_ready_latency
        measure: nanoseconds to uart_rx_ready()
        target: < 10ns

    bench uart_reset_latency
        measure: nanoseconds to uart_reset()
        target: < 50ns
}

// 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(data: u8) -> bool { return uart_tx_send(data); }

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

Все уроки