Files
retroSoC/docs/ip/ws2812.md
T
maksyuki dd3cb6ff5c feat: add formal verification properties for DMA design and corresponding testbench
- Introduced  to define formal properties for the DMA design, ensuring correct behavior under various conditions.
- Created  as a testbench for the DMA register interface, implementing APB and AXI4 protocols to validate register operations.
- Added  to verify synchronization between RTL and SDK register constants, ensuring consistency across implementations.
2026-08-18 16:54:55 +08:00

5.9 KiB

WS2812 Transmitter

The Mini SoC WS2812 block is a single-channel, transmit-only peripheral for 24-bit GRB LED words. It replaces the former generic one-wire block; it is not a Dallas/Maxim 1-Wire controller. The block has a strict APB4 register target, a 16-word FIFO, programmable symbol and reset timing, sticky interrupt and error state, and a GPIO alternate-function output.

Integration

Property Value
APB4 base address 0x10008000
FIFO depth 16 24-bit words
Pixel order GRB, bit 23 first
GPIO route GPIO2 alternate function 1
APB4 interrupt group Bit 10
Management-core interrupt 17
DMA target Fixed address TXDATA

IP_INFO reports the implemented data width, FIFO depth, and ABI version so software does not need to duplicate the configured FIFO depth. The current value is 0x18100100: 24-bit data, 16 entries, ABI 1.0.

Register ABI

All registers are 32 bits and naturally aligned. Unmapped, unaligned, and direction-invalid accesses complete with resp_err. TXDATA requires all four byte strobes; partial writes complete with resp_err and set the command error. Timing and frame registers support byte strobes unless noted below.

Offset Name Access Description
0x00 BIT_CYCLES RW Total system-clock cycles per serialized bit; implemented width is 16 bits.
0x04 T0H_CYCLES RW High cycles for a zero bit; implemented width is 16 bits.
0x08 T1H_CYCLES RW High cycles for a one bit; implemented width is 16 bits.
0x0C RESET_CYCLES RW Low cycles after a frame, abort, or underflow.
0x10 TXDATA WO Push one 24-bit GRB word into the FIFO. Bits 31:24 must be zero in software.
0x14 CTRL WO One-hot commands: bit 0 START, bit 1 ABORT, bit 2 FIFO_FLUSH.
0x18 STATUS RO Bits 0:4 are BUSY, FIFO_EMPTY, FIFO_FULL, CONFIG_VALID, and RESET_ACTIVE.
0x1C FRAME_WORDS RW Exact number of FIFO words consumed by the next frame.
0x20 FIFO_LEVEL RO Current FIFO occupancy.
0x24 FIFO_WATERMARK RW Low-watermark threshold; valid values are 0 through 15.
0x28 REMAINING_WORDS RO Frame words not yet completely serialized.
0x2C ERROR_STATUS RW1C Bits 0:2 are configuration, underflow, and command errors.
0x30 INTR_STATE RW1C Bits 0:3 are done, FIFO-low, error, and aborted state.
0x34 INTR_ENABLE RW Interrupt enable mask.
0x38 INTR_TEST WO Write-one software interrupt test bits.
0x3C IP_INFO RO {data_width, fifo_depth, abi_major, abi_minor}.

The external interrupt is the reduction OR of INTR_STATE & INTR_ENABLE. ERROR_STATUS and INTR_STATE are sticky until software writes one to clear the corresponding bit. INTR_STATE.ERROR reflects any newly observed error. FIFO_LOW is asserted while a frame still needs input and FIFO occupancy is at or below the programmed watermark.

Timing contract

The active timing is captured on an accepted START command and cannot change mid-frame. A valid configuration satisfies:

0 < T0H_CYCLES < T1H_CYCLES < BIT_CYCLES
RESET_CYCLES > 0

For a source frequency f and duration in nanoseconds, the HAL rounds the bit and high durations to the nearest integer cycle. It rounds reset duration up, so the specified minimum reset/latch time is never shortened. The default HAL profile is a 1,250 ns bit, 350 ns zero-high, 700 ns one-high, and 300 us reset. Software must recompute and program the timing after changing the source clock.

Transfer sequence

  1. Configure GPIO2 for alternate function 1 and call rs_ws2812_init().
  2. Clear old errors and interrupts, flush the idle FIFO, and enqueue initial 24-bit GRB words.
  3. Program the exact nonzero FRAME_WORDS count and issue START.
  4. Refill TXDATA with the CPU or generic DMA before the FIFO empties.
  5. Wait for DONE; the output remains low for RESET_CYCLES before the frame is complete and the done state is raised.

When TXDATA is full during an active frame, APB4 applies wait-states until a FIFO entry becomes available. A full-FIFO write while idle is rejected instead of waiting indefinitely. Underflow aborts the frame, flushes queued data, sets the underflow and error state, and holds the output low for the configured reset interval. ABORT has the same output-safety behavior and additionally sets the aborted interrupt state. FIFO_FLUSH is accepted only while idle.

rs_ws2812_write() implements bounded CPU refill. rs_ws2812_write_dma() preloads the FIFO, programs the generic DMA for incrementing source and fixed TXDATA destination writes, then starts the frame and DMA. The DMA emits native one-beat AXI4 FIXED writes for this APB4 endpoint and waits for its backpressure; it never sends an APB4 burst or uses RIB. Both paths validate the complete pixel array before modifying peripheral state and use caller timeouts for all waits.

Verification and current scope

The self-checking RTL test verifies exact zero/one pulse widths, MSB-first word order, frame length, reset low time, FIFO backpressure, watermark and done interrupts, invalid accesses, underflow, abort, and software interrupt test. The DMA integration test connects the production dma_core to TXDATA through a native AXI4 BFM and checks fixed-destination writes, full-FIFO backpressure, completion, and the resulting serialized frame. The formal target proves bounded FIFO, APB4 response, idle-low output, and sticky event invariants and covers normal, underflow-precondition, and abort paths. Host C tests cover GRB packing and integer timing conversion. SoC topology tests lock the address, interrupt, and GPIO route.

The current delivery is deliberately one channel and 24-bit GRB. RGBW framing, parallel lanes, per-pixel brightness processing, and a dedicated DMA request line are outside this ABI and require a versioned extension rather than an incompatible register reinterpretation.