trim READMEs to eliminate dual-source-of-truth drift, add --list CLI flags

The hw/rtl, sw, formal, and tests READMEs had exhaustive listings of
every module/app/target that duplicated what was already in code. This
created two sources of truth that were already drifting (3 sw apps were
undocumented in the old README).

- hw/rtl/README: replace file-by-file tree with subdirs-only map;
keep the architectural "Module Details" section (high-value, low-drift)
- sw/README: replace multi-paragraph app descriptions with a compact
20-row table of one-line summaries covering all apps; point to
source-level doc comments as the authoritative detail
- formal/README: replace target table with pointer to --list-targets
- tests/README: replace test table with pointer to --list-tests
- test_run_cocotb.py: add --list-tests flag (single source of truth)
- test_run_formal.py: add --list-targets flag (single source of truth)

Author: adambagley

formal/README.md

@@ -22,17 +22,17 @@ Each `.sby` file defines a verification target with tasks:
 
 ## Targets
 
-| Target | SBY File | Module | Tasks | Properties |
-|--------|----------|--------|-------|------------|
-| **hru** | `hru.sby` | `hazard_resolution_unit` | bmc, cover, prove | Load-use stall contract, branch flush duration, trap override, MMIO termination, CSR bounded, shift register fill, stale flush prevention |
-| **lr_sc** | `lr_sc.sby` | `lr_sc_reservation` | bmc, cover, prove | SC clears reservation, LR sets reservation, SC priority over LR, stall preserves state, reset clears all |
-| **trap_unit** | `trap_unit.sby` | `trap_unit` | bmc, cover | Trap/MRET mutex (RTL-enforced trap priority), trap needs source, interrupt priority, vectored offsets, re-entry prevention, WFI stall |
-| **csr_file** | `csr_file.sby` | `csr_file` | bmc, cover | Trap saves state, MIE/MPIE management, mepc/mtvec alignment, mip reflects inputs, counter increments, fflags sticky |
-| **fwd_unit** | `fwd_unit.sby` | `forwarding_unit` | bmc, cover | MA priority over WB, x0 always zero, no-forward uses raw value, reset clears enables, forward requires write |
-| **fp_fwd_unit** | `fp_fwd_unit.sby` | `fp_forwarding_unit` | bmc, cover | Reset/flush clear enables, pending self-clearing, stall matches pending, capture bypass requires write enable |
-| **cache_hit** | `cache_hit.sby` | `cache_hit_detector` | bmc, cover | MMIO exclusion, non-load exclusion, tag mismatch exclusion, byte/halfword/word valid bit checks |
-| **cache_write** | `cache_write.sby` | `cache_write_controller` | bmc, cover | MMIO stores bypass cache, AMO byte enables, stale load prevention, store valid bit merging |
-| **data_mem_arb** | `data_mem_arb.sby` | `data_mem_arbiter` | bmc, cover | Priority encoding (FP > AMO write > AMO stall > default), stall gates stores, AMO gets all bytes |
+Formal targets are intentionally documented from code, not duplicated in this README.
+The source of truth is `FORMAL_TARGETS` in `tests/test_run_formal.py` plus the `.sby`
+files in this directory.
+
+```bash
+# List all targets and their supported tasks
+./tests/test_run_formal.py --list-targets
+
+# See CLI help (includes --target choices)
+./tests/test_run_formal.py --help
+```
 
 ## Running
 
@@ -42,6 +42,7 @@ pytest tests/test_run_formal.py
 
 # Standalone runner
 ./tests/test_run_formal.py
+./tests/test_run_formal.py --list-targets
 ./tests/test_run_formal.py --target hru
 ./tests/test_run_formal.py --task bmc
 ./tests/test_run_formal.py --verbose
@@ -129,15 +130,7 @@ Yosys supports a subset of SystemVerilog Assertions. Key constraints:
 formal/
 ├── README.md               # This file
 ├── .gitignore              # Ignores sby working directories
-├── hru.sby                 # Hazard resolution unit
-├── lr_sc.sby               # LR/SC reservation register
-├── trap_unit.sby           # Trap unit
-├── csr_file.sby            # CSR file
-├── fwd_unit.sby            # Forwarding unit
-├── fp_fwd_unit.sby         # FP forwarding unit
-├── cache_hit.sby           # Cache hit detector
-├── cache_write.sby         # Cache write controller
-└── data_mem_arb.sby        # Data memory arbiter
+└── *.sby                   # Formal targets (one file per block)
 ```
 
 Assertions live in the RTL files themselves (inside `ifdef FORMAL` blocks), not in separate files.

hw/rtl/README.md

@@ -639,123 +639,29 @@ Cycle N+1:        +--------------+------------------------+
 
 ## Directory Structure
 
+`hw/rtl/frost.f` is the source of truth for synthesis/simulation file ordering and
+module inclusion. This README keeps only a high-level map to avoid drift.
+
 ```
 rtl/
-├── frost.sv                          # Top-level: clocks, resets, I/O integration
-├── frost.f                           # File list for simulation/synthesis
-│
-├── lib/                              # Generic FPGA library components
-│   ├── ram/
-│   │   ├── sdp_dist_ram.sv           # Simple dual-port distributed RAM (async read)
-│   │   ├── mwp_dist_ram.sv        # Multi-write-port distributed RAM (LVT-based)
-│   │   ├── sdp_block_ram.sv          # Simple dual-port block RAM (sync read)
-│   │   ├── sdp_block_ram_dc.sv       # Dual-clock block RAM (for CDC)
-│   │   ├── tdp_bram_dc.sv            # True dual-port RAM (dual-clock, simple)
-│   │   └── tdp_bram_dc_byte_en.sv    # True dual-port RAM (dual-clock, byte enables)
-│   ├── stall_capture_reg.sv          # Pipeline stall capture register (generic utility)
-│   └── fifo/
-│       ├── sync_dist_ram_fifo.sv     # Synchronous FIFO (distributed RAM)
-│       └── dc_fifo.sv                # Dual-clock FIFO (binary pointers)
-│
-├── peripherals/                      # Peripheral modules
-│   ├── uart_tx.sv                    # UART transmitter
-│   └── uart_rx.sv                    # UART receiver
-│
-└── cpu_and_mem/
-    ├── cpu_and_mem.sv                # CPU + memory integration
-    │
-    └── cpu/
-        ├── cpu.sv                    # 6-stage pipeline top-level
-        ├── data_mem_arbiter.sv       # Data memory interface mux (EX/AMO/FP64 arbitration)
-        ├── riscv_pkg.sv              # Type definitions, opcodes, structs
-        │
-        ├── if_stage/                 # Instruction Fetch stage
-        │   ├── if_stage.sv           # PC management, instruction fetch
-        │   ├── pc_controller.sv      # PC update logic, branch targeting
-        │   ├── pc_increment_calculator.sv # Sequential PC computation (parallel adders)
-        │   ├── control_flow_tracker.sv # Holdoff signal generation
-        │   ├── branch_prediction/    # Branch prediction subsystem
-        │   │   ├── branch_predictor.sv           # 32-entry BTB
-        │   │   ├── branch_prediction_controller.sv # Prediction gating logic (BTB + RAS)
-        │   │   ├── prediction_metadata_tracker.sv  # Stall/spanning handling
-        │   │   ├── ras_detector.sv                # Call/return/coroutine detection
-        │   │   └── return_address_stack.sv        # 8-entry return address stack
-        │   └── c_extension/          # Compressed instruction (C ext) support
-        │       ├── c_ext_state.sv        # C extension state machine
-        │       ├── instruction_aligner.sv # Parcel selection, alignment
-        │       └── rvc_decompressor.sv   # 16-bit to 32-bit expansion
-        │
-        ├── pd_stage/                 # Pre-Decode stage
-        │   └── pd_stage.sv           # C extension decompression, early source register extraction
-        │
-        ├── id_stage/                 # Instruction Decode stage
-        │   ├── id_stage.sv           # ID stage integration, pipeline register
-        │   ├── instr_decoder.sv      # Opcode/funct decoder
-        │   ├── immediate_decoder.sv  # I/S/B/U/J immediate extraction
-        │   ├── instruction_type_decoder.sv  # Direct type detection (timing opt)
-        │   └── branch_target_precompute.sv  # Pre-computed targets/prediction verification
-        │
-        ├── ex_stage/                 # Execute stage
-        │   ├── ex_stage.sv           # EX stage integration, pipeline register
-        │   ├── branch_jump_unit.sv   # Branch condition evaluation, target calc
-        │   ├── branch_redirect_unit.sv  # Misprediction detection, BTB/RAS recovery
-        │   ├── store_unit.sv         # Store address/data preparation
-        │   ├── exception_detector.sv # ECALL, EBREAK, misaligned access detection
-        │   ├── alu/
-        │   │   ├── alu.sv            # Main ALU (all extensions)
-        │   │   ├── multiplier.sv     # 4-cycle DSP-tiled multiplier
-        │   │   └── divider.sv        # 17-cycle radix-2 divider (2x folded)
-        │   ├── dsp_tiled_multiplier_unsigned.sv # Shared 27x35 tiled unsigned multiply core
-        │   └── fpu/                  # Floating-Point Unit (F/D extensions)
-        │       ├── fpu.sv            # FPU top-level, operation routing
-        │       ├── fpu_adder_unit.sv # S+D adder wrapper (tracking FSM, NaN-boxing)
-        │       ├── fpu_mult_unit.sv  # S+D multiplier wrapper
-        │       ├── fpu_fma_unit.sv   # S+D FMA wrapper
-        │       ├── fpu_compare_unit.sv # S+D compare/min/max wrapper
-        │       ├── fpu_sign_inject_unit.sv # S+D sign injection wrapper
-        │       ├── fpu_classify_unit.sv # S+D classify wrapper
-        │       ├── fpu_div_sqrt_unit.sv # S+D divider + sqrt wrapper (shared FSM)
-        │       ├── fpu_convert_unit.sv # S+D+SD conversion wrapper
-        │       ├── fp_adder.sv       # Addition/subtraction (4-cycle)
-        │       ├── fp_multiplier.sv  # Multiplication (multi-cycle, non-pipelined)
-        │       ├── fp_divider.sv     # Division (~32-cycle)
-        │       ├── fp_sqrt.sv        # Square root (~32-cycle)
-        │       ├── fp_fma.sv         # Fused multiply-add (multi-cycle, non-pipelined)
-        │       ├── fp_compare.sv     # Comparisons and min/max (3-cycle)
-        │       ├── fp_convert.sv     # Integer/FP conversions (3-cycle)
-        │       ├── fp_classify.sv    # FCLASS.S (1-cycle)
-        │       ├── fp_sign_inject.sv # Sign injection (1-cycle)
-        │       ├── fp_convert_sd.sv  # Single/double conversion (5-cycle)
-        │       ├── fp_result_assembler.sv # Rounding + overflow/underflow + result formatting (shared)
-        │       ├── fp_lzc.sv         # Leading zero counter (shared)
-        │       ├── fp_classify_operand.sv # Operand classifier (shared)
-        │       ├── fp_operand_unpacker.sv # Field extraction + classification (shared)
-        │       └── fp_subnorm_shift.sv # Subnormal right-shift (shared)
-        │
-        ├── ma_stage/                 # Memory Access stage
-        │   ├── ma_stage.sv           # Load completion, AMO coordination
-        │   ├── load_unit.sv          # Load data extraction/extension
-        │   ├── amo_unit.sv           # Atomic memory operation state machine
-        │   └── fp64_sequencer.sv     # FP64 load/store sequencer (FLD/FSD over 32-bit bus)
-        │
-        ├── wb_stage/                 # Writeback stage
-        │   └── generic_regfile.sv    # Parameterized register file (int 2R/1W, FP 3R/1W)
-        │
-        ├── cache/                    # Cache subsystem
-        │   ├── l0_cache.sv           # Direct-mapped L0 data cache
-        │   ├── cache_hit_detector.sv # Cache hit detection logic
-        │   └── cache_write_controller.sv # Cache write enable and data muxing
-        │
-        ├── csr/                      # CSR subsystem (Zicsr + Zicntr + M-mode)
-        │   └── csr_file.sv           # CSR register file (M-mode + counters)
-        │
-        └── control/                  # Pipeline control
-            ├── forwarding_unit.sv    # Integer data hazard forwarding
-            ├── fp_forwarding_unit.sv # FP data hazard forwarding (F/D extensions)
-            ├── hazard_resolution_unit.sv # Stall/flush control (incl. FPU stalls)
-            ├── hru_fp_hazards.sv    # FP hazard detection (submodule of HRU)
-            ├── trap_unit.sv          # Interrupt/exception handling
-            └── lr_sc_reservation.sv  # A extension: LR/SC address reservation
+├── frost.sv            # Top-level integration
+├── frost.f             # Authoritative file list
+├── lib/                # Reusable RAM/FIFO/util blocks
+├── peripherals/        # UART and MMIO-facing blocks
+└── cpu_and_mem/        # CPU pipeline and memory subsystem
+```
+
+Useful discovery commands (from repo root):
+
+```bash
+# All RTL modules currently in-tree
+find hw/rtl -name '*.sv' | sort
+
+# Files included for build/simulation
+sed -n '1,200p' hw/rtl/frost.f
+
+# Tomasulo-related modules
+find hw/rtl/cpu_and_mem/cpu/tomasulo -name '*.sv' | sort
 ```
 
 ## Module Details