Baud and the divisor
You will learn
How one divisor turns a clock into a bit rate, and what changing it breaks.
The rate is a divisor: the clock divided by the baud gives the bit period, and the spec states it as a constant expression -- UART_BIT_PERIOD is UART_CLOCK_HZ / UART_BAUD_RATE, 100,000,000 over 115,200. The test uart_configure_changes_baud_divisor checks that configuring the driver moves the divisor. The recording shows the spec lowered to hardware IR: the compiler's own view of the wires and state before Verilog exists.
Try it
In the recording, watch the IR view of the divisor; then in the spec frame find UART_BIT_PERIOD and the test that moves it.
The UART spec lowered to hardware IR: the compiler's own view of the wires, ports and state before Verilog exists.
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); }
All lessons
Module 1 · What a bus is
Why a bus exists at all: a conversation on wires, framed and addressed, and who is allowed to talk.
Module 2 · UART
The two-wire bus with no clock: the frame, the divisor that sets the rate, and the status a driver polls.
Module 3 · SPI
The clocked conversation: four modes, a prescaler ladder, and a chip select per servant.
Module 4 · APB
The register bus: PSEL and PENABLE, strobes and wait states, and how many address bits a peripheral count costs.
Module 5 · AXI4
The five channels: address, data and response in both directions, lite or full, bursts and IDs.
Module 6 · Memory
What sits on the far side of every bus: memory maps, port kinds, and latency that a wait state must cover.
Module 7 · Bridges
Why designs grow more than one bus, and the packet bridge that moves work between them.
Module 8 · Ethernet
Frames, the frame check sequence, RGMII timing, and the pre-registered steps of a real bring-up.
Module 9 · The bench
The discipline that guards real hardware: who holds the IO, taking and giving the lock, and what runs next.