← portfolio  /  UART
Overview Verification Sources
Project note

This version is no longer actively maintained. Known bugs and identified issues may remain unresolved here.

The actively maintained design is lives under DMCTP , which builds on this initial architecture with expanded formal and functional verification, improved performance, and improved static timing analysis results.

UART PROJECT · UVM + FORMAL

Configurable UART
with UVM and Formal Verification

Asynchronous serial transceiver with runtime configurable baud rates, FIFO decoupled TX/RX paths, and a register mapped interface. Verified using both UVM constrained random verification and formal property based verification.

Scope
RTL + UVM + Formal
Focus
Randomized stimulus, coverage driven, property proving
Test strategy
Agent based, self checking, formal harness
See testbench → Source files

Module Overview

  • Baud generator: Clock divider with configurable baud rate divisor; produces tick and 16× sample tick
  • TX FSM: Start, data (8 bits), parity (optional), stop (1 or 2 bits); pulls from TX FIFO on demand
  • RX FSM: 16× oversampling with majority voting; detects start edge, samples at bit centers, captures data, validates stop bit
  • TX/RX FIFOs: Decouples serial FSM from CPU facing interface; independent full/empty flags
  • MMIO wrapper: Exposes TXDATA, RXDATA, STATUS, CTRL, IE, IP, DIV registers for integration into larger SoC
Verification approach

The testbench uses constrained random stimulus with transaction level sequencing. A randomized sequence generates TX writes, RX reads, and reset toggles. The driver applies these to the DUT; monitors capture before/after state; and a scoreboard compares expected against observed transactions.

Functional coverage is collected throughout simulation to measure verification progress, with simulations targeting at least 80% functional coverage.

Key verification techniques: UVM agents, transaction level modeling (TLM), constrained random stimulus, reset aware scoreboarding, and functional coverage.
UVM testbench structure

Architecture and components

FIG. 1
top_tb (module) uart_test (uvm_test) uart_seq (uvm_sequence) uart_env (uvm_environment) uart_agent (uvm_agent) uart_cov (uvm_subscriber) uart_seqr (uvm_sequencer) uart_drv (uvm_driver) uart_mon (uvm_monitor) uart_scb (uvm_subscriber) DUT (uart_mmio) uart_txn (uvm_sequence_item) uart_if (interface)
[1] UVM Diagram. (Blue = sequencer/driver handshake, Purple = analysis ports, Black = signals between virtual interface and the DUT).
Implementation details

Key modules and their role

FIG. 2

uart_test.sv

Top-level test. Instantiates environment, starts randomized sequence, and waits for functional coverage to reach 80% before ending the test.

Open source

uart_env.sv

Environment container. Builds agent and scoreboard; connects monitor output ports to scoreboard input ports.

Open source

uart_agent.sv

Active agent. Packages sequencer, driver, and monitor; exposes analysis ports for before/after transaction streams.

Open source

uart_drv.sv

Consumes seq_item_port from sequencer. Applies reset, TX write, and RX read transactions to the virtual interface with proper handshake timing.

Open source

uart_mon.sv

Monitors virtual interface. Captures reset edge, TX completion, and RX completion; publishes observed transactions to analysis port with sequence number stamps.

Open source

uart_scb.sv

Scoreboard with expected/actual queues. Maintains simplified FIFO model of DUT; predicts output; matches against monitor observations. Handles reset-induced queue flushes.

Open source

uart_seq.sv

Randomized sequence body. Generates a weighted mix of TX writes, RX reads, and reset toggles. Each item is randomized (data, timing).

Open source

uart_txn.sv

Transaction class hierarchy. Defines reset_item, tx_item, and rx_item with randomizable fields (data, delay, mode). Implements compare() and print() methods.

Open source
Verification results

The testbench has achieved >80% functional coverage on a randomized stimulus suite. Coverage points are TX/RX byte value distribution (five ranges: zero, low, mid, high, 0xFF), per transaction sequence numbers, and reset occurrence. The scoreboard confirmed zero mismatches after reset aware queueing was added.

Formal Verification

Property-based verification with SymbiYosys

FIG. 3

In addition to the UVM testbench, the UART design has been verified using formal property-based verification. This approach uses SymbiYosys to exhaustively prove safety properties and verify reachability of important protocol states without the need for directed or random test vectors.

Formal verification harness structure:
  • env/uart_env.sv — Top-level formal harness that instantiates the DUT and assembles all property files
  • env/uart_assumptions.sv — Assumptions about reset behavior and baud configuration
  • env/uart_coverpoints.sv — Coverpoints for reachability goals
  • properties/ — Seven property files covering reset, FIFO, status, TX, RX, protocol, and baud generation
  • prove/full.sby — SymbiYosys job for bounded/inductive safety proof (depth 24)
  • cover/full.sby — SymbiYosys job for reachability coverage (depth 220)
  • Reset behavior (P1): All state machines return to idle, TX stays high, FIFOs empty
  • FIFO consistency (P2-P4): Empty/full flags match levels, levels stay within bounds
  • Status correctness (P5): Ready signals reflect FIFO status
  • TX protocol (P6-P10): TX idle is high, start bit is low, state advances only on baud ticks, proper state transitions
  • RX protocol (P11-P13): RX state holds without sample ticks, data valid only on sample ticks
  • Baud generation (P14-P15): Baud and sample ticks match divisor configuration

The proof runs with a depth of 24 cycles for safety properties, while coverage goals explore up to 220 cycles to explore reachable protocol states including reset release, TX/RX enqueue/dequeue, and baud divisor changes.