AXI4-Lite Crossbar

The interconnect the rest of the catalogue integrates against. Constrained-random routing with a scoreboard covers address decode, response correctness and DECERR; the arbiter's round-robin fairness bound and the crossbar's end-to-end properties are formal proofs. Deadlock freedom is argued structurally — circuit-switched, no partial grants — and written down.

Design choice, documented: one outstanding write and one read per manager. It keeps the latch small and the proofs tractable, and the datasheet says so instead of leaving you to discover it.