UART

A UART built like infrastructure: CSR control with interrupt truth-table semantics, parity/stop/divisor sweeps, FIFO overrun with W1C status — and the parts that silently corrupt data in lesser implementations are formally proven. FIFO occupancy and full shadow-memory data integrity carry unbounded proofs; exact frame timing is a 350-cycle bounded model check over every divisor/parity/stop combination.

An independent line-level BFM decodes every TX frame and injects corrupt and runt RX frames — the encoder and decoder are separate implementations, so a shared misunderstanding cannot cancel out. The echo demo runs on an Arty A7-100T.