From 096a07bd79be152834bf2b153daa479561d1c252 Mon Sep 17 00:00:00 2001 From: drewbabel <122849144+drewbabel@users.noreply.github.com> Date: Tue, 21 Jul 2026 23:06:10 -0700 Subject: [PATCH] [docs] Restructure the README --- README.md | 38 +++++++++++++++++++------------------- 1 file changed, 19 insertions(+), 19 deletions(-) diff --git a/README.md b/README.md index 4ef6f41..a13e441 100644 --- a/README.md +++ b/README.md @@ -12,6 +12,25 @@ A configurable UART core written in SystemVerilog. ![Block diagram](docs/block_diagram.svg) +## Verification + +| Module | Method | +|--------|--------| +| `synchronizer` | Self-checking testbench | +| `tick_gen` | Self-checking testbench | +| `uart_tx` | Self-checking testbench + SymbiYosys proofs | +| `uart_rx` | Self-checking testbench + SymbiYosys proofs | +| `uart` | cocotb loopback + FPGA validation | + +Properties proven in formal: +- Transmit interface protocol correctness (`tx_ready` handshake behavior) +- Stable framing behavior and idle-line enforcement +- Receiver framing correctness under oversampling assumptions + +## Results + +![Loopback waveform](docs/loopback_waveform.svg) + ## Parameters | Parameter | Default | Description | @@ -36,25 +55,6 @@ A configurable UART core written in SystemVerilog. | `rx_valid` | out | 1 | One-cycle pulse on valid receive | | `rx_error` | out | 1 | One-cycle pulse on framing error | -## Verification - -| Module | Method | -|--------|--------| -| `synchronizer` | Self-checking testbench | -| `tick_gen` | Self-checking testbench | -| `uart_tx` | Self-checking testbench + SymbiYosys proofs | -| `uart_rx` | Self-checking testbench + SymbiYosys proofs | -| `uart` | cocotb loopback + FPGA validation | - -Properties proven in formal: -- Transmit interface protocol correctness (`tx_ready` handshake behavior) -- Stable framing behavior and idle-line enforcement -- Receiver framing correctness under oversampling assumptions - -## Results - -![Loopback waveform](docs/loopback_waveform.svg) - ## Building and running Every module builds from the top-level Makefile.