Source Files

File	Description
uart.sv	UART core with TX/RX FIFOs, framing, baud control, and oversampled RX
uart_mmio.sv	MMIO wrapper for register level integration and IRQ/status handling
uart_if.sv	Simulation interface shared with the testbench

File	Description
CMakeLists.txt	Simulation build entry point
filelist.f	Source list for the verification build
uart_tb_top.sv	Top level testbench wrapper and DUT hookup
uart_test.sv	UVM test that starts sequences and watches coverage
uart_env.sv	UVM environment that connects agent and scoreboard
uart_agent.sv	Agent wrapper for driver, monitor, and sequencer
uart_drv.sv	Transaction driver
uart_mon.sv	Protocol monitor
uart_scb.sv	Scoreboard
uart_seq.sv	Constrained random sequence
uart_seqr.sv	Sequence item / sequencer support
uart_txn.sv	Transaction definition
uart_cov.sv	Functional coverage model

File	Description
Makefile	Build entry point for SymbiYosys formal verification
README.md	Formal verification environment documentation
env/uart_env.sv	Top-level formal harness wrapping the DUT
env/uart_assumptions.sv	Assumptions about reset behavior and baud configuration
env/uart_coverpoints.sv	Coverpoints for reachability goals
properties/uart_reset.sv	Reset behavior assertions
properties/uart_fifo.sv	FIFO flag and level consistency assertions
properties/uart_status.sv	Status register assertions
properties/uart_tx.sv	TX path protocol assertions
properties/uart_rx.sv	RX path protocol assertions
properties/uart_protocol.sv	TX state machine transition assertions
properties/uart_baud.sv	Baud tick generation assertions
prove/full.sby	SymbiYosys job for bounded/inductive safety proof
cover/full.sby	SymbiYosys job for reachability coverage